Verifpal 0.80.0: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability

Verifpal 0.80.0 is out, a few days behind 0.70.0. The two releases do quite different kinds of work, and it is worth separating them at the outset: 0.70.0 changed how you write models, while 0.80.0 changes what a model is able to say.

There are two additions. The first is that a primitive can now be declared broken — weak, forgeable, and optionally only from a chosen phase onward — so that an assumption which previously had to be approximated with a list of leaked values, or which could not be written down at all, becomes part of the model itself. The second is that unlinkability queries are now decided by searching for a concrete link witness: a value in the attacker’s hands that ties two identities to the same participant. When such a witness exists, Verifpal reports it to you as the explanation.

Unlike 0.70.0, this release asks you to edit nothing. A model with no annotations behaves exactly as it did before, and there is a test in the suite whose only job is to keep that true. The one thing worth re-checking is your unlinkability verdicts, which can legitimately move in either direction; we will come back to why near the end.

If you have not used Verifpal before, here is the shape of it. You describe a protocol in a small language — who knows what, who generates fresh values, who sends what to whom, what gets hashed, signed and encrypted — and then you write down the security properties you want, as queries. Verifpal plays an attacker on the network, reading everything and, if you ask for an active attacker, tampering with anything you have not explicitly protected. If it cannot break a property, that property holds against every attack Verifpal knows how to look for, under the model you wrote. If it can, it shows you how, step by step. The 0.70.0 post walks through that machinery in some detail.

Why a model might want imperfect cryptography

In a symbolic model, cryptographic primitives are perfect by construction. A hash is never invertible, a signature is never forgeable, an encryption never gives up its plaintext. This is not a simplification we tolerate; it is the entire point of the approach. Because the primitives are ideal, every attack the tool finds has to come from the structure of the protocol — from a missing check, a reused key, a value that arrives unauthenticated — rather than from a weakness in a cipher. That is what makes symbolic analysis fast, automatic, and worth doing.

But some of the most important questions we ask about protocols are precisely questions about what happens when a primitive stops being perfect. What survives if this cipher is broken in ten years? What does an implementation flaw in one signature scheme cost the rest of the handshake? These questions are about protocol structure too — they ask how well the design contains a failure — and until now Verifpal could only approximate them.

The approximation was leaks. If you wanted to model “the attacker can now break this Diffie-Hellman”, you handed the attacker the private values with a leaks declaration and let the ordinary deduction rules do the rest. The 0.70.0 post leaned on exactly this technique: the hybrid key-exchange argument was made with three files whose only difference was what phase 1 leaked.

This works well, and it is still the right tool for many jobs. Its limitation is that a leaks declaration enumerates values, while the assumption you are actually making is about a capability. When those two line up exactly, and the list is short, nothing is lost. As a model grows, keeping them lined up becomes your job rather than the tool’s. If you later add a sixth Diffie-Hellman exchange and forget to extend the list, the model quietly proves something weaker than you believe it proves, and nothing in the output tells you so.

From 0.80.0, you can state the capability directly. A primitive call site may carry a bracketed list of declared weakening assumptions, written between the primitive’s name and its arguments:

ga = PUBKEY[weak](a)                    // discrete logarithm: holding ga yields a
s  = SIGN[forgeable](sk, m)             // signatures forgeable without sk
e  = AEAD_ENC[weak, forgeable from phase 2](k, m, ad)

weak means that confidentiality is lost, so that holding the term yields whatever the term was protecting. forgeable means that authenticity is lost, so that the term becomes constructible by someone who does not hold its secret. from phase N means the assumption comes into force from phase N onward, and it binds to the capability it follows; without it, the assumption is in force from the beginning.

Which primitives accept which assumption, and what precisely falls out of each, is declarative data on the primitive specification — the same table that already defines every rewrite and decomposition rule in the equational theory:

