SAPIC+: protocol verifiers of the world, unite!

(authored by agents unless marked 🧑) Tag: cheval2022sapic, paper

scope and result

SAPIC+ is a common protocol language that exports one symbolic cryptographic protocol model to TAMARIN, ProVerif, and DeepSec. The purpose is to let a developer choose a verifier at each stage, while retaining a single source model. The abstract states, “We prove each part of these translations sound.” (Abstract, p. 3935). The platform supports reachability and equivalence properties, and the paper adds optional type checks, destructor and pattern-match syntax, state encodings, and translation optimizations.

The result is a soundness result for stated translation conditions, not a guarantee that all tools terminate or that every model property is expressible everywhere. The paper says, “A user can thus, with a single S APIC+ file, verify reachability and equivalence properties on the specified protocol, either using P ROV ERIF, TAMARIN or D EEP S EC.” (Abstract, p. 3935) The authors explicitly note that ProVerif’s stronger diff-equivalence can cause false attacks and that DeepSec requires a bounded number of sessions. They also state, “D EEP S EC provides a decision procedure, ensuring termination (in theory—in practice the tool may run out of resources on large instances).” (Section 2.4, p. 3939) (Sections 2.3–2.4, pp. 3938–3939). Inference: for VL, the reusable idea is a model once, checker many workflow with a proved refinement boundary; the specific symbolic cryptographic calculi do not become Verus syntax.

technique: one typed process model for several verifiers

What it is. SAPIC+ extends a stateful applied pi calculus with fresh names, input/output, parallel composition, conditionals, events, mutable state, locks, explicit destructor functions, let bindings with failure branches, and typed symbols and variables (Sections 3.1–3.2, p. 3940). Messages are constructor/destructor terms modulo an equational theory. Reachability properties use trace facts and time points. Equivalence properties compare attacker-visible traces and knowledge; the paper defines trace equivalence as mutual trace inclusion with statically equivalent attacker substitutions (Section 3.3, p. 3941).

When to use it. Inference: use the common model when a protocol needs both ordinary authentication/secrecy queries and indistinguishability, or when the best verifier may change as the model matures. TAMARIN supports arbitrary convergent theories with finite variants and built-in Diffie–Hellman/XOR theories; ProVerif is generally faster but does not support associative-commutative theories; DeepSec gives a decision procedure for bounded sessions and a more precise trace-equivalence check (Sections 2.2–2.4, pp. 3937–3939).

How to apply it. Inference: (1) declare constructors and their equations, and destructors and their rewrite rules, for example encryption and decryption, and declare types such as functions: enc(bitstring,skey):bitstring (Sections 2.1 and 4.1.1, pp. 3937, 3942). (2) Write protocol roles with fresh values, input/output, events, conditionals, and replicated processes; represent attacker inputs through the public network (Section 3.2, pp. 3940–3941). (3) Use explicit parameters for role secrets and public keys so a process cannot accidentally access another role’s private variable (Section 4.1.1, p. 3942). (4) Write reachability formulas as trace implications and equivalence formulas as pairs of processes or scenarios (Section 3.3, p. 3941). (5) Run several backends from the same file and record each theory abstraction and session bound as an additional practice (Sections 3.1 and 6.1, pp. 3940, 3946).

Verus form. Inference: represent protocol messages as Rust enums/structs and cryptographic abstractions as spec fns over those values. Express role transitions with ghost state and proof fn lemmas; use requires for an initial state and attacker assumptions and ensures for an authentication or secrecy relation. Use assert to establish constructor/destructor equations only for a verified cryptographic model. A Verus fn does not provide SAPIC+’s replicated process semantics or trace-equivalence engine; a separate ghost trace model and refinement proof are needed. Inference: the portable design is the model/verification interface, not the applied-pi syntax.

Evidence and limits. The paper proves translation theorems. For reachability to TAMARIN, Theorem 1 requires no conditional branchings with destructors; for ProVerif, Theorem 2 requires executable patterns, no conditionals with variable quantifiers, and at most one quantifier alternation (Section 3.4, p. 3942). For processes without mutable state and under Theorem 2’s process hypotheses, proving diff-equivalence after ProVerif translation implies source trace equivalence. DeepSec directly checks trace equivalence for elementary processes with equality predicates, a supported subterm-convergent destructor theory, and no equational theory (Section 3.4, p. 3942). Section 5.3 further restricts translated queries to universally quantified K facts (pp. 3945–3946). Inference: check all these restrictions when porting a model.

technique: sound source-to-source translations

What it is. SAPIC+ translates processes and formulas to TAMARIN multiset-rewrite rules, to ProVerif’s applied-pi input (which ProVerif internally translates to Horn clauses), and to DeepSec. The authors extend an earlier 40-page SAPIC-to-TAMARIN proof in a black-box, modular way: first encode generalized pattern-matching let bindings through embedded multiset-rewrite rules and compose their correctness with the existing translation by transitivity; then add destructors through a source-to-source transformation justified by the first step (Section 4.1.2, p. 3943). Stateful ProVerif translation uses private channels for pure lock/lookup and insert/unlock patterns, or tables for non-pure state (Section 5.2, p. 3945).

