diff --git a/manual/scyther-manual.idx b/manual/scyther-manual.idx
new file mode 100644
index 0000000..393936a
--- /dev/null
+++ b/manual/scyther-manual.idx
@@ -0,0 +1,122 @@
+\indexentry{Scyther website}{5}
+\indexentry{website|see{Scyther website}}{5}
+\indexentry{downloading Scyther}{9}
+\indexentry{installing Scyther}{9}
+\indexentry{quick start tutorial}{11}
+\indexentry{comments}{15}
+\indexentry{whitespace}{15}
+\indexentry{identifier}{15}
+\indexentry{case-sensitive}{15}
+\indexentry{atomic term}{15}
+\indexentry{constant}{16}
+\indexentry{global constant}{16}
+\indexentry{freshly generated value}{16}
+\indexentry{nonce}{16}
+\indexentry{random value}{16}
+\indexentry{variable}{16}
+\indexentry{var}{16}
+\indexentry{pairing}{16}
+\indexentry{tupling}{16}
+\indexentry{symmetric keys}{16}
+\indexentry{k(X,Y)@\spd{k(X,Y)}}{16}
+\indexentry{asymmetric keys}{17}
+\indexentry{sk(X)@\spd{sk(X)}}{17}
+\indexentry{pk(X)@\spd{pk(X)}}{17}
+\indexentry{hash functions}{17}
+\indexentry{hashfunction@\spd{hashfunction}}{17}
+\indexentry{Agent@{\tt  Agent}}{17}
+\indexentry{Function@{\tt  Function}}{17}
+\indexentry{Nonce@{\tt  Nonce}}{17}
+\indexentry{Ticket@{\tt  Ticket}}{17}
+\indexentry{usertype@{\tt  usertype}}{17}
+\indexentry{events}{18}
+\indexentry{send@{\tt  send}}{18}
+\indexentry{event!send}{18}
+\indexentry{event!recv}{18}
+\indexentry{send@{\tt  send}}{18}
+\indexentry{recv@{\tt  recv}}{18}
+\indexentry{20@{\tt "!}}{18}
+\indexentry{event!claim}{18}
+\indexentry{claim event}{18}
+\indexentry{security properties}{18}
+\indexentry{claim@{\tt  claim}}{18}
+\indexentry{Secret@{\tt  Secret}}{19}
+\indexentry{SKR@{\tt  SKR}}{19}
+\indexentry{Alive@{\tt  Alive}}{19}
+\indexentry{Weakagree@{\tt  Weakagree}}{19}
+\indexentry{Commit@{\tt  Commit}}{19}
+\indexentry{Running@{\tt  Running}}{19}
+\indexentry{agreement on data}{19}
+\indexentry{data agreement}{19}
+\indexentry{non-injective agreement}{19}
+\indexentry{Nisynch@{\tt  Nisynch}}{19}
+\indexentry{synchronisaton}{19}
+\indexentry{non-injective synchronisation}{19}
+\indexentry{Niagree@{\tt  Niagree}}{19}
+\indexentry{agreement (on messages)}{19}
+\indexentry{message agreement}{19}
+\indexentry{non-injective agreement}{19}
+\indexentry{Reachable@{\tt  Reachable}}{19}
+\indexentry{Empty@{\tt  Empty}}{19}
+\indexentry{internal computation events}{19}
+\indexentry{pattern match events}{19}
+\indexentry{match event}{19}
+\indexentry{event!match}{19}
+\indexentry{not match event}{20}
+\indexentry{event!not match}{20}
+\indexentry{role definition}{20}
+\indexentry{protocol definition}{20}
+\indexentry{helper protocol|textbf}{21}
+\indexentry{19@"@}{21}
+\indexentry{symmetric-role protocol|textbf}{21}
+\indexentry{global declarations}{21}
+\indexentry{const@{\tt  const}}{21}
+\indexentry{macro@{\tt  macro}}{22}
+\indexentry{abbreviate}{22}
+\indexentry{define macro}{22}
+\indexentry{include@{\tt  include}}{22}
+\indexentry{import file}{22}
+\indexentry{input file}{22}
+\indexentry{one-role-per-agent@{\tt  one-role-per-agent}}{23}
+\indexentry{one role per agent}{23}
+\indexentry{multiple roles per agent}{23}
+\indexentry{BNF}{23}
+\indexentry{Needham-Schroeder protocol}{25}
+\indexentry{NS|see{Needham-Schroeder protocol}}{25}
+\indexentry{Commit@{\tt  Commit}}{29}
+\indexentry{Running@{\tt  Running}}{29}
+\indexentry{agreement on data}{29}
+\indexentry{data agreement}{29}
+\indexentry{non-injective agreement}{29}
+\indexentry{GUI}{31}
+\indexentry{at least X attack(s)}{31}
+\indexentry{exactly X attack(s)}{32}
+\indexentry{exactly X pattern(s)}{32}
+\indexentry{at least X pattern(s)}{32}
+\indexentry{no attacks within bounds}{32}
+\indexentry{no attacks}{32}
+\indexentry{verification}{32}
+\indexentry{attack graph}{33}
+\indexentry{attack window}{33}
+\indexentry{run}{33}
+\indexentry{communication event}{35}
+\indexentry{construct}{35}
+\indexentry{command-line tools}{37}
+\indexentry{GUI!using Scyther without GUI}{37}
+\indexentry{multiple asymmetric key pairs per agent}{39}
+\indexentry{asymmetric key!multiple pairs per agent}{39}
+\indexentry{equational theories}{39}
+\indexentry{exponentiation|see{Diffie-Hellman exponentiation}}{39}
+\indexentry{Diffie-Hellman exponentiation}{39}
+\indexentry{bidirectional keys}{39}
+\indexentry{syntactic equality}{39}
+\indexentry{helper protocol}{39}
+\indexentry{time-stamps|(}{41}
+\indexentry{counter|see{global counter}}{41}
+\indexentry{global counter|(}{41}
+\indexentry{global counter|)}{41}
+\indexentry{time-stamps|)}{42}
+\indexentry{multi-protocol attacks}{42}
+\indexentry{cross-protocol attacks}{42}
+\indexentry{chosen protocol attacks}{42}
+\indexentry{read@{\tt  read}}{51}
diff --git a/manual/scyther-manual.ilg b/manual/scyther-manual.ilg
new file mode 100644
index 0000000..03a57d9
--- /dev/null
+++ b/manual/scyther-manual.ilg
@@ -0,0 +1,6 @@
+This is makeindex, version 2.16 [TeX Live 2022] (kpathsea + Thai support).
+Scanning input file scyther-manual.idx....done (122 entries accepted, 0 rejected).
+Sorting entries....done (900 comparisons).
+Generating output file scyther-manual.ind....done (181 lines written, 0 warnings).
+Output written in scyther-manual.ind.
+Transcript written in scyther-manual.ilg.
diff --git a/manual/scyther-manual.ind b/manual/scyther-manual.ind
new file mode 100644
index 0000000..88d1d1f
--- /dev/null
+++ b/manual/scyther-manual.ind
@@ -0,0 +1,181 @@
+\begin{theindex}
+
+  \item @, 21
+  \item {\tt !}, 18
+
+  \indexspace
+
+  \item abbreviate, 22
+  \item {\tt  Agent}, 17
+  \item agreement (on messages), 19
+  \item agreement on data, 19, 29
+  \item {\tt  Alive}, 19
+  \item asymmetric key
+    \subitem multiple pairs per agent, 39
+  \item asymmetric keys, 17
+  \item at least X attack(s), 31
+  \item at least X pattern(s), 32
+  \item atomic term, 15
+  \item attack graph, 33
+  \item attack window, 33
+
+  \indexspace
+
+  \item bidirectional keys, 39
+  \item BNF, 23
+
+  \indexspace
+
+  \item case-sensitive, 15
+  \item chosen protocol attacks, 42
+  \item {\tt  claim}, 18
+  \item claim event, 18
+  \item command-line tools, 37
+  \item comments, 15
+  \item {\tt  Commit}, 19, 29
+  \item communication event, 35
+  \item {\tt  const}, 21
+  \item constant, 16
+  \item construct, 35
+  \item counter, \see{global counter}{41}
+  \item cross-protocol attacks, 42
+
+  \indexspace
+
+  \item data agreement, 19, 29
+  \item define macro, 22
+  \item Diffie-Hellman exponentiation, 39
+  \item downloading Scyther, 9
+
+  \indexspace
+
+  \item {\tt  Empty}, 19
+  \item equational theories, 39
+  \item event
+    \subitem claim, 18
+    \subitem match, 19
+    \subitem not match, 20
+    \subitem recv, 18
+    \subitem send, 18
+  \item events, 18
+  \item exactly X attack(s), 32
+  \item exactly X pattern(s), 32
+  \item exponentiation, \see{Diffie-Hellman exponentiation}{39}
+
+  \indexspace
+
+  \item freshly generated value, 16
+  \item {\tt  Function}, 17
+
+  \indexspace
+
+  \item global constant, 16
+  \item global counter, 41
+  \item global declarations, 21
+  \item GUI, 31
+    \subitem using Scyther without GUI, 37
+
+  \indexspace
+
+  \item hash functions, 17
+  \item \spd{hashfunction}, 17
+  \item helper protocol, \textbf{21}, 39
+
+  \indexspace
+
+  \item identifier, 15
+  \item import file, 22
+  \item {\tt  include}, 22
+  \item input file, 22
+  \item installing Scyther, 9
+  \item internal computation events, 19
+
+  \indexspace
+
+  \item \spd{k(X,Y)}, 16
+
+  \indexspace
+
+  \item {\tt  macro}, 22
+  \item match event, 19
+  \item message agreement, 19
+  \item multi-protocol attacks, 42
+  \item multiple asymmetric key pairs per agent, 39
+  \item multiple roles per agent, 23
+
+  \indexspace
+
+  \item Needham-Schroeder protocol, 25
+  \item {\tt  Niagree}, 19
+  \item {\tt  Nisynch}, 19
+  \item no attacks, 32
+  \item no attacks within bounds, 32
+  \item non-injective agreement, 19, 29
+  \item non-injective synchronisation, 19
+  \item {\tt  Nonce}, 17
+  \item nonce, 16
+  \item not match event, 20
+  \item NS, \see{Needham-Schroeder protocol}{25}
+
+  \indexspace
+
+  \item one role per agent, 23
+  \item {\tt  one-role-per-agent}, 23
+
+  \indexspace
+
+  \item pairing, 16
+  \item pattern match events, 19
+  \item \spd{pk(X)}, 17
+  \item protocol definition, 20
+
+  \indexspace
+
+  \item quick start tutorial, 11
+
+  \indexspace
+
+  \item random value, 16
+  \item {\tt  Reachable}, 19
+  \item {\tt  read}, 51
+  \item {\tt  recv}, 18
+  \item role definition, 20
+  \item run, 33
+  \item {\tt  Running}, 19, 29
+
+  \indexspace
+
+  \item Scyther website, 5
+  \item {\tt  Secret}, 19
+  \item security properties, 18
+  \item {\tt  send}, 18
+  \item \spd{sk(X)}, 17
+  \item {\tt  SKR}, 19
+  \item symmetric keys, 16
+  \item symmetric-role protocol, \textbf{21}
+  \item synchronisaton, 19
+  \item syntactic equality, 39
+
+  \indexspace
+
+  \item {\tt  Ticket}, 17
+  \item time-stamps, 41--42
+  \item tupling, 16
+
+  \indexspace
+
+  \item {\tt  usertype}, 17
+
+  \indexspace
+
+  \item var, 16
+  \item variable, 16
+  \item verification, 32
+
+  \indexspace
+
+  \item {\tt  Weakagree}, 19
+  \item website, \see{Scyther website}{5}
+  \item whitespace, 15
+
+\end{theindex}
diff --git a/manual/scyther-manual.pdf b/manual/scyther-manual.pdf
index 9233625..187e8e9 100644
Binary files a/manual/scyther-manual.pdf and b/manual/scyther-manual.pdf differ
diff --git a/manual/scyther-manual.tex b/manual/scyther-manual.tex
index 443e515..262f053 100644
--- a/manual/scyther-manual.tex
+++ b/manual/scyther-manual.tex
@@ -286,7 +286,7 @@ More help can be found online on the Scyther website:
 \index{Scyther website}
 \index{website|see{Scyther website}}
 \medskip
-\url{http://users.ox.ac.uk/~coml0529/scyther/index.html}
+\url{https://cispa.saarland/group/cremers/scyther/index.html}
 \medskip
 
 \noindent
@@ -331,7 +331,7 @@ their properties.
 Scyther can be downloaded from the following website:
 
 \index{downloading Scyther}
-\url{http://users.ox.ac.uk/~coml0529/scyther/}
+\url{https://cispa.saarland/group/cremers/scyther/index.html}
 
 \medskip