Verifpal 0.70.0 is out. It is the biggest change to the Verifpal language since the project started, and the first release in years that asks you to edit your existing models, so this post goes through what changed and why.
Three things landed. Diffie-Hellman equations are gone: G^a is now PUBKEY(a), ga^b is now DH_KEX(ga, b), and the ^ operator no longer exists. There is a new key encapsulation mechanism, KEM_ENCAP and KEM_DECAP, for modelling post-quantum and hybrid key exchange. And the active attacker has been rebuilt around a different way of searching for attacks — and around explaining them, because an attack Verifpal finds is now narrated to you as a numbered sequence of things the attacker does, rather than dumped as a pile of state for you to decode.
If you have not used Verifpal before: 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. It then tries to break those properties. If it cannot, your protocol holds under the model you wrote. If it can, it shows you how, step by step.
An example: one missing character
Signal’s session setup is called X3DH. Bob publishes a bundle of public keys in advance, including a signed prekey: a medium-term key carrying a signature from his long-term identity key. Alice fetches the bundle, checks that signature, and mixes four Diffie-Hellman values into a master secret. The Double Ratchet takes over from there and gives every message its own key.
In Verifpal, Alice’s signature check looks like this:
_ = SIGNVERIF(gblongterm, gbs, gbssig)?The ? is what makes it a check. It tells Verifpal that Alice stops if verification fails. Without it, Alice computes the verification, discards the result and carries on. That is a realistic bug: the line is present, it calls the right function with the right arguments, and only the return value is missing.
Below is Verifpal 0.70.0 on a model of X3DH plus three Double Ratchet messages, with that ? removed. This model and the correct one both end with phase[1], in which Alice and Bob leak their long-term identity keys. That is how you ask Verifpal about forward secrecy: when these keys are compromised later, do the earlier messages stay secret?
Fail ✗ confidentiality? m1 ╭─ Attack trace: │ 1. Attacker replaces gbs, gbo (sent by Bob to Alice) with │ PUBKEY(nil), PUBKEY(nil). (gbs was PUBKEY(bs); gbo was PUBKEY(bo)) │ 2. Attacker observes e1 on the wire. │ 3. Attacker observes gae2 on the wire. │ 4. Attacker constructs akshared1 from gae2, nil. │ 5. Attacker constructs gbs from nil. │ 6. Attacker is handed alongterm by a leaks declaration. │ 7. Attacker constructs DH_KEX(gbs, alongterm) from gbs, alongterm. │ 8. Attacker observes gae1 on the wire. │ 9. Attacker is handed blongterm by a leaks declaration. │ 10. Attacker constructs DH_KEX(gblongterm, ae1) from gae1, blongterm. │ 11. Attacker constructs DH_KEX(gbs, ae1) from gae1, nil. │ 12. Attacker constructs amaster from DH_KEX(gbs, alongterm), │ DH_KEX(gblongterm, ae1), DH_KEX(gbs, ae1), DH_KEX(gbs, ae1). │ 13. Attacker constructs arkba1 from amaster, nil, nil. │ 14. Attacker constructs ackab1 from akshared1, arkba1, nil. │ 15. Attacker constructs MAC(ackab1, nil) from ackab1, nil. │ 16. Attacker constructs akenc1 from MAC(ackab1, nil), nil, nil. │ 17. Attacker opens e1 with akenc1, obtaining m1. ╰▸ m1 (m1) is obtained by Attacker. Pass ✓ authentication? Alice -> Bob: e1 Pass ✓ confidentiality? m2 Pass ✓ authentication? Bob -> Alice: e2 Pass ✓ confidentiality? m3 Pass ✓ authentication? Alice -> Bob: e3
The order of the steps matters here, so it is worth walking through them.
In step 1, before anything has been encrypted, the attacker swaps two of Bob’s public values for its own. That works because Alice’s signature check is not a check. At that point the attacker still cannot read anything: X3DH mixes four Diffie-Hellman values into the master secret, and two of them involve keys it does not have.
Then phase 1 arrives and the long-term keys leak. Two of the four Diffie-Hellman values now come from the leak, and the other two come from the substitution made much earlier, because PUBKEY(nil) is a public key whose private half the attacker knows. The master secret completes, the key schedule runs forward, and m1 opens.
The queries that passed are worth reading too, because they tell you where the damage stops.
m2 and m3 survive because the Double Ratchet heals. By the second message the key schedule has moved on to ephemerals the attacker never touched, and touching them now would fail a checked decryption on the far side and halt the protocol. Verifpal is reporting the boundary of the break as well as the break itself, which is usually the more useful half for a protocol designer.
All three authentication queries also pass. The attacker reads m1, but it never gets Alice or Bob to accept a message the other one did not send. Reading and forging are separate properties, and the tool keeps them separate.
The whole analysis takes 0.28 seconds.
How the search finds it
Seventeen steps, two simultaneous substitutions on one message, and a payoff a full phase later. That combination is why the search engine was replaced.
The old active attacker searched forwards: pick some combination of wire values to replace, try it, see what the attacker learns. The number of combinations grows quickly — six controllable values already give you six single substitutions, fifteen pairs and twenty triples — so the search needed a depth limit and a per-principal budget. Once those exist, they decide which attacks are reachable, rather than the protocol deciding.
Signal is the clearest example. The classic man-in-the-middle against X3DH needs three public keys replaced at the same time, and no affordable budget reliably got there. Whether Verifpal found it came down to a constant that could not be justified by looking at the model.
The new engine starts from the query instead. Given an unresolved query, what would the attacker need in order to contradict it? That requirement is broken into subgoals. Each subgoal is discharged against something the attacker already holds, or against the shape of what a principal is about to compute. A subgoal that can only be discharged under a particular substitution forces that substitution as a binding.
An attack requiring four simultaneous substitutions is then not a four-element combination that has to be affordable. It is four bindings, each forced independently, merged at the end.
Termination now comes from the structure of the search rather than a cap on it. Goals are memoised, so the same question is never answered twice. A goal that ends up depending on itself is cut as a cycle. The two rules that could otherwise generate unboundedly many new terms are restricted to a finite basis drawn from the protocol. Each of those is a property of the term algebra that you can check by reading it.
The old engine — verifyactive.rs, inject.rs and mutationmap.rs, 1,624 lines between them — is gone, along with the rayon dependency that parallelised the sweep. There is no SearchConfig in the new code, no depth cap, and nothing to tune.
Why the results can be trusted
Replacing the search engine in a verification tool is risky in one specific direction. Verifpal is sound but incomplete by design: the search may miss an attack, but any attack it reports has to be real. A missed attack is a disappointment. A false attack costs someone a day of work and their trust in the tool.
So soundness is enforced by the structure of the code rather than argued for in a comment. No module under src/solve/ can record a query result. The solver only proposes a substitution. Every proposal is materialised into a real principal state, re-executed through the ordinary analysis pipeline, and re-checked against actual attacker knowledge before anything is allowed to resolve. A bug in the solver costs a missed attack and cannot produce a false one.
The validator also owns one more check that does a lot of work: a substituted term that reduces back to the honest value is a replay, not an attack. Handing someone their own message back unchanged is not forgery, and conflating the two is one of the easiest ways to produce a false authentication result. Four models in the test suite exist to hold that line.
leaks declarations make available in that phase, values are resolved and rewritten, and the deduction rules run until nothing new can be learned. Query evaluation is a separate step that never interleaves with that loop. Under an active attacker, unresolved queries are solved backwards, and anything validation uncovers feeds the next round of deduction.Making the attack readable
A verifier that prints confidentiality? m1 and stops has done the easy half of the job. Knowing that something is broken is useful. Knowing what the attacker does is what lets you fix it, review it, argue about it, or teach it. Verifpal used to print the attacker’s knowledge set and the mutated state, and leave you to reconstruct the story from that yourself, which is a genuinely difficult reading exercise on anything the size of Signal.
So the engine does that work now. When a query resolves, two things happen before you see anything: the witness is minimized, and then it is narrated.
Minimizing: dropping everything the attack did not need
The solver pursues goals for every unresolved query at once and installs the union of the bindings it collects. That is the efficient thing to do, but it means the state that finally answers your query usually carries substitutions that some other query needed.
The forward-secrecy model from the top of this post is a good illustration. Analysing it, Verifpal made 1,805 proposals, and the one that broke confidentiality? m1 replaced five values on the wire simultaneously. You can watch this yourself by setting VERIFPAL_SOLVE_DEBUG=1, which logs every proposal the solver makes:
[solve] Alice ran=true [gbs=PUBKEY(nil) gbo=PUBKEY(nil) gbssig=nil gbe=PUBKEY(nil) e2=nil] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the two the attack needs the three the minimizer drops
The trace you actually saw named two of them. The other three went away one at a time, each dropped because the query kept resolving without it. gbssig is Bob’s prekey signature, and the attacker never needs to touch it precisely because Alice is not checking it. gbe and e2 belong to the second message, which has nothing to do with m1.
Minimization is deliberately paranoid, because a minimizer that cheats produces a trace that does not reproduce. Every probe re-runs the attack through the same re-execution path the search itself uses, in a scratch analysis context that is not permitted to record results. Each probe also re-seeds attacker knowledge from the passive baseline rather than from everything the attacker knew at the end of the search: knowledge only ever grows, so probing against the final state would make every substitution look droppable. And if nothing replays at all, Verifpal says so and reports only the derivation, instead of naming substitutions that may not be the ones that mattered.
Narrating: three kinds of step
What survives minimization gets rendered as numbered steps, of which there are exactly three kinds.
A substitution, grouped per wire message rather than one line per value, with the honest values in parentheses so you can see what was displaced:
1. Attacker replaces gbs, gbo (sent by Bob to Alice) with PUBKEY(nil),
PUBKEY(nil). (gbs was PUBKEY(bs); gbo was PUBKEY(bo))
A gate — a checked primitive that passed even though its inputs were attacker-controlled. This is the step a reader is most likely to disbelieve, so it gets a line of its own rather than being left implicit.
A derivation — one line for each step of the knowledge derivation, ingredients before target. These are not reconstructed after the fact by a pretty-printer guessing at what must have happened. Every rule that adds something to attacker knowledge is required to record how it got there, so the narration is read straight off the derivation the engine performed. A step the attacker carried out inside a different principal’s session is labelled with that session, on the line itself.
Names, not terms
The other half of readability is vocabulary. Step 17 of that trace read:
17. Attacker opens e1 with akenc1, obtaining m1.
Here is the engine’s internal record of the same step, with the terms written out in full:
Deduction › m1 obtained by decomposing AEAD_ENC(HKDF(MAC(HKDF(DH_KEX(PUBKEY(nil),
ae2), HKDF(HASH(DH_KEX(PUBKEY(nil), alongterm), DH_KEX(PUBKEY(blongterm), ae1),
DH_KEX(PUBKEY(nil), ae1), DH_KEX(PUBKEY(blongterm), ae1)), nil, nil), nil), nil),
nil, nil), m1, HASH(PUBKEY(alongterm), PUBKEY(blongterm), PUBKEY(ae2))) with
HKDF(MAC(HKDF(DH_KEX(PUBKEY(nil), ae2), HKDF(HASH(DH_KEX(PUBKEY(nil), alongterm),
DH_KEX(PUBKEY(blongterm), ae1), DH_KEX(PUBKEY(nil), ae1),
DH_KEX(PUBKEY(blongterm), ae1)), nil, nil), nil), nil), nil, nil).
Both say the same thing. The difference is that the narrator keeps a table mapping terms back to the names the model already gave them, so a value Alice calls akenc1 is called akenc1 in the trace, and only the parts with no name of their own get spelled out. The table also excludes the slots a step is itself touching, which is what stops a substitution line from reading “replaces gb with gb”, and the same table feeds the summary line so it quotes the same vocabulary as the steps above it.
None of this changes a single verdict. It changes whether the verdict is something you can hand to a colleague who has never opened Verifpal, walk through line by line, and check by hand — and, for the people who use Verifpal to teach protocol analysis, whether an attack is a thing students can read.
Phases, and when the attacker knows things
Phases are how Verifpal models time. phase[1] means later, and a leaks declaration inside it is a compromise that happens after the earlier traffic has already gone by. That is what makes forward secrecy, key compromise impersonation and post-compromise security expressible.
It also creates a trap. If the attacker’s phase-1 knowledge is allowed to justify an action it took in phase 0, then any key that ever leaks retroactively forges every signature that was ever checked, and forward secrecy queries stop meaning anything.
In 0.70.0, a proposed substitution is judged against the attacker’s knowledge as of the phase of the value it touches, not against everything accumulated by the end of the run. Attacker knowledge is snapshotted at the end of each phase, and a substitution that reaches back into an earlier phase is re-executed against that earlier snapshot.
Two models one line apart show the difference:
| model | the prekey is… | phase 1 | confidentiality? m |
|---|---|---|---|
| phase_signed_prekey.vp | signed, and checked with ? | both identity keys leak | holds |
| phase_unsigned_prekey.vp | not signed at all | both identity keys leak | contradicted |
In the signed model, the attacker would have to swap the prekey during phase 0, and in phase 0 it does not have the identity key it would need to forge the accompanying signature. The leak arrives too late to help. In the unsigned model there is no signature to forge, the swap succeeds when it is made, and the phase-1 leak completes it. It is the same shape as the Signal example above, in about twenty lines, which makes it a good teaching model for why signed prekeys exist.
Both directions matter. Too permissive and the tool invents retroactive forgeries; too strict and it misses the store-now-decrypt-later attacks that phases exist to express. Seven models in examples/test/ pin the boundary from both sides, including a three-phase one where the tampering, the compromise and the payoff happen at three different times.
Relaying is not forging
This distinction comes up as soon as a protocol has more than two parties.
Take a value that Alice signs and encrypts to Carol; Carol opens it and re-envelopes it to Bob; Bob verifies the signature and MACs it onward to Damian. The message Bob receives was sent by Carol, and it contains Alice’s content unchanged. Should authentication? Alice -> Carol: envelope fail?
It should not, because being known to the attacker is not the same as being forgeable by the attacker. A value the attacker can watch go past, relay unchanged, or rebuild identically out of honest pieces is not a value it can substitute for something else. An engine that blurs those two things reports man-in-the-middle attacks against protocols that do not have any.
Fail ✗ confidentiality? msg ╭─ Attack trace: │ 1. Attacker observes msg on the wire. ╰▸ msg (msg) is obtained by Attacker. Pass ✓ authentication? Alice -> Carol: envelope Pass ✓ authentication? Carol -> Bob: re_envelope Pass ✓ authentication? Bob -> Damian: audit_mac
Confidentiality fails because the final hop sends the plaintext in the clear, which is what this model does deliberately, and the trace is one line long because that is the whole attack. The three authentication queries hold across the entire relay chain, through a re-envelope, a signature check and a MAC. relay_not_forgery.vp and key_ratchet.vp pin the same property in smaller models.
Removing equations
Verifpal has always had a kind of value that existed for exactly one purpose. Alongside constants and primitives there were equations, written G^a and G^a^b, with G as a reserved generator, a limit of two exponents, and their own handling in the parser, the pretty printer, the equational theory, the unifier and the attacker search. They modelled Diffie-Hellman and nothing else, and all five of those places had to be kept consistent by hand.
From 0.70.0, Diffie-Hellman is written with two ordinary primitives: PUBKEY(a) for a public key derived from a private value, and DH_KEX(gb, a) for a shared secret.
DH_KEX(PUBKEY(a), b) and DH_KEX(PUBKEY(b), a) are still the same shared secret, and the attacker still cannot compute either one from two public keys. What changed is where those facts live: commutativity, and the argument restrictions that make computational Diffie-Hellman structural, are now two fields on a primitive spec instead of properties baked into the value representation.Migration is mechanical, with five patterns to look for:
| 0.53 | 0.70 |
|---|---|
ga = G^a |
ga = PUBKEY(a) |
gab = ga^b |
gab = DH_KEX(ga, b) |
SIGNVERIF(G^sk, m, sig) |
SIGNVERIF(PUBKEY(sk), m, sig) |
PKE_ENC(G^sk, m) |
PKE_ENC(PUBKEY(sk), m) |
the attacker’s own key, G^nil |
the attacker’s own key, PUBKEY(nil) |
Value now has two variants instead of three. Every function in the engine that matched on a value used to carry a third arm whose behaviour had to be kept consistent with the other two by hand. Resolution, equivalence, matching and the solver each lost one.
KEM_ENCAP and KEM_DECAP
Removing equations was the prerequisite for this part, rather than the goal in itself.
principal Alice[
generates r
ss, ct = KEM_ENCAP(ekb, r) // a shared secret, and a ciphertext
e = AEAD_ENC(ss, m, nil)
]
Alice -> Bob: ct, e
principal Bob[
ssb = KEM_DECAP(dkb, ct) // where ekb = PUBKEY(dkb)
d = AEAD_DEC(ssb, e, nil)?
]A key encapsulation mechanism has no exponent to commute and no generator to sit in base position, so there was no way to express one through the equation interface — not for want of a feature, but because that interface was shaped around one algebraic structure that a KEM does not have. As two ordinary primitives, KEM_ENCAP and KEM_DECAP are about thirty-five lines of declarative data in primitive/spec.rs, and the rest of the engine picked them up without being told they exist.
They are generic rather than named after a specific algorithm. ML-KEM, HQC and Classic McEliece are indistinguishable in the symbolic model: what a symbolic attacker can do with a ciphertext does not depend on whether the underlying hardness assumption is module-lattice or code-based. Naming the primitive MLKEM_ENCAP would imply a precision the model does not have.
Since we started recommending post-quantum native design, the question we get most often is what a hybrid actually buys you. Three models answer it:
| model | what leaks in phase 1 | confidentiality? m |
|---|---|---|
| kem_hybrid_classical_broken.vp | both Diffie-Hellman private values | holds |
| kem_hybrid_pq_broken.vp | the decapsulation key | holds |
| kem_hybrid_both_broken.vp | both, together | contradicted |
All three are the same protocol: an X25519 shared secret and a KEM shared secret, both fed into HKDF, with the resulting session key protecting one message. The only difference is what phase 1 leaks. It is the hybrid construction argument as three files you can run in a design review.
One detail in the KEM rules is easy to get wrong. An attacker holding the decapsulation key can open an encapsulation even if no principal in the model ever calls KEM_DECAP, because the decomposition rule yields one of the primitive’s outputs rather than one of its arguments. Holding the ciphertext and a decapsulation key of its own gets the attacker nowhere: kem_secret_not_forgeable.vp gives the attacker its own key pair, leaks it outright, hands it the ciphertext from the wire, and both confidentiality queries still hold.
Two more shapes follow from encapsulation being a function of its arguments. Encapsulate twice to the same key with the same randomness and the shared secret is identical, so equivalence? ss1, ss2 holds — which is how the hazard becomes visible, since two secrets from two separate encapsulations should not be interchangeable. With fresh randomness the query is contradicted. Freshness works the same way: a shared secret is only as fresh as the randomness behind it, so freshness? ssfresh passes and freshness? ssstatic does not.
Twelve messages of Signal
In February, Verifpal verified X3DH and the Double Ratchet across three messages under an active attacker, which was then the deepest result the tool had produced. examples/messaging/signal_twelve.vp extends the same model to twelve messages. Each one generates a fresh ephemeral, mixes it with the peer’s most recent ephemeral public value, and chains the resulting root key onto the previous one — twelve rounds of nested key derivation, and twenty-four queries covering every message in both directions.
attacker[active] · 2 principals · 12 messages · 24 queries c0a0c0a0c0a0c0a0c0a0c0a0c0a0c0a0c0a0c0a0c0a0c0a0 confidentiality and authentication, for every message, all holding. real 37.19s
Thirty-seven seconds is slower than we would like, and we intend to bring it down. But it finishes, and it finishes with the right answer, which the old search could not do at this depth.
Getting it, and moving your models over
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. Either way you get automatic updates.
There is no automatic migration tool, deliberately. A rewriter would have to guess which side of a ^ was meant to be the exponent in the cases where a model was doing something unusual, and a wrong guess gives you a model that parses cleanly and means something else. The parser points at every line that needs attention instead:
Error: mymodel.vp:5:8: parse error: cannot use reserved keyword in name: g
ga = G^a
^
Work through the five patterns above and most models take a few minutes. The rest of the toolchain is already updated: the browser-based Workbench runs 0.70.0 with nothing to install, Print 20 of the Verifpal Manual documents the new primitives and the backwards search, and both the VS Code extension (1.0.11) and the Neovim extension highlight and document PUBKEY, DH_KEX, KEM_ENCAP and KEM_DECAP.
If you model something and a result looks wrong to you, please open an issue. Several of the changes in this release started with exactly that.