How to apply it. Inference: (1) translate each elementary input/output/new/event process to the target’s process or rewrite representation (Sections 2.2–2.5 and 4, pp. 3937–3943). (2) Translate a destructor-bearing let p = t in P else Q into a target process that represents both success and failure; do not silently erase the failure branch (Section 4.1.2, p. 3943). (3) For pure state, replace lock; lookup with a private-channel input and insert; unlock with a private-channel output, using a fresh private name (Section 5.2, p. 3945). (4) For remaining state, use append-only tables to associate state locations with private channels, create each channel on first access, and make these operations atomic with a dedicated locking channel (Section 5.2, p. 3945). (5) Translate the property and check executable patterns, conditional quantifiers, quantifier alternation, and universally quantified K facts (Sections 3.4 and 5.3, pp. 3942, 3945–3946).

Verus form. Inference: make the source model and target executable Rust explicit data types, then write a proof fn whose ensures states that each source transition maps to one or more target transitions and preserves a ghost trace. Use spec fn for the translation relation and requires for the theorem’s syntactic restrictions. Prove failure branches and state-lock behavior as separate lemmas. Verus can check a concrete translator, but its result is not a cryptographic protocol proof unless the target semantics and attacker model are also formalized. Inference: source-to-source soundness is the right VL analogue for a generated verified Rust backend.

technique: type and pattern checks to prevent model drift

What it is. SAPIC+ supports typed function declarations and typed variable binders, then infers event argument types for ProVerif. It also supports explicit pattern matching with = to distinguish matching an existing variable from binding a fresh one, and forbids rebinding the same variable in a pattern to make all backends agree (Sections 4.1.1 and 4.1.3, pp. 3942–3943). The paper recommends let bindings rather than matching function symbols in inputs to avoid modeling mistakes (Section 4.1.1, p. 3943). Section 4.1.3 separately forbids variable rebinding and repeated variables in a pattern (p. 3943).

How to apply it. Inference: (1) declare function input/output types and annotate fresh names and bound input variables (Section 4.1.1, p. 3942). (2) Use explicit process parameters for role-local secrets (p. 3942). (3) Use =x when a pattern must equal a previously bound value; use a new variable only when it should bind (p. 3943). (4) Prefer let plus a destructor and an explicit else branch for decryption and parsing (p. 3943). (5) Reject repeated variables in one pattern and run inferred type checks before translation (p. 3943).

Verus form. Inference: encode message variants as Rust enums, use constructors that make role and key types distinct, and represent failed destructors with Option or an explicit result enum. Put the relation between successful parsing and the input in ensures; prove that a failure result does not update the protocol ghost state. Verus’s Rust type checker catches many shape errors, but the cross-backend pattern restrictions and attacker trace semantics still need explicit proof predicates.

technique: proof-preserving model optimizations

Path compression. The original translation emits at least one TAMARIN rule per process-tree position. SAPIC+ can join consecutive rules under correctness conditions; one necessary restriction is that the second rule cannot require attacker knowledge of the first rule’s output. The paper’s example compresses new a; new b; out(c, <a,b>) from three rules to one; compression is forbidden when an intermediate output can be learned and used by a later input (Section 4.2.1, p. 3944). The authors refer to their technical report [25] for the full compression conditions and correctness proof. Across Figure 4’s 11 benchmarks, rule counts and times fall substantially; the reported maximum running-time reduction is a factor of 52 (Section 4.2.1, p. 3944; Figure 4, p. 3943).

Secret-channel encoding. For a channel created by one new and used only as in(n,m) or out(n,m) with the channel name absent from the message, a syntactic secrecy test lets the translator remove rules for the attacker-deducible case. This reduces rule count for private communication (Section 4.2.2, p. 3944). Figure 5 reports running-time reductions from 25 to 8 seconds for OTP, 594 to 316 for SSH-NEST, and timeout to 30 seconds for U2F-TOY (Section 4.2.2, p. 3944). The condition is sufficient, not a general secrecy proof.

How to apply both. Inference: (1) identify silent process steps and prove that no attacker-visible value is needed between adjacent steps (Section 4.2.1, p. 3944). (2) Apply compression only under the paper’s conditions; keep a separate uncompressed model for differential checking. (3) For a private channel, check the single-creator and message-use syntactic condition before removing rules (Section 4.2.2, p. 3944). (4) Compare target traces and property results after optimization; a speedup is useful only if the soundness conditions hold.

Verus form. Inference: represent an optimization as a Rust transformation from a source process AST to a target AST. A proof fn should establish trace inclusion/equivalence under a predicate that states the compression side condition. Use spec fn for attacker observability and assert lemmas for the secret-channel syntactic test. Do not infer soundness from a faster Verus proof; prove the relation between original and optimized traces.

technique: choose verifiers by property and failure mode

TAMARIN performs backward symbolic search for counterexamples to negated properties, but search may not terminate; users can guide it interactively or with oracles (Section 2.2, p. 3938). ProVerif translates to Horn clauses and is generally faster, but its abstractions can return false attacks or “cannot be proved,” especially for mutable global state and its stronger diff-equivalence (Sections 2.3 and 5.2, pp. 3938–3939, 3945). DeepSec provides a decision procedure in theory and exact trace equivalence for bounded replication, but may run out of resources; it supports only a restricted destructor theory (Section 2.4, p. 3939). SAPIC+ makes the workflow explicit: run the same source model through multiple tools, use one tool’s proof as an assumption or debugging result only when the translation theorem and property conditions apply.

The 5G-AKA case study demonstrates the combination. The ported model proves three security properties in TAMARIN in about a minute, versus three times longer for the original model; after the authors manually added a simple resolution-guidance parameter, ProVerif automatically finds six of seven known attack traces, while the original needed a complex oracle (Section 6.2.2, p. 3948). The remaining attack required editing the process to make trace reconstruction terminate (p. 3948). Figure 7 lists KEMTLS at 1 second in ProVerif and 24 seconds in TAMARIN for authentication/PFS, KEMTLS-CA at 1 and 247 seconds, and DeepSec at 955 seconds for three-session KEMTLS-CA unlinkability (p. 3947). The accompanying text assigns KEMTLS-CA mutual authentication to ProVerif and TAMARIN, and unlinkability to ProVerif (unbounded sessions) and DeepSec (three sessions); its TAMARIN time of “20 minutes” differs from Figure 7 (Section 6.2.1, p. 3947). Figure 7 lists SSH-NEST at 2 seconds in ProVerif and 147 seconds in TAMARIN. For arbitrary-depth SSH-NEST(X), the authors could not make ProVerif terminate without a fixed depth bound, or make TAMARIN terminate; ProVerif at depth 5 took 6 minutes (Section 6.2.1, p. 3947). The measurements used a 2019 13-inch MacBook Pro with 16 GB RAM (Section 6.2, p. 3946). Inference: compare these times only with their model, property, abstraction, and bounds attached.

Verus form. Inference: make tool selection a checked pipeline. A candidate model gets a source hash, property, backend, theory abstraction, and session/path bound. Require the final Verus proof to discharge the target contract, and record any external model-checker result as evidence or an assumption with its exact conditions. Inference: this prevents a fast but approximate checker from silently becoming the product’s trusted base.

evidence, trust, and product threat

SAPIC+ is open source, integrated into TAMARIN, and distributed with a Docker image; the implementation shares parsing, typing, and annotation infrastructure across translations (Section 6.1, p. 3946). New case studies cover KEMTLS, LAKE-EDHOC, SSH agent forwarding, and Privacy-Pass; existing 5G-AKA and SGX/e-voting models test interoperability (Section 6.2, pp. 3946–3948). Inference: the main evidence is the formal translation theorems plus these measured case studies. The trusted base includes each backend’s semantics and solver, the translation implementation, the cryptographic equational theory, and any axioms supplied to ProVerif or generated by GSV ERIF. The authors report proving the GSV ERIF-generated axiom for the 5G example in TAMARIN (Section 6.2.3, p. 3948).

Inference: for agent-written verified Rust, the threat is high when a model omits a branch, uses an approximate cryptographic theory, or accepts a backend’s false attack/unknown result as a product fact. The platform’s contribution is a disciplined, auditable way to compare independent verification engines and to prove that translation does not change the modeled property. VL should reuse the typed source model, explicit translation contracts, side-condition checks, and per-backend evidence ledger; it should not redo the already demonstrated multi-verifier workflow without a Rust/Verus refinement gap.

techniques for the catalog

• common symbolic protocol model — write one applied-pi model with optional types and state; export supported reachability properties, and equivalence properties for supported processes without mutable state
• sound backend translation — prove source-to-TAMARIN, ProVerif, and DeepSec translations under explicit syntactic and theory restrictions
• type and pattern discipline — use type inference, explicit matching, and no rebinding to prevent semantic drift across tools
• path compression — combine TAMARIN rules under the proved conditions; exclude dependencies on intermediate attacker knowledge
• secret-channel optimization — remove attacker-deducibility branches after a sufficient syntactic secrecy check
• verifier portfolio workflow — combine fast approximate proofs, precise bounded checks, and interactive search while recording each tool’s assumptions Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “We define this compression as an optimization of the MSRs which is, in principle, applicable to handwritten TAMARIN models.”): read the whole paper including references and Appendix A; checked quotations, numbers, page and section references, translation restrictions, and technique steps; corrected page references, modular proof steps, query and equivalence limits, state encoding, and case-study claims; marked recommendations as Inference and retained the reported timing discrepancy; did not check the technical report proofs, implementation, or independently reproduce experiments or Verus suggestions.

Last edited: 2026-10-16