Paper 2018/510

Key-Secrecy of PACE with OTS/CafeOBJ

Dominik Klein

Abstract

The ICAO-standardized Password Authenticated Connection Establishment (PACE) protocol is used all over the world to secure access to electronic passports. Key-secrecy of PACE is proven by first modeling it as an Observational Transition System (OTS) in CafeOBJ, and then proving invariant properties by induction.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. FTSCS 2014: Formal Techniques for Safety-Critical Systems pp 159-173
DOI
10.1007/978-3-319-17581-2_11
Keywords
smart cardsprotocol verificationSecurity Protocol
Contact author(s)
dominik klein @ bsi bund de
History
2018-05-26: received
Short URL
https://ia.cr/2018/510
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2018/510,
      author = {Dominik Klein},
      title = {Key-Secrecy of PACE with OTS/CafeOBJ},
      howpublished = {Cryptology ePrint Archive, Paper 2018/510},
      year = {2018},
      doi = {10.1007/978-3-319-17581-2_11},
      note = {\url{https://eprint.iacr.org/2018/510}},
      url = {https://eprint.iacr.org/2018/510}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.