\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}