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 protocolsformal methodscomputational 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},
note = {\url{https://eprint.iacr.org/2006/171}},
url = {https://eprint.iacr.org/2006/171}
}
