|
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.
|
|