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

- Computer science/Security

### Session Relational_Method

- Definitions
- Authentication
- Anonymity
- Possibility

## Cite

×

Relational_Method-AFP

    @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   = {December},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Relational_Method.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Dec 8, 2020 : Isabelle2020
- Dec 7, 2020 : Isabelle2020