-begins with the logic of Burrows, Abadi and Needham \cite{Burrows:1989:LAa}.
-Their approach requires a `formalising' step, in which one expresses in the
-logic the contents of the message flows, and the \emph{beliefs} of the
-participants.
-
-Bellare and Rogaway \cite{Bellare:1994:EAK} describe a model for studying the
-computational security of authentication and key-exchange protocols in a
-concurrent setting, i.e., where multiple parties are running several
-instances of a protocol simultaneously. They define a notion of security in
-this setting, and show that several simple protocols achieve this notion.
-Their original paper dealt with pairs of parties using symmetric
-cryptography; they extended their definitions in \cite{Bellare:1995:PSS} to
-study three-party protocols involving a trusted key-distribution centre.
-
-Blake-Wilson, Johnson and Menezes \cite{Blake-Wilson:1997:KAP} applied the
-model of \cite{Bellare:1994:EAK} to key-exchange protocols using asymmetric
-cryptography, and Blake-Wilson and Menezes \cite{Blake-Wilson:1998:EAA}
-applied it to protocols based on the Diffie-Hellman protocol.
-
-The security notion of \cite{Bellare:1994:EAK} is based on a \emph{game}, in
-which an adversary nominates a \emph{challenge session}, and is given either
-the key agreed by the participants of the challenge session, or a random
-value independently sampled from an appropriate distribution. The
-adversary's advantage -- and hence the insecurity of the protocol -- is
-measured by its success probability in guessing whether the value it was
-given is really the challenge key. This challenge-session notion was also
-used by the subsequent papers described above.
-
-Bellare, Canetti and Krawczyk \cite{Bellare:1998:MAD} described a pair of
-models which they called the \textsc{am} (for `authenticated links model')
-and \textsc{um} (`unauthenticated links model'). They propose a modular
-approach to the design of key-exchange protocols, whereby one first designs a
-protocol and proves its security in the \textsc{am}, and then applies a
-authenticating `compiler' to the protocol which they prove yields a protocol
-secure in the realistic \textsc{um}. Their security notion is new. They
-define an `ideal model', in which an adversary is limited to assigning
-sessions fresh, random and unknown keys, or matching up one session with
-another, so that both have the same key. They define a protocol to be secure
-if, for any adversary~$A$ in the \textsc{am} or \textsc{um}, there is an
-ideal adversary~$I$, such that the outputs of $A$ and $I$ are computationally
-indistinguishable.
-
-In \cite{cryptoeprint:1999:012}, Shoup presents a new model for key-exchange,
-also based on the idea of simulation. He analyses the previous models,
-particularly \cite{Bellare:1994:EAK} and \cite{Bellare:1998:MAD}, and
-highlights some of their inadequacies.
+begins with the logic of Burrows, Abadi and Needham
+\cite{burrows-1989:logic-authn}. Their approach requires a `formalising'
+step, in which one expresses in the logic the contents of the message flows,
+and the \emph{beliefs} of the participants.
+
+Bellare and Rogaway \cite{bellare-rogaway-1994:entity-authn-key-distrib}
+describe a model for studying the computational security of authentication
+and key-exchange protocols in a concurrent setting, i.e., where multiple
+parties are running several instances of a protocol simultaneously. They
+define a notion of security in this setting, and show that several simple
+protocols achieve this notion. Their original paper dealt with pairs of
+parties using symmetric cryptography; they extended their definitions in
+\cite{bellare-rogaway-1995:session-key-distrib} to study three-party
+protocols involving a trusted key-distribution centre.
+
+Blake-Wilson, Johnson and Menezes \cite{blake-wilson-1997:key-agreement}
+applied the model of \cite{bellare-rogaway-1994:entity-authn-key-distrib} to
+key-exchange protocols using asymmetric cryptography, and Blake-Wilson and
+Menezes \cite{blake-wilson-menezes-1998:asymm-key-transport} applied it to
+protocols based on the Diffie-Hellman protocol.
+
+The security notion of \cite{bellare-rogaway-1994:entity-authn-key-distrib}
+is based on a \emph{game}, in which an adversary nominates a \emph{challenge
+session}, and is given either the key agreed by the participants of the
+challenge session, or a random value independently sampled from an
+appropriate distribution. The adversary's advantage -- and hence the
+insecurity of the protocol -- is measured by its success probability in
+guessing whether the value it was given is really the challenge key. This
+challenge-session notion was also used by the subsequent papers described
+above.
+
+Bellare, Canetti and Krawczyk \cite{bellare-1998:modular-key-exchange}
+described a pair of models which they called the \textsc{am} (for
+`authenticated links model') and \textsc{um} (`unauthenticated links model').
+They propose a modular approach to the design of key-exchange protocols,
+whereby one first designs a protocol and proves its security in the
+\textsc{am}, and then applies a authenticating `compiler' to the protocol
+which they prove yields a protocol secure in the realistic \textsc{um}.
+Their security notion is new. They define an `ideal model', in which an
+adversary is limited to assigning sessions fresh, random and unknown keys, or
+matching up one session with another, so that both have the same key. They
+define a protocol to be secure if, for any adversary~$A$ in the \textsc{am}
+or \textsc{um}, there is an ideal adversary~$I$, such that the outputs of $A$
+and $I$ are computationally indistinguishable.
+
+In \cite{shoup-1999:formal-model-key-exchange}, Shoup presents a new model
+for key-exchange, also based on the idea of simulation. He analyses the
+previous models, particularly
+\cite{bellare-rogaway-1994:entity-authn-key-distrib} and
+\cite{bellare-1998:modular-key-exchange}, and highlights some of their inadequacies.