Verifpal, Rewritten in Rust

Today we’re releasing a complete rewrite of Verifpal in Rust. Every line of Go has been replaced. The result is a faster, more correct, and more capable protocol verifier — with a new analysis technique, a rich terminal interface, 147 tests (up from 67), and a binary that ships with zero runtime dependencies.

Verifpal 0.40.1 is an almost complete ground-up rearchitecture that fixes longstanding design limitations while introducing features that weren’t possible in the old codebase.

Why Rewrite?

Verifpal was first released in 2019, written in Go. Go served the project well for its first seven years — fast compilation, easy cross-platform builds, and a straightforward concurrency model. But as the analysis engine grew more sophisticated, Go’s limitations started to compound.

Parallel slices instead of structured data. The core PrincipalState type in Go maintained 18 separate parallel slices — Constants, Assigned, Creator, BeforeMutate, BeforeRewrite, KnownBy, DeclaredAt, Phase, and more — all correlated by index. Adding a new field meant updating every function that iterated over principal state. An off-by-one in any slice silently corrupted the analysis.

Interface boxing and runtime casts. Go’s Value type used an interface (ValueData) with three implementing types. Every operation required a type switch and cast: v.Data.(*Constant). The compiler couldn’t help you if you forgot a case or cast to the wrong type. The value.go file alone was 935 lines, much of it repetitive dispatch logic.

Global mutable state. The attacker’s knowledge base was a package-level global behind a sync.RWMutex. Every test run had to reinitialize it. Defensive snapshot copies on every read added allocation pressure in the hottest code paths.

No unit tests. The Go codebase had a single TestMain function that ran 67 integration tests. There were no unit tests for value equivalence, equation flattening, primitive rewriting, or any of the core symbolic operations. Bugs in these low-level functions only surfaced as incorrect results on full protocol models.

These weren’t insurmountable problems — plenty of good software is written in Go. But for a symbolic verification engine where correctness is paramount and the core data structures are recursive algebraic types, Rust is a natural fit.

What Changed

Algebraic Types All the Way Down

The new Value type is a Rust enum:

pub enum Value {
    Constant(Constant),
    Primitive(Arc<Primitive>),
    Equation(Arc<Equation>),
}

Pattern matching is exhaustive — the compiler rejects any function that forgets a variant. Accessor methods like try_as_constant() return Result<&Constant> instead of panicking, and errors propagate with ?. The 935-line value.go has been split into five focused modules: value.rs, equivalence.rs, hashing.rs, resolution.rs, and rewrite.rs.

Structured Principal State

The 18 parallel slices are gone. Each protocol constant is now a single SlotValues struct:

pub struct SlotValues {
    pub assigned: Value,
    pub before_rewrite: Value,
    pub before_mutate: Value,
    pub mutated: bool,
    pub rewritten: bool,
    pub creator: PrincipalId,
    pub sender: PrincipalId,
}

Immutable metadata (guard status, wire participation, phase membership) lives in a separate SlotMeta struct shared via Arc:

pub struct PrincipalState {
    pub meta: Arc<Vec<SlotMeta>>,       // shared, immutable
    pub values: Vec<SlotValues>,        // deep-cloned per attack stage
    pub index: Arc<HashMap<ValueId, usize>>,
}

When cloning state for a new attack stage, only values is deep-copied. The metadata and index increment an atomic reference count — an O(1) operation. This pattern eliminates an entire class of parallel-slice indexing bugs while reducing clone overhead.

Three-Valued Lifecycle

Every protocol constant tracks three snapshots of its value: before_mutate (original), before_rewrite (after attacker mutation but before primitive rewriting), and assigned (final). The resolution system uses a simple rule to decide which value a principal actually sees:

pub fn should_use_before_mutate(&self, i: usize) -> bool {
    self.values[i].creator == self.id
        || !self.meta[i].known
        || !self.meta[i].wire.contains(&self.id)
        || !self.values[i].mutated
}

When a principal created a value themselves, or when it wasn’t sent over the wire, or when the attacker hasn’t mutated it, the principal sees the original. This prevents false-positive authentication failures that plagued earlier versions — a subtle correctness issue that the structured data model makes explicit and verifiable.

Hand-Written Parser

The Go version used a PEG grammar (libpeg.peg) that generated parser code. The Rust version replaces it with a hand-written recursive descent parser operating directly on byte slices — zero allocations during lexing, better error messages with position context, and no build-time code generation dependency. The parser is 841 lines, self-contained, and easy to maintain.

