Key-Secrecy of PACE with OTS/CafeOBJ

Dominik Klein

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 cards protocol verification Security Protocol
Contact author(s): dominik klein @ bsi bund de
History: 2018-05-26: received
Short URL: https://ia.cr/2018/510
License: 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},
      url = {https://eprint.iacr.org/2018/510}
}