The last row of the weak group is worth pausing on, because of how much it gives us for how little. PUBKEY[weak] says that a public key yields its private half, which is to say that discrete logarithm has been solved. Notice what this implies for Diffie-Hellman: if the attacker takes a public key off the wire and recovers the private value behind it, then it can recompute every shared secret that value was ever used in. That cascade is not something we had to teach the engine. Recall from 0.70.0 that Diffie-Hellman in Verifpal is written with two ordinary primitives, PUBKEY and DH_KEX, with commutativity declared as a field on the specification. Because of that, once PUBKEY[weak] hands the attacker a private value, the existing reconstruction machinery — the same rules that let an attacker rebuild any primitive whose arguments it knows — carries the consequences forward on its own. There is no Diffie-Hellman-specific rule involved anywhere. The model cap_weak_pubkey_dh.vp exists to pin that down, and its header comment says so explicitly, so that a future change which quietly introduces a special case will be caught.

A worked example: the hybrid argument, written as an assumption

Two new models in examples/messaging/ describe PQXDH, Signal’s current session setup, which is X3DH with a signed KEM prekey added and the KEM shared secret mixed into the master secret alongside the four Diffie-Hellman values.

The first model, pqxdh.vp, asks the harvest-now-decrypt-later question in the older style. The attacker records the handshake as it goes past, and then in phase 1 every Diffie-Hellman private value leaks — five of them, named one by one. The message has to survive on the KEM leg alone, and it does.

The second model, pqxdh-weak.vp, is the same protocol with the same adversary stated as an assumption instead. Every Diffie-Hellman public key is annotated, and nothing leaks at all:

principal Bob[
	knows private blongterm, bs
	generates bo, dkb
	gblongterm = PUBKEY[weak from phase 1](blongterm)
	gbs = PUBKEY[weak from phase 1](bs)
	gbo = PUBKEY[weak from phase 1](bo)
	ekb = PUBKEY(dkb)
	gbssig = SIGN(blongterm, HASH(c2, gbs))
	ekbsig = SIGN(blongterm, HASH(c3, ekb))
]

The one line to look at closely is ekb, the KEM encapsulation key, which carries no annotation. That omission is the hybrid argument in its entirety: discrete logarithm falls, the KEM does not, and the model claims the message survives on exactly that difference. The phase[1] block in this model is empty, because the annotation is carrying the whole adversary by itself.

  Warning ▲ Analysis performed under 5 declared weakening assumptions:
  Warning ▲ PUBKEY[weak from phase 1](alongterm)
  Warning ▲ PUBKEY[weak from phase 1](blongterm)
  Warning ▲ PUBKEY[weak from phase 1](bs)
  Warning ▲ PUBKEY[weak from phase 1](bo)
  Warning ▲ PUBKEY[weak from phase 1](ae1)
 
     Pass ✓ confidentiality? m1
     Pass ✓ authentication? Alice -> Bob: e1

The warning block above the results is deliberate, and we would like to explain the reasoning behind it. A passing result obtained under a weakening assumption is a different claim from a passing result obtained without one, and results travel: they get pasted into review documents, quoted in issues, and screenshotted into slides. So a verification performed under declared assumptions now says so every time, listing each annotated term directly above the verdicts. The internal-json interface carries the same list on every result it emits, and the Workbench displays it, so the caveat stays attached to the verdict wherever the verdict goes.

Both models report the same result code, which is a good sign: the new mechanism reproduces what the old technique already established. What differs is what each model claims, and how each behaves as it grows. The annotated version covers any key derived through an annotated PUBKEY, whether or not the author remembered that particular key was there.

Assumptions that arrive later

There is a class of assumption that leaks approximates awkwardly, and one that it cannot express at all. The second case is easiest to see in a small model, cap_weak_phase_delayed.vp, which is about twenty lines long:

principal Alice[
	knows private k
	knows private m_now
	knows private m_later
	e_now = AEAD_ENC(k, m_now, nil)
	e_later = AEAD_ENC[weak from phase 2](k, m_later, nil)
]

Read the two encryptions carefully: they use the same key. The result code is c0c1, meaning that m_now stays confidential for the whole run, while m_later — recorded off the wire back in phase 0 — opens once phase 2 arrives.