Trait-Based Primitive Dispatch

The 21 built-in cryptographic primitives (AEAD_ENC, AEAD_DEC, SIGN, SIGNVERIF, HASH, HKDF, DH operations, PKE, blind signatures, Shamir secret sharing, and more) are defined as structured specs with function pointer dispatch:

pub struct PrimitiveSpec {
    pub name: &'static str,
    pub decompose: DecomposeRule,
    pub recompose: RecomposeRule,
    pub rewrite: RewriteRule,
    pub rebuild: RebuildRule,
    pub definition_check: bool,
    pub explosive: bool,
    pub password_hashing: Vec<usize>,
}

Each rule encodes the primitive’s cryptographic semantics declaratively. For example, AEAD_ENC’s decompose rule says: “given the key (argument 0), reveal the plaintext (argument 1); associated data (argument 2) is always publicly extractable.” The Go version encoded the same logic through scattered switch statements across multiple files.

The rewrite also cleanly separates two concepts that were previously conflated: definition check (an inherent property of the primitive — AEAD_DEC always requires the correct key) and instance check (set by the ? suffix in model syntax — this specific decryption operation is verified by the principal). This distinction is critical for correctly modeling protocols where some cryptographic operations are checked and others are blindly accepted.

No Globals, Explicit Context

All mutable verification state lives in a VerifyContext struct passed explicitly through the call stack. The only global mutable state in the entire codebase is a single AtomicU32 analysis counter used by the TUI — a pragmatic exception for a progress indicator that must be readable from a rendering thread without holding a reference to the verification context.

RwLock poison recovery (unwrap_or_else(|e| e.into_inner())) prevents cascading failures when a thread panics during testing, ensuring that one failing test doesn’t poison the lock for all subsequent tests running in parallel.

Equation Bypass: A New Attack Strategy

The most significant new feature isn’t about language or architecture — it’s a new analysis technique called Equation Bypass that finds attacks the Go version sometimes missed.

The Problem

Verifpal’s active attacker analysis works by systematically replacing wire values with attacker-controlled alternatives, then checking whether the attacker can derive secrets or forge messages. The search is staged: stage 1 tries single-value replacements, stage 2 tries pairs, and so on. For simple protocols, this works well.

But for protocols like Scuttlebutt, the brute-force search never terminates. The combinatorial space is too large, and the canonical attack — replacing an ephemeral DH public key with the attacker’s own — is buried in a haystack of useless mutations. The old Go verifier would run indefinitely on Scuttlebutt without ever finding the attack that any cryptographer would spot in minutes.

The Solution

Equation Bypass is a targeted analysis pass that runs before the general mutation loop. It directly models the most common class of active attack: replacing unguarded Diffie-Hellman public keys with the attacker’s own public key (G^nil, where nil is the attacker’s known private key).

The mechanism has four phases:

Replace. For each principal, collect all equation-valued wire inputs that are received from another principal and not guarded (not sent in [brackets]). Try replacing each one individually with G^nil, and also try replacing all of them simultaneously.

Identify bypassable guards. After replacement, resolve all values and attempt primitive rewrites. Guarded primitives (AEAD_DEC?, SIGNVERIF?) whose rewrite fails are collected. For each failed guard, extract the “bypass key” — the value the attacker would need to forge a valid input. For AEAD_DEC, that’s the decryption key. For SIGNVERIF with a public key G^sk, that’s the private key sk. If the attacker can obtain the bypass key — because it’s already known, or reconstructible from known values — the guard is bypassable.

Inject. For each bypassable guard, inject G^nil into the guard’s output slot. This injection must update all three state vectors (assigned, before_rewrite, and before_mutate) to ensure correct propagation through downstream computations. The injection iterates up to 5 times to handle cascading guards: bypassing one guard may change downstream keys enough to make a later guard bypassable.

Decompose. With the fully-resolved bypass state, attempt to decompose all wire-carried primitive values. For example, AEAD_ENC(key, plaintext, nil) where the attacker now knows the key yields the plaintext.

The Scuttlebutt Result

For Bob’s state in the Scuttlebutt protocol, replacing ephemeralAPub with G^nil causes a cascade:

1. Every shared secret Bob derives from Alice’s ephemeral key now uses G^nil — which the attacker knows.
2. The master secret derived from these shared secrets is reconstructible by the attacker.
3. The first AEAD_DEC guard fails, but the attacker knows the key — so G^nil is injected.
4. This propagates through the second AEAD_DEC guard, which also becomes bypassable.
5. The attacker decomposes both encrypted messages, learning m1 and m2.

