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.
Category / Keywords: cryptographic protocols / Automated Proofs, Universal Composition, Diffie-Hellman key exchange, forward secrecy Date: received 20 May 2010 Contact author: gajek at post tau ac il Available format(s): PDF | BibTeX Citation Version: 20100525:210708 (All versions of this report) Short URL: ia.cr/2010/303 Discussion forum: Show discussion | Start new discussion