It is worth trying to write this with leaks before reading on, because the exercise is short and the failure is instructive. Leaking k breaks both messages, since both were encrypted under it. Leaking m_later assumes the very thing we wanted the tool to derive. There is simply no value whose disclosure expresses “the attacker becomes able to invert this particular encryption, at this particular time”. The assumption is about an ability rather than about a secret, and it is scheduled rather than immediate.

This is the distinction the two mechanisms now divide between them. leaks hands the attacker values. A capability grants the attacker abilities, optionally on a timetable. Harvest-now-decrypt-later scenarios are the obvious beneficiaries, since their entire premise is that data collected today becomes readable under a capability the adversary does not yet have.

Why weak and forgeable are two separate assumptions

The 0.70.0 post made a point of keeping properties apart: reading a message and forging one are different powers, and Verifpal reports them as different queries. When we designed capabilities, the same separation had to hold for assumptions, which is why there are two words here rather than one general notion of “broken”.

The case that settles the argument is AEAD_ENC[forgeable]: a ciphertext that an attacker can produce but still cannot read. That combination sounds unusual, but it is exactly what an authenticity failure without a confidentiality failure looks like, and a single combined assumption could not express it. The model cap_forgeable_aead.vp keeps the two from collapsing back together:

  Warning ▲ Analysis performed under 1 declared weakening assumption:
  Warning ▲ AEAD_ENC[forgeable](k, m, ad)
 
     Pass ✓ confidentiality? m
     Fail ✗ authentication? Alice -> Bob: e
            ╭─ Attack trace:
            │ 1. Attacker replaces e (sent by Alice to Bob) with
            │    AEAD_ENC(k, nil, ad). (e was AEAD_ENC(k, m, ad))
            │ 2. Bob's AEAD_DEC(k, e, ad)? passes — its inputs are
            │    attacker-controlled.
            ╰▸ e (e), sent by Attacker and not by Alice, is successfully
               used in AEAD_DEC(k, e, ad)? within Bob's state.

Step 2 of that trace is the one to examine. Bob’s decryption is checked, marked with ?, which normally means that a failure halts him — and here it passes, on a ciphertext Alice never produced, because the assumption says such ciphertexts can be manufactured. The narrator prints that step on a line of its own rather than leaving it implicit, since it is the step a careful reader will want to see justified. Meanwhile confidentiality? m still passes, because forgeability says nothing whatsoever about reading. The model’s header comment records what it is guarding: if that confidentiality query ever starts failing, weak and forgeable have been merged somewhere in the engine and the distinction has stopped doing its job.

What happens when an assumption does not apply

A declared assumption reads, to anyone reviewing the model, like a check that was carried out. That creates a responsibility for the tool. If SIGN[weak] were to parse and then quietly do nothing, every reader of that model would come away believing something about it that is not true, and they would have no way of noticing. An annotation that silently does nothing is therefore more dangerous than no annotation at all.

For that reason, every capability is validated against the primitive specification when the model is loaded, and the diagnostics try to name the assumption you probably intended:

Error: cap_err_sign_weak.vp:11:2: sanity error: SIGN provides authenticity,
not confidentiality; did you mean `SIGN[forgeable]`?
   s = SIGN[weak](sk, m)
   ^^^^^^^^^^^^^^^^^^^^^
 
Error: cap_err_hash_forgeable.vp:10:2: sanity error: HASH has no secret
argument; anyone who knows its inputs can compute it
   h = HASH[forgeable](m)
   ^^^^^^^^^^^^^^^^^^^^^^
 
Error: cap_err_aead_malleable.vp:12:2: sanity error: malleability of an
authenticated primitive is an authenticity break; did you mean
`AEAD_ENC[forgeable]`?
   e = AEAD_ENC[malleable](k, m, ad)
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Each message tries to teach something rather than merely refuse. SIGN[weak] is rejected with a reminder of what a signature is for. HASH[forgeable] is rejected because a hash has no secret argument, so there is nothing for forgeability to bypass — anyone who knows the inputs can already compute the output. The same principle extends to time: weak from phase 5 in a model that never reaches phase 5 is a hard error, not an assumption that quietly never fires.

