+Many proposed key-exchange protocols have turned out to have subtle security
+flaws. The idea of using formal methods to analyse key-exchange protocols
+begins with the logic of Burrows, Abadi and Needham \cite{Burrows:1989:LA}.
+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{Shoup:1999:OFM}, 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.
+
+Canetti and Krawczyk \cite{Canetti:2001:AKE} describe a new notion of
+security in the basic model of \cite{Bellare:1998:MAD}, based on the
+challenge-session notion of \cite{Bellare:1994:EAK}. The security notion,
+called `SK-security', seems weaker in various ways than those of earlier
+works such as \cite{Bellare:1994:EAK} or \cite{Shoup:1999:OFM}. However, the
+authors show that their notion suffices for constructing `secure channel'
+protocols, which they also define.
+
+In \cite{Canetti:2001:UCP}, Canetti describes the `universal composition'
+framework. Here, security notions are simulation-based: one defines security
+notions by presenting an `ideal functionality'. A protocol securely
+implements a particular functionality if, for any adversary interacting with
+parties who use the protocol, there is an adversary which interacts with
+parties using the ideal functionality such that no `environment' can
+distinguish the two. The environment is allowed to interact freely with the
+adversary throughout, differentiating this approach from that of
+\cite{Bellare:1998:MAD} and \cite{Shoup:1999:OFM}, where the distinguisher
+was given only transcripts of the adversary's interaction with the parties.
+With security defined in this way, it's possible to prove a `universal
+composition theorem': one can construct a protocol, based upon various ideal
+functionalities, and then `plug in' secure implementations of the ideal
+functionalities and appeal to the theorem to prove the security of the entire
+protocol. The UC framework gives rise to very strong notions of security,
+due to the interactive nature of the `environment' distinguisher.
+
+Canetti and Krawczyk \cite{Canetti:2002:UCN} show that the SK-security notion
+of \cite{Canetti:2001:AKE} is \emph{equivalent} to a `relaxed' notion of
+key-exchange security in the UC framework, and suffices for the construction
+of UC secure channels.
+
+The result of \cite{Canetti:2002:UCN} gives us confidence that SK-security is
+the `right' notion of security for key-exchange protocols. Accordingly,
+SK-security is the standard against which we analyse our key-exchange
+protocol.
~mdw / doc / wrestlers / commitdiff