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

 

Title: The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
Author: Pasquale Noce (pasquale /dot/ noce /dot/ lavoro /at/ gmail /dot/ com)
Submission date: 2020-12-05
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.
BibTeX:
@article{Relational_Method-AFP,
  author  = {Pasquale Noce},
  title   = {The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2020,
  note    = {\url{https://isa-afp.org/entries/Relational_Method.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License