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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.