A sound translation from Tamarin to ProVerif is presented that enables a rigorous comparison of the two tools and introduces techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, supporting a large subset of Tamarin's features, including multiset rewrite rules, lemmas, and restrictions.
Abstract
Tamarin and ProVerif are two prominent tools for the formal verification of security protocols. They share the same high-level goal but differ significantly in their underlying formalisms and verification techniques, making a systematic comparison challenging: Tamarin uses multiset rewrite rules with sound and complete verification, whereas ProVerif employs an extension of the applied-pi calculus that provides fast but potentially incomplete results. We present a sound translation from Tamarin to ProVerif that enables a rigorous comparison of the two tools. It introduces techniques for formula rewriting, encoding multiset rewrite semantics, and handling simultaneous events, supporting a large subset of Tamarin's features, including multiset rewrite rules, lemmas, and restrictions, while precisely characterizing the cases where faithful translation is not possible. We provide formal proofs: within the faithful fragment, soundness ensures that any property verified in ProVerif also holds in the original Tamarin model, and completeness ensures that exists-trace properties not involving attacker knowledge are preserved. Best-effort encodings, in particular XOR, are reported separately and are outside these guarantees. Finally, we evaluate our translation on 121 Tamarin models. The ProVerif front end accepts executable translations for 523 of 566 lemma tasks. Among non-XOR tasks with definitive results from both tools, 237 of 238 agree, with the remaining verdict explicitly flagged as using an incomplete model. Among the 344 tasks for which Tamarin returns a Boolean result and ProVerif completes with a logical result, ProVerif is faster in 316 cases (91.9%), with median per-task runtime and peak-memory ratios of 6.74x and 6.13x, respectively.
Pistis is introduced, an agentic, oracle-guided proof search that produces formal Lean proofs that satisfy faithfulness conditions and can accept or refute natural language proofs written by humans or AI, demonstrating that faithful formalization is useful as a proof-checking tool.
Tadd Mao, Tianjun Zhong, Dhruva Arekar et al.· 1 citation
Security protocols are concurrent processes that communicate using cryptography to achieve various security properties. Their formal verification has been the subject of much research, which has led to a number of successful tools. Several of these tools use variants of the applied pi-calculus as an input language to model protocols, though the internal representation used for verification may vary. The translation from processes to their internal representation has received relatively little attention despite its important role in the soundness and efficiency of the security analyses. We consider this problem within the Squirrel prover framework, where processes are translated to so-called systems of actions, which serve as the basis for a logic-based verification technique. Intuitively, actions consist of groups of elementary instructions. We provide a general theory for grouping instructions in a way that preserves both indistinguishability and trace properties, and we instantiate it to obtain a new translation procedure for Squirrel. We have implemented our procedure as a replacement of the original (unsound) translation, demonstrating that it can serve as an almost drop-in replacement in existing case studies.
David Baelde, Stéphanie Delaune, Julia Gabet et al.· IEEE Computer Security Found...· 0 citations
The key idea is to implement an entailment checker as a combination of an efficient but unverified prover, suitable for fast-paced interactive proofs, and a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori.
V. Mikhal'chuk, V. Gladshtein, I. Sergey· International Conference on...· 0 citations
SymCert is presented, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies that provide a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterex-ample extractor for proving analysis completeness.
This paper provides a formal account of the syntax and semantics of Hedgehog, a popular PBT framework, and proves that Hedgehog→ possesses a compositional distribution semantics, and introduces Hedgehog→, a restricted version of the language based on the arrow calculus, and proves that Hedgehog→ possesses a compositional distribution semantics.
Anthony Vandikas, Kiarash Sotoudeh, Marsha Chechik· Proc. ACM Program. Lang.· 0 citations
Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification. As such, weak specifications and redundant invariants may create overconfidence in ``verified''code. We present \proofpulse, a tool for Dafny that diagnoses specification quality using a three-valued proof coverage model. By analyzing proof dependencies, ProofPulse distinguishes between elements that contribute to specification intent, those used only for auxiliary checks, and those irrelevant to any proof obligation. Evaluated against an oracle of 252 programs from the dafny-synthesis benchmark, ProofPulse provides a high-precision signal for specification weaknesses, particularly unnecessary preconditions and vacuous proofs. With unsat-core minimization, ProofPulse achieves perfect precision for precondition classification and reduces false positives across all evaluated categories. These results show that proof coverage is a practical complement to verification. Although it cannot fully capture semantic intent, it can reveal weak proof coupling in programs that otherwise appear fully verified. Just as a pulse check distinguishes vitality from the mere absence of symptoms, ProofPulse exposes weaknesses in proofs that technically verify successfully but still suffer from inadequate or redundant code and specifications.
Álvaro F. Silva, Ruben Martins, Alexandra Mendes· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