The third message deserves a fuller explanation, since malleable is in the vocabulary and parses correctly, yet no primitive declares it, so every use of it is rejected. It was designed and partially built during this release cycle and then deliberately held back. The attacks that malleability enables generally require two coordinated substitutions on the wire, and the solver’s goal-directed search cannot presently derive the ciphertext goal that would force them. Shipping the annotation anyway would have meant advertising a class of attack that the engine could not actually find, and a model author would read a passing result as evidence of resistance to malleability when it was really evidence of a search limitation. Rejecting the word with an explanation seemed much better than that, so it stays reserved until the solver can honor it.

Two further guarantees are worth stating plainly, because they are what let you adopt this feature without auditing your existing work. First, weak, forgeable, malleable and from are contextual keywords: they are recognised only inside the parameter brackets, where no constant can appear. A model that already uses weak or from as a constant name is unaffected. Second, a model with no annotations produces byte-identical behaviour to before, and cap_noop_annotated.vp holds an annotated model to the exact verdicts of its unannotated twin.

That second guarantee rests on a design decision that we think is interesting in its own right. Capabilities are deliberately invisible to term hashing and to equivalence, so an annotated term and its unannotated twin count as the same cryptographic object throughout the engine. The assumptions live instead in a model-level index that the engine consults separately. The reason is that attacker knowledge deduplicates values by equivalence: if the engine read capabilities off whichever copy of a term it happened to be holding, then the outcome could depend on whether the annotated or the unannotated copy of a value reached the attacker first, which in turn depends on the order in which principals were walked. Keeping the annotation out of the term and in an index removes that possibility entirely. And because capabilities feed the ordinary deduction pipeline, the soundness argument from 0.70.0 carries over untouched: the solver still only proposes, and validation still re-executes every proposal against real attacker knowledge before any result is recorded.

Unlinkability, decided by finding a witness

The other half of this release concerns a query we had been deciding badly. unlinkability? asks whether an attacker can tell that two values belong to the same party — the property that pseudonymous identifiers, rotating beacons and anonymous credentials are built to provide. Verifpal decided it with two structural tests, and we now think both were the wrong shape.

The first test failed the query whenever a queried value contained no fresh constant. That reports a property of the model as though it were an attack, and worse, it disagreed with Verifpal’s own freshness? query, which asks about the very same thing and asks it correctly. The second test failed the query when two queried values were outputs of a single primitive application that the attacker could rebuild. Because it could only ever compare siblings from one application, linkability across sessions or epochs — which is the kind privacy protocols actually worry about — was invisible to it by construction. Neither test consulted what the attacker had observed, which is a strange thing for a decision about an attacker’s knowledge.

Verifpal now decides unlinkability the way the User Manual has always defined it, by searching for a concrete link witness: a value the attacker holds which ties both queried values to one participant. There are three kinds of witness, tried in order of cost:

The third kind is the one the old procedure could not see at all, and a contact-tracing model shows why it matters. In dp3t_root_leaked.vp, each phone derives its broadcast identifiers from a daily seed, and each day’s seed is the hash of the previous one:

EphID00A, EphID01A, EphID02A = HKDF(nil, SK0A, BroadcastKey)
// the next day:
SK1A = HASH(SK0A)
EphID10A, EphID11A, EphID12A = HKDF(nil, SK1A, BroadcastKey)

EphID00A and EphID10A come from different days, and from different HKDF applications, so the old sibling test had no way to relate them. Leak the day-zero seed, and the new procedure finds the connection immediately:

     Fail ✗ unlinkability? ephid00a, ephid10a
            ╭─ Attack trace:
            │ 1. Attacker is handed sk0a by a leaks declaration.
            ╰▸ Attacker links ephid00a and ephid10a via sk0a.

