Principles for pRHL Proofs of Cryptographic Protocols: How to Convince EasyCrypt that your Protocol is Secure

Manuel Barbosa; François Dupressoir; Cameron Low; Charlotte Mylog; Sabine Oechsner; Théo Vignon

Paper 2026/1334

Principles for pRHL Proofs of Cryptographic Protocols: How to Convince EasyCrypt that your Protocol is Secure

Manuel Barbosa

, University of Porto, INESC TEC

François Dupressoir

, University of Bristol

Cameron Low

, University of Bristol

Charlotte Mylog

, Norwegian University of Science and Technology

Sabine Oechsner

, Vrije Universiteit Amsterdam

Théo Vignon, École Normale Supérieure Paris-Saclay, University of Porto

Abstract

The EasyCrypt proof assistant has been used to successfully formalize security proofs for a wide variety of crypto- graphic primitives. However, attempts at formalizing objects with interactivity, such as protocols, have fared much worse. In this paper, we investigate (some of) the reasons for this difficulty by formalizing a simple interactive key agreement protocol. From a first complete but exploratory proof, to a failed attempt at a structured proof, and to what we believe is an “essential” proof, we identify which proof features contribute most to the complexity of formalization in pRHL. In particular, we argue that difficulties in formalizing the security of interactive protocols in the computational model arise from the fact that such proofs rely on both state and temporal invariants—the former to support cryptographic reasoning, and the latter to support reasoning about the protocol’s structure. We believe that this observation can help build new reasoning tools that can bridge the gap that currently exists between primitive-focused tools and protocol- focused tools.

Metadata

Available format(s): PDF
Category: Cryptographic protocols
Publication info: Preprint.
Keywords: Key Exchange Machine-checked Proofs EasyCrypt Game-playing State-separating
Contact author(s): mbb @ fc up pt
f dupressoir @ bristol ac uk
cameron low 2018 @ bristol ac uk
charlotte mylog @ ntnu no
s a oechsner @ vu nl
theo vignon @ lmf cnrs fr
History: 2026-06-30: approved; 2026-06-29: received; See all versions
Short URL: https://ia.cr/2026/1334
License: CC BY

BibTeX

@misc{cryptoeprint:2026/1334,
      author = {Manuel Barbosa and François Dupressoir and Cameron Low and Charlotte Mylog and Sabine Oechsner and Théo Vignon},
      title = {Principles for {pRHL} Proofs of Cryptographic Protocols: How to Convince {EasyCrypt} that your Protocol is Secure},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/1334},
      year = {2026},
      url = {https://eprint.iacr.org/2026/1334}
}