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


Lecturer

Dominik Klein
Federal Office for Information Security, Germany

Place/Time

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

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

Leave a comment

Your email address will not be published.