International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Key confirmation and adaptive corruptions in the protocol security logic

Authors:
Prateek Gupta
Vitaly Shmatikov
Download:
URL: http://eprint.iacr.org/2006/171
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2006-21664,
  title={Key confirmation and adaptive corruptions in the protocol security logic},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols, formal methods, computational soundness},
  url={http://eprint.iacr.org/2006/171},
  note={FCS-ARSPA 2006 (Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis) shmat@cs.utexas.edu 13346 received 16 May 2006, last revised 17 Jul 2006},
  author={Prateek Gupta and Vitaly Shmatikov},
  year=2006
}