Paper 2026/1334 Original: eprint.iacr.org/2026/1334 ↗

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

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.