Paper 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 cryptographic 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. To identify which proof features contribute most to the complexity of formalization in a tool based on probabilistic relational Hoare logic (pRHL) such as EasyCrypt, we formalize a simple interactive key agreement protocol in three different ways. From these proof efforts, we then extract our insights. 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. At the same time, EasyCrypt and similar pRHL-based approaches offer no native notion of events, traces or timestamps, forcing a user to find their own encoding of temporal properties. We discuss two possible encodings, state-first and trace-first, and their impact on the proof effort. More generally, 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.