Cryptology ePrint Archive: Report 2004/334
Universally Composable Symbolic Analysis of Cryptographic Protocols (The case of encryption-based mutual authentication and key exchange)
Ran Canetti and Jonathan Herzog
Abstract: Symbolic analysis of cryptographic protocols is dramatically simpler than full-fledged cryptographic analysis. In particular, it is readily amenable to automation. However, symbolic analysis does not a priori carry any cryptographic soundness guarantees. Following recent work on cryptographically sound symbolic analysis, we demonstrate how Dolev-Yao style symbolic analysis can be used to assert the security of cryptographic protocols within the universally composable (UC) security framework. Consequently, our methods enable security analysis that is completely symbolic, and at the same time cryptographically sound with strong composability properties.
More specifically, we define a mapping from a class of cryptographic protocols to Dolev-Yao style symbolic protocols. For this mapping, we show that the symbolic protocol satisfies a certain symbolic criterion if and only if the corresponding cryptographic protocol is UC-secure. We concentrate on mutual authentication and key-exchange protocols that use public-key encryption as their only cryptographic primitive. For mutual authentication, our symbolic criterion is similar to the traditional Dolev-Yao criterion. For key exchange, we demonstrate that the traditional Dolev-Yao style symbolic criterion is insufficient, and formulate an adequate symbolic criterion.
Finally, to demonstrate the viability of the treatment, we use an existing automated verification tool to assert UC security of some prominent key exchange protocols.
Category / Keywords: foundations / symbolic analysis, formal methods, cryptographic soundness, protocol composition
Publication Info: To appear at JoC. Preliminary version in TCC '06.
Date: received 2 Dec 2004, last revised 13 Oct 2009
Contact author: canetti at watson ibm com
Available formats: PDF | BibTeX Citation
Note: Updates in the Feb 05 version from the original version (Nov 04): New result added: fully-automated verification of real-or-random secrecy for Needham-Schroeder-Lowe protocol. Also, new abstract and introduction. (Lastly, minor bug-fix to Definition 15, key agreement).
Further updates in the current version (Sept 05): Added an overview, and fixed two bugs: one in the definition of F_cpke, and one in the proof of Theorem 3.
Updates in the October 09 version: Updates mainly to the introduction and overciew sections.
Version: 20091013:071933 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]