International Association for Cryptologic Research

International Association
for Cryptologic Research


Sebastian Gajek


Universally Composable Symbolic Analysis of Diffie-Hellman based Key Exchange
Ran Canetti Sebastian Gajek
Canetti and Herzog (TCC'06) show how to efficiently perform fully automated, computationally sound security analysis of key exchange protocols with an unbounded number of sessions. A key tool in their analysis is {\em composability}, which allows deducing security of the multi-session case from the security of a single session. However, their framework only captures protocols that use public key encryption as the only cryptographic primitive, and only handles static corruptions. We extend the [CH'06] modeling in two ways. First, we handle also protocols that use digital signatures and Diffie-Hellman exchange. Second, we handle also forward secrecy under fully adaptive party corruptions. This allows us to automatically analyze systems that use an unbounded number of sessions of realistic key exchange protocols such as the ISO 9798-3 or TLS protocol. A central tool in our treatment is a new abstract modeling of plain Diffie-Hellman key exchange. Specifically, we show that plain Diffie-Hellman securely realizes an idealized version of Key Encapsulation.
Universally Composable Security Analysis of TLS---Secure Sessions with Handshake and Record Layer Protocols
We present a security analysis of the complete TLS protocol in the Universal Composable security framework. This analysis evaluates the composition of key exchange functionalities realized by the TLS handshake with the message transmission of the TLS record layer to emulate secure communication sessions and is based on the adaption of the secure channel model from Canetti and Krawczyk to the setting where peer identities are not necessarily known prior the protocol invocation and may remain undisclosed. Our analysis shows that TLS, including the Diffie-Hellman and key transport suites in the uni-directional and bi-directional models of authentication, securely emulates secure communication sessions.