All 9 security queries fail. The attack is found in seconds. The Go version would have run forever.

A Rich Terminal Interface

The Rust rewrite introduces a full-screen terminal user interface for live analysis visualization. When running with the --tui flag, Verifpal renders:

• A protocol overview showing principals, their private/generated/computed values, and message flows
• Live query status with pass/fail indicators updating in real time
• Attacker activity tracking: current scan target, mutation weight, budget consumption, and last worthwhile mutations
• Knowledge gain feed: newly deduced values color-coded by derivation method (decomposition, reconstruction, recomposition, equivalence, password guessing)
• Contextual narrative text describing the attacker’s actions in natural language

The TUI uses an alternate screen buffer, hides the cursor, detects terminal width, and throttles redraws to 20fps to avoid flooding the terminal. All rendering uses 1-cell-wide Unicode characters (box drawing, block elements) for correct alignment across terminal emulators.

Character Modes

Because formal verification should be fun: the --character flag lets you switch the attacker’s narrative voice. The default is a clinical security analyst. But you can also run analysis as Jevil or Spamton from Deltarune, complete with character-appropriate commentary on every phase of the attack:

Jevil (on deduction): “UEE HEE HEE! A SECRET FALLS INTO MY TINY HANDS!”

Spamton (on mutation): “HEY Alice!! WANT SOME [[Slightly Used]] REPLACEMENT VALUES?? ONLY 3 [[Kromer]]!!”

Spamton (on query failure): “[[DEAL OF A LIFETIME]]!! YOUR PROTOCOL IS [[Bankrupt]]!!”

Expanded Test Suite

The Go version had 67 integration tests and no unit tests. The Rust version has 147 tests: 70 unit tests covering value equivalence, equation flattening, primitive handling, and other core operations, plus 77 integration tests running full protocol models.

Fifteen new protocol models were added, covering scenarios the old test suite never touched:

• Double Ratchet (double_ratchet.vp): Signal-style DH ratcheting with alternating rounds and HKDF chain key derivation
• Triple DH (triple_dh.vp): X3DH-style key agreement combining identity, signed, and ephemeral DH computations
• Four-Party Relay (four_party.vp): Multi-hop message relay with cross-principal authentication and re-encryption
• Phase Forward Secrecy (phase_forward_secrecy.vp): Ephemeral DH ensuring confidentiality survives long-term key compromise
• PSK + DH (psk_with_dh.vp): TLS PSK+DHE-style hybrid key agreement with forward secrecy under PSK compromise
• Key Ratchet (key_ratchet.vp): Symmetric HKDF chain key ratcheting across multiple messages
• Shamir Reconstruction (shamir_reconstruction.vp): 2-of-3 threshold secret sharing with partial share leakage
• Blind Signature (blind_signature.vp): Message blinding, blind signing, and signature unblinding
• Deep Nesting (deep_nesting.vp): Five layers of nested encryption testing value resolution depth
• Concat Bomb variants: Maximum-arity concatenation testing decomposition, equivalence, key leakage, and unchecked assertions
• Many Principals (many_principals.vp): Broadcast signature verification across six recipients
• Passive DH Chain (passive_dh_chain.vp): Three-hop relay testing chain-of-custody under passive attackers

These models test real-world protocol patterns — ratcheting, multi-party flows, threshold cryptography, hybrid key agreement — that represent the bread and butter of modern protocol design.

By the Numbers

The Rust binary ships with fat link-time optimization, a single codegen unit, symbol stripping, and panic=abort — producing a compact, fully static binary with no runtime dependencies.

Getting Verifpal

Verifpal is available now:

• Homebrew (Linux/macOS): brew install verifpal
• Scoop (Windows): scoop install verifpal
• Source: cargo build --release from the GitHub repository
• Releases: Pre-built binaries for Windows, Linux, macOS, and FreeBSD on GitHub Releases

The Verifpal User Manual and the VS Code extension (syntax highlighting, live analysis, diagram visualizations) remain fully compatible with the Rust version.

This rewrite represents weeks of careful work. Every test passes. Every protocol model produces identical results to the Go version (plus the new ones the Go version couldn’t handle). The codebase is smaller in spirit if not in line count — structured, typed, and tested in ways that weren’t possible before.