JAIST Logic@JAIST

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

  • Dominik Klein
  • Federal Office for Information Security, Germany
Date: 2015/05/26 (Tue) 13:30 to 15:00
Place: Room B, Tokyo Satellite, JAIST
Group: Research Center for Software Verification
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.
Contact nao-aoki