Paper 2026/1654

From Toy to Instrument: Seven Years of Verifpal

Abstract

Verifpal is a symbolic protocol analyzer introduced in 2019 to make formal analysis accessible during protocol design. It provides a small modeling language, built-in cryptographic primitives, and attack reports that use the model's names. This paper describes the analysis engine of Verifpal 1.6.7. A backward solver proposes attacker actions, which an executor checks by running all sessions and peer configurations together. An injected value is delivered only when the attacker can derive it from information already available in that execution. A separate query evaluator, or judge, records the result. We define the model, its five query predicates, and a reference semantics, and prove that every judged execution is a history of that semantics. Executions terminate; search termination is conditional on the solver calls terminating. Evaluation covers 885 secrecy queries across 189 configurations of the fifteen fundamental Noise patterns, varying static-key compromise and protocol checks. At one and two sessions, a separate executor reproduces every reported disclosure, and ProVerif proves all 290 passing counterparts for unbounded sessions. The protocol computations also match 90 external cryptographic test-vector messages. These results support the implementation on the tested models; a Verifpal pass remains the outcome of bounded, incomplete search.