Paper 2026/1654

From Toy to Instrument: Seven Years of Verifpal

Abstract

Symbolic protocol verifiers must make a difficult tradeoff: their models and counterexamples should be accessible to protocol designers, but their results must still have a precise meaning. Verifpal addresses the first goal with a compact modeling language and source-level attack explanations. Its original analysis engine, introduced in 2019, had only a preliminary account of its guarantees. This paper presents and evaluates the replacement engine. The engine searches backward from a violated security query to candidate attacker actions. A separate validator then checks whether the attacker can perform those actions, re-executes the affected roles, and evaluates the query. We specify this process from the term algebra and primitive registry through knowledge deduction, bounded sessions, peer configurations, validation, and counterexample presentation. We also give a single-history reference semantics, relate it to the implemented replay system, prove termination under the engine's search bounds, and state exactly what each result category establishes. Our evaluation combines targeted regression models, mutation analysis, corpus measurements, and comparisons with ProVerif, Tamarin, and Scyther. It shows that the engine can express and find attacks that require several sessions, different peer assignments, or staged compromise, while exposing the implementation choices that limit its search. The result is an auditable account of Verifpal as a bounded counterexample finder: useful for finding and explaining protocol flaws, but not a substitute for an unbounded proof or a certified attack trace.