The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols

Pasquale Noce 📧

December 5, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This paper introduces a new method for the formal verification of cryptographic protocols, the relational method, derived from Paulson's inductive method by means of some enhancements aimed at streamlining formal definitions and proofs, specially for protocols using public key cryptography. Moreover, this paper proposes a method to formalize a further security property, message anonymity, in addition to message confidentiality and authenticity. The relational method, including message anonymity, is then applied to the verification of a sample authentication protocol, comprising Password Authenticated Connection Establishment (PACE) with Chip Authentication Mapping followed by the explicit verification of an additional password over the PACE secure channel.

License

BSD License

Topics

Session Relational_Method