Universally Composable Symbolic Analysis of Mutual Authentication and Key Exchange Protocols
| Title | Universally Composable Symbolic Analysis of Mutual Authentication and Key Exchange Protocols |
| Publication Type | Conference Paper |
| Year of Publication | 2006 |
| Authors | Canetti, Ran, and Jonathan Herzog |
| Conference Name | Proceedings, Theory of Cryptography Conference (TCC) |
| Date Published | March |
| Abstract | Symbolic analysis of cryptographic protocols is dramatically
simpler than full-fledged cryptographic analysis. In particular, it is simple enough to be automated. However, symbolic analysis does not, by
itself, provide 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 concentrate on mutual authentication and key-exchange protocols. We restrict attention to protocols that use public-key
encryption as their only cryptographic primitive and have a specific restricted format. We define a mapping from such protocols to Dolev-Yao
style symbolic protocols, and show that the symbolic protocol satisfies a
certain symbolic criterion if and only if the corresponding cryptographic
protocol is UC-secure. 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 our treatment, we use an existing tool to automatically verify whether some prominent key-exchange
protocols are UC-secure. |
| URL | http://files.jonathanherzog.com/canetti_universally_conf.pdf |
