Verifpal 0.51.0: Sharper Semantics for Passwords, Assertions, and AEAD

Verifpal 0.51.0 is out. Where 0.50.0 was a deep architectural redesign of the analysis engine, 0.51.0 is a short, correctness-focused release: three semantic fixes, one UI fix, and a few new models — all driven by bug reports filed against the 0.50.0 series. None of the changes affect the Verifpal modeling language. Every existing model still parses, still runs, and produces results that are at worst the same and in several cases strictly more accurate.

Thanks to Cédric Picard (@cym13) for issues #11, #12, and #13, and to @EFCCWEB3 for issue #10. This release exists because of them.

Passwords: From Static Tables to Verifiable Guesses

The largest change in 0.51.0 is a rewrite of how Verifpal reasons about password-qualified values. Passwords occupy a strange place in the Verifpal model: they are secrets, but they are low-entropy secrets, so the attacker is assumed to be able to brute-force them if and only if the attacker has a way to verify guesses. Getting that “if and only if” right turns out to be subtle.

What Was Wrong

Before 0.51.0, password protection was defined by a static password_hashing field on each primitive’s spec — a list of argument positions at which passwords were considered cryptographically protected. For ENC, that list was vec![1]: the plaintext is protected, the key is not.

This captures the common case — if you encrypt a password with a known key, the attacker can brute-force it — but it fails on compositions. Consider:

principal Alice[
    knows private key
    knows public  data
    knows password pwd_2

    msg2 = ENC(key, CONCAT(pwd_2, data))
]

In 0.50.0, a passive confidentiality query on pwd_2 would fail. The password sits inside CONCAT, which has no password_hashing list of its own, so the engine treated the password as “unprotected” and assumed the attacker could brute-force it — even though the attacker does not know key and therefore has no way to verify a guess. This was Cédric’s issue #11.

The same shape arose elsewhere: ENC(secret, pwd), MAC(secret, pwd), AEAD_ENC(pwd, secret, pubdata), BLIND(secret, pwd), SIGN(pwd, secret). Each one has a different “right answer” depending on whether the attacker actually has enough of the surrounding context to mount an offline dictionary attack. A flat static table cannot express that.

The New Model

0.51.0 replaces the table with a dynamic, position-sensitive check. A password-qualified value at position i of primitive P(a₀, …, aₙ) is obtainable by the attacker only when both of the following hold at every primitive level in the nesting chain:

1. No inherent protection. Position i is not listed in P.password_hashing. This field is now reserved exclusively for primitives that resist brute-force by construction (only PW_HASH qualifies — it is expensive by design). Every other primitive loses its static entry.

2. Verifiable guess. The attacker knows every sibling argument aⱼ (j ≠ i), which is what it takes to reconstruct P(…, guess, …) and compare against the observed output. If any sibling is unknown, the guess cannot be verified and the password is safe.

Protection — check (1) — propagates to descendants: once you are inside a PW_HASH argument, everything below is protected. Verifiability — check (2) — propagates only as long as every ancestor has known siblings; the first ancestor with an unknown sibling blocks the check all the way down.

This gives much more accurate results across the matrix of primitives. For instance, in the canonical ENC(key, pwd) case where key is private, the attacker does not know key — the only sibling of pwd — so the password is safe. For ENC(pwd, pubdata) where pubdata is public, the attacker knows every sibling of pwd, so the password is guessable. Both outcomes fall out of the same rule, with no per-primitive configuration.

The new examples/test/password_underspec.vp file walks through eleven queries across ENC, MAC, AEAD_ENC, SIGN, BLIND, and SHAMIR_SPLIT, with an inline comment on each one explaining what the attacker can and cannot do and why. It is probably the fastest way to get intuition for the new semantics.

This fix addresses issue #11 in full and substantially refactors the machinery that issue #12 was asking to clarify. #12 remains open for further discussion of edge cases, but the core formalism is now in place.

Checked ASSERT? Now Actually Halts the Principal

Issue #13, also from Cédric, was a pleasing little bug. Consider a protocol where Alice checks a tag before leaking a derived value:

principal Alice[
    tag_ = DEC(Ka, enctag)
    Kab_ = DEC(Ka, Kab_alice)
    Kab_bob_ = DEC(Ka, Kab_bob_alice)

    _ = ASSERT(tag_, HASH(Kab_, Kab_bob_))?
    leaks Kab_bob_
]

The ? on the ASSERT makes it a checked assertion: if the two sides are not equivalent, the principal halts, and the leaks statement that follows does not execute. Any downstream reasoning about what the attacker can learn must respect that halt.

In 0.50.0, Verifpal reported a false-positive attack against this protocol. An active attacker could swap two ciphertexts on the wire, making the assertion symbolically fail — the trace literally read ASSERT(HASH(kab, ENC(kb, kab)), HASH(kab, kab))?, which is not equivalent under any substitution — and yet the engine still treated leaks Kab_bob_ as firing in that branch and harvested values from it. The attack trace was nonsensical: the assertion it relied on was clearly false, but Verifpal was claiming the attacker had won anyway.

The underlying issue was that leaks was represented as a single leaked: bool flag on the target constant, with no record of which principal had declared the leak or where in that principal’s execution it sat. Active-attacker analysis can truncate a principal’s state after a failed checked primitive, but a constant declared before the failed assertion is still in the truncated state — and the attacker was using the leaked-constant token to re-resolve that constant in the mutated state and pick up a value the principal never actually leaked.

0.51.0 fixes this by adding an explicit LeakEvent record for every leaks declaration:

pub struct LeakEvent {
    pub constant_id: ValueId,
    pub principal_id: PrincipalId,
    pub declared_at: i32,
    pub phase: i32,
}

Each PrincipalState now carries an Option<halted_at> stamp set whenever a checked primitive fails during mutation analysis. The rule_equivalize deduction rule — the rule that lets the attacker re-resolve a known constant in the current state — consults both: if a leak event belongs to this principal with declared_at > halted_at, the principal never reached it, and the equivalize step is suppressed.

The examples/test/assert_junglegym.vp model is the reduced test case from Cédric’s report, now enforced as a regression test. Behavior with unchecked ASSERT (no ?) is deliberately unchanged: unchecked assertions are informative only, and the attacker is free to walk past them.

AEAD_ENC No Longer Leaks Associated Data

Up until 0.50.0, AEAD_ENC(key, plaintext, ad) was declared with passive_reveal: vec![2], meaning a passive attacker watching the ciphertext on the wire was automatically given the associated data. This was wrong in two ways.

First, the AD is an input to AEAD encryption, not a part of the ciphertext output. It is bound into the authentication tag, but the tag commits to AD without necessarily revealing it — whether AD is public depends on how the protocol transmits it, not on the encryption primitive itself.

Second, the blanket passive reveal was blocking legitimate queries where the AD was a secret (for example, a password used as AD), because Verifpal was automatically handing that secret to the attacker.

0.51.0 removes the passive_reveal: vec![2] entry. Associated data is now treated like any other argument: if the protocol sends it in the clear, the attacker sees it; if not, the attacker does not. The aead_leak.vp test has been updated to reflect the corrected semantics, and a new password_aead.vp test demonstrates that a password used as AD is safe when the other inputs are secret.

TUI: Multi-Output Primitive Labels

Issue #10, from @EFCCWEB3, was a small but annoying display bug in the terminal UI. The compact deduction ticker strips a "Output of " prefix off each deduction message to show a short label like HASH via reconstruct. For multi-output primitives — HKDF, SPLIT, SHAMIR_SPLIT — the underlying message uses indexed forms like "First output of HKDF(…)" or "Second output of SPLIT(…)". The literal-prefix match missed those, and the ticker fell back to the first whitespace-separated word, which was "First" or "Second".

The fix is one line: look for the shared " of " delimiter instead of the literal prefix. Multi-output primitives now show up correctly in the ticker.

New Models

Two models of note ship with the release:

• examples/transport-layer/tls13.vp — a 326-line TLS 1.3 model, included explicitly as a case study in Verifpal’s current limitations on large multi-phase protocols with many key-schedule stages. It is useful both as a reference and as motivation for future engine work.

• examples/messaging/scuttlebutt.vp — the existing Scuttlebutt model has been updated to guard longTermBPub (Bob -> Alice: [longTermBPub]), which exercises more interesting branches of the analysis than the unguarded form.

The password, assertion, and AEAD fixes each ship with at least one new dedicated test model in examples/test/.

Getting Verifpal 0.51.0

Scoop (Windows):

scoop update verifpal

Homebrew (macOS, Linux):

brew upgrade verifpal

From source:

cargo install --path . --features cli

Binaries for Windows, Linux, macOS, and FreeBSD are attached to the 0.51.0 GitHub release. As always, issues and contributions are welcome at github.com/symbolicsoft/verifpal.