Cryptology ePrint Archive: Report 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.

Category / Keywords: cryptographic protocols / smart cards, protocol verification, Security Protocol

Original Publication (in the same form): FTSCS 2014: Formal Techniques for Safety-Critical Systems pp 159-173

Date: received 25 May 2018

Contact author: dominik klein at bsi bund de

Available format(s): PDF | BibTeX Citation

Version: 20180526:143311 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]