Paper 2006/171

Key confirmation and adaptive corruptions in the protocol security logic

Prateek Gupta and Vitaly Shmatikov


Cryptographic security for key exchange and secure session establishment protocols is often defined in the so called ``adaptive corruptions'' model. Even if the adversary corrupts one of the participants in the middle of the protocol execution and obtains the victim's secrets such as the private signing key, the victim must be able to detect this and abort the protocol. This is usually achieved by adding a key confirmation message to the protocol. Conventional symbolic methods for protocol analysis assume unforgeability of digital signatures, and thus cannot be used to reason about security in the adaptive corruptions model. We present a symbolic protocol logic for reasoning about authentication and key confirmation in key exchange protocols. The logic is cryptographically sound: a symbolic proof of authentication and secrecy implies that the protocol is secure in the adaptive corruptions model. We illustrate our method by formally proving security of an authenticated Diffie-Hellman protocol with key confirmation.

Available format(s)
Publication info
Published elsewhere. FCS-ARSPA 2006 (Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis)
cryptographic protocolsformal methodscomputational soundness
Contact author(s)
shmat @ cs utexas edu
2006-07-17: revised
2006-05-17: received
See all versions
Short URL
Creative Commons Attribution


      author = {Prateek Gupta and Vitaly Shmatikov},
      title = {Key confirmation and adaptive corruptions in the protocol security logic},
      howpublished = {Cryptology ePrint Archive, Paper 2006/171},
      year = {2006},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.