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. It then runs every session and peer configuration of the protocol together as one execution under those actions, in which each injected value must be derivable from what that same execution has already disclosed, and evaluates the query on that execution. We specify this process from the term algebra and primitive registry through knowledge deduction, bounded sessions, peer configurations, execution, and counterexample presentation. We also give a single-history reference semantics, prove that every execution the engine judges is a history of that semantics, 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: every reported attack is an explicit protocol execution, but a passing query is not an unbounded proof, and no report is a machine-checked certificate.