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.