International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols

Gergei Bana
Koji Hasebe
Mitsuhiro Okada
Search ePrint
Search Google
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.
  title={Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols / cryptographic protocols, formal methods, first order logic, computational semantics},
  note={ 14810 received 13 Feb 2010, last revised 20 Jul 2010},
  author={Gergei Bana and Koji Hasebe and Mitsuhiro Okada},