Key confirmation and adaptive corruptions in the protocol security logic

Prateek Gupta; Vitaly Shmatikov

Paper 2006/171

Key confirmation and adaptive corruptions in the protocol security logic

Prateek Gupta and Vitaly Shmatikov

Abstract

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.

Metadata

Available format(s): PDF PS
Publication info: Published elsewhere. FCS-ARSPA 2006 (Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis)
Keywords: cryptographic protocols formal methods computational soundness
Contact author(s): shmat @ cs utexas edu
History: 2006-07-17: revised; 2006-05-17: received; See all versions
Short URL: https://ia.cr/2006/171
License: CC BY

BibTeX

@misc{cryptoeprint:2006/171,
      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},
      url = {https://eprint.iacr.org/2006/171}
}