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.