Abstract
In the design and analysis of authentication and key agreement protocols, provably secure formal methods play a very important role, among which the Canetti-Krawczyk (CK) model and universal composable (UC) security model are very popular at present. This chapter focuses on these two models and consists mainly of three parts: (1) an introduction to CK model and UC models; (2) A study of these two models, which includes an analysis of CK model and an extension of UC security model. The analysis of CK model presents its security analysis, advantages, and disadvantages, and a bridge between this formal method and the informal method (heuristic method) is established; an extension of UC security model gives a universally composable anonymous hash certification model. (3) The applications of these two models. With these two models, the four-way handshake protocols in 802.11i and Chinese wireless LAN (WLAN) security standard WLAN authentication and privacy infrastructure (WAPI) are analyzed.
Key Terms in this Chapter
Composition Theorem: The key advantage of UC security is that we can create a complex protocol from already designed sub-protocols that securely achieves the given local tasks. This is very important since complex systems are usually divided into several sub-systems, each one performing a specific task securely. Canetti presented this feature as the composition theorem (Canetti, 2001). This theorem assures that we can generally construct a large size “UC-secure” cryptographic protocol by using sub-protocols which is proven as secure in UC-secure manner.
Explicit Key Authentication: Explicit key authentication is the property obtained when both (implicit) key authentication and key confirmation hold.
Key-Agreement Protocol: A key-agreement protocol or mechanism is a key establishment technique in which a shared secret is derived by two (or more) parties as a function of information contributed by, or associated with, each of these, (ideally) such that no party can predetermine the resulting value.
Session-Key Security: A KE protocol p is called Session-key secure (or SK-secure) if the following properties hold for any KE-adversary M:
Acknowledgment (ACK) property: Let F an ideal functionality and let p be an SK-secure KE protocol in the F -hybrid model. An algorithm I is said to be an internal state simulator for p if for any environment machine Z and any adversary A we have HYBp,A,Z HYB,A,Z,I
Universally Composable (UC) Security: In UC framework, real protocol p securely realizes ideal functionality if F, for ? A and ? Z, it has the same “action” as F,. Formally, a protocol p securely realizes an ideal functionality F is for any real-life adversary A there exists an ideal-process adversary S such that, for any environment Z and on any input, the probability that Z outputs “1” after interacting witha A and parties running p in the real-life model differs by at most a negligible fraction from the probability that Z outputs “1” after interacting with S and F in the ideal process.
(Implicit) Key Authentication: (Implicit) key authentication is the property whereby one party is assured that no other party aside from a specifically identified second party (and possibly additional identified trusted parties) may gain access to a particular secret key.
Key Confirmation: Key confirmation is the property whereby one party is assured that a second (possibly unidentified) party actually has possession of a particular secret key.