Formal analysis of a security protocol for e-passports based on rewrite theory specifications

We report on a case study in which Password Authentication Connection Establishment (PACE) protocol has been formally analyzed based on its rewrite theory specification with Maude, a rewriting logic-based computer language and system. Dominik Klein has formally verified with interactive theorem proving that PACE enjoys the key secrecy property under the condition that the password shared by a passport chip C and a terminal T would be never leaked to the third party. In contrast, our analysis supposes that the password is leaked to an intruder once it has been used in a session completed. Under the condition, the analysis unveils some security weakness that PACE does not enjoy the correspondence (or authentication or agreement) properties from both C and T points of view. Then, we propose that one-time password is used in PACE. We have formally analyzed that the revised version enjoys the correspondence properties under the latter condition. We have used the Maude search command that can be used to conduct reachability analysis because the correspondence properties can be formalized as invariant properties.