Cryptographic protocols form the backbone of modern digital infrastructure. Designing them is difficult and flaws are costly, yet their complexity is outpacing our ability to analyze them rigorously.

Cryptographers have developed mathematical frameworks for modeling protocols and proving them secure. Yet how best to model a protocol, capture adversarial behavior, and state its guarantees remain active foundational questions. Pen-and-paper proofs can precisely quantify security, but they remain unwieldy and error-prone, especially when analyzing protocols of real-world dimension. Formal verification, meanwhile, offers higher assurance and handles more complex and more realistic specifications, but tools either do not yet scale to full protocol verification or reach it only in idealized security models. How those models relate to the ones used on paper is itself poorly understood.

This Dagstuhl Seminar brings together researchers who write game-based, simulation-based, and composition-based security proofs, on paper and with machine support alike, with researchers developing tools and techniques for program verification. Both communities are ultimately after the same thing—formalizing systems and proving properties about them—and differ in method, in standards of rigor, and in culture rather than in aim. Together, we will assess where each tradition stands, examine the shortcomings of each in its own terms and in relation to the others, and look for bridges between them. We are as interested in what a verification technique can offer a proof that will never be mechanized, as in what a pen-and-paper insight can offer a tool. We begin by building common ground: overview talks in which each community explains to the others what its methods do, what they assume, and what they cost. Building on that common ground, the rest of the week is organized around three questions, which we expect participants to reshape and add to.

Modeling protocols and stating guarantees. Turing-machine models connect directly to complexity theory but sit too low-level for proofs to be carried out in full; pseudocode and games suit primitives but strain under concurrent, multi-party message flow; symbolic formalisms excel at interaction and automation but abstract probability and cost away. Where one protocol has been analyzed in several formalisms, do the guarantees differ essentially, or only as artifacts of the modeling? And what happens to the security guarantees when a system consists of components analyzed in different formalisms?

Precise reasoning at scale. Compositionality is what makes analysis at scale possible. Unfortunately, shared state such as setup assumptions, long-lived keys, and state carried across protocol sessions seems to break it again: These cases are exactly what composition theorems currently exclude or handle by hand. Much of the proliferation of frameworks (global setup, joint state, state separation) are answers to this difficulty. Program verification has faced the same tension for decades and has answers of its own: ownership, invariants, rely-guarantee. Do they transfer, and if not, what is different about cryptography?

Supporting the proof process. Producing a proof for a realistic protocol is laborious either way: Mechanizing one takes person-years and is out of reach for many protocols. Meanwhile pen-and-paper practice maintains large collections of games and descriptions by hand. What machinery could sharpen the arguments on paper, whether or not it is ever mechanized? Could one imagine lightweight tools that support the protocol development process, e.g., code management or type checking? Could such tools serve as a stepping stone into heavier-weight verification? How would a layered ecosystem that spans pen-and-paper approaches to lightweight tools to full mechanization look like?

We do not expect the seminar to fully settle these questions. What we hope to leave with is a shared vocabulary, a clearer sense of which problems are genuinely open and which are artifacts of how we work, and a roadmap concrete enough to act on afterwards.

Creative Commons BY 4.0

Simon Oddershede Gregersen, Sabine Oechsner, Douglas Stebila, and Pierre-Yves Strub

This seminar qualifies for Dagstuhl's LZI Junior Researchers program. Schloss Dagstuhl wishes to enable the participation of junior scientists with a specialisation fitting for this Dagstuhl Seminar, even if they are not on the radar of the organizers. Applications by outstanding junior scientists are possible until October 23, 2026.