Paper 2010/080

Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols

Gergei Bana, Koji Hasebe, and Mitsuhiro Okada

Abstract

We present a computationally sound first-order system for security analysis of protocols that places secrecy of nonces and keys in its center. Even trace properties such as agreement and authentication are proven via proving a non-trace property, namely, secrecy first. This results a very powerful system, the working of which we illustrate on the agreement and authenti- cation proofs for the Needham-Schroeder-Lowe public-key and the amended Needham-Schroeder shared-key protocols in case of unlimited sessions. Unlike other available formal verification techniques, computational soundness of our approach does not require any idealizations about parsing of bitstrings or unnecessary tagging. In particular, we have total control over detecting or eliminating the possibility of type-flaw attacks.

Note: Minor corrections

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Keywords
cryptographic protocolsformal methodsfirst order logiccomputational semantics
Contact author(s)
bana @ math upenn edu
History
2010-07-20: last of 4 revisions
2010-02-16: received
See all versions
Short URL
https://ia.cr/2010/080
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2010/080,
      author = {Gergei Bana and Koji Hasebe and Mitsuhiro Okada},
      title = {Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2010/080},
      year = {2010},
      note = {\url{https://eprint.iacr.org/2010/080}},
      url = {https://eprint.iacr.org/2010/080}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.