A single leaked seed links every identifier that phone will ever broadcast, in every epoch, because HASH(SK0A) and each HKDF above it can be recomputed from the root. This is seed-compromise linkability, and being able to name the seed as the witness is what makes the result actionable: the fix is visible in the trace itself.

Two conditions that keep a witness honest

A search that reports links is only useful if the links are real, so two conditions gate every witness. They are worth understanding if you write privacy models, because they explain results that might otherwise look conservative.

The first is observability. Both queried values must have travelled on the wire or been leaked. A value the attacker cannot reach cannot be linked, no matter what it is derived from, since linkage is a statement about what an observer can conclude. Related to this, when the search tries to reconstruct values from a candidate secret, it first withholds the queried values themselves from the attacker’s knowledge. The reason is worth stating: merely receiving a value tells you nothing about whose it is. Only being able to recompute it from something that identifies a participant does. Reconstructing a value the attacker was simply handed would be circular, and the search declines to do it.

The second condition is that neither queried value may be attacker-authored. An active attacker that overwrites two slots with one value of its own has manufactured the very equality it would then be reporting, which is not an observation about the protocol at all. unlink_injected_equality.vp pins that this is never counted as a witness.

That restriction applies to the linked values themselves, not to the attacker’s activity in general. Attacker actions upstream still count, and they should. In unlink_active_links.vp, the attacker substitutes its own Diffie-Hellman key into the handshake, and the session key that results becomes the common origin for two tokens that the victim went on to compute honestly:

│ 1. Attacker replaces ga (sent by Alice to Bob) with PUBKEY(nil). (ga was PUBKEY(a))
│ 2. Attacker observes gb on the wire.
│ 3. Attacker constructs k from gb, nil.
╰▸ Attacker links tok1 and tok2 via k.

Both queried tokens are Bob’s own values, computed by Bob, so the witness describes something genuine about the protocol. The boundary sits precisely at authorship of the linked values, and nowhere earlier.

There is one more restriction, and it is our favourite illustration of how much care the identifying-check witness needs. Consider two models with the same structure and opposite verdicts:

Two ordinary signatures verifying under one key are linkable, and the reasoning is exactly what a student would give: the verification key names the signer, so a successful SIGNVERIF over both signatures identifies them as coming from the same party. Two ring signatures over the same ring are not linkable, even though RINGSIGNVERIF also succeeds over both, because a successful ring verification names a set of possible signers and never a member of it. The engine knows the difference because the specification table records which argument positions identify a participant: SIGNVERIF declares its key argument as identifying, and RINGSIGNVERIF deliberately declares none. That declared emptiness is the only thing standing between this query and a false attack against the one primitive whose entire purpose is unlinkability, which is why the two models sit next to each other in the test suite.

If you have unlinkability queries in existing models, please re-run them, because verdicts can move in both directions and both movements are corrections. Models that used to fail on the freshness clause will now pass, since a value the attacker can neither reach nor observe cannot be linked. Models with a compromised seed high in a derivation chain may now fail where they previously passed, which is the case the old procedure was structurally unable to detect. In both directions, a failing query now hands you a witness you can check by hand rather than a condition you have to take on faith.

Getting it, and what to re-check

brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install verifpal

On Windows, scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git followed by scoop install verifpal.

There is no migration this time. Annotations are entirely opt-in, an unannotated model behaves as it did under 0.70.0, and the result code format is unchanged. Two things are worth your attention. Re-run any model containing an unlinkability? query, and read the witness if the verdict has changed. And look at any leaks declaration that was standing in for “this primitive is broken”, since it may now be expressible directly, with the added benefit that anyone reading the output will see the assumption stated alongside the result.

The rest of the toolchain is current. The Workbench runs 0.80.0 and displays declared weakening assumptions alongside results, internal-json attaches the assumption list to every result it emits, the Verifpal User Manual documents both additions, and the VS Code extension (1.0.12) and Neovim extension highlight the new syntax.

If you model something and a result looks wrong to you, please open an issue. The unlinkability rework in this release began with noticing that the old procedure disagreed with the tool’s own manual and its own freshness query, and that sort of noticing is how the tool improves.