Verification of Real-World Security Protocols in CafeOBJ: A Case Study of PACE


Dominik Klein
Federal Office for Information Security, Germany


JAIST Tokyo Satellite Campus Shinagawa, Room B
2015/02/26 (Thu) 15:00 to 17:00


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. Experience and learned lessons are discussed, and the approach is compared with competing approaches.

Leave a comment

Your email address will not be published. Required fields are marked *