Verifpal 1.3 is out. The new engine work in it is peer scenarios, which let a model instantiate a principal’s counterparty differently across concurrent runs. Three smaller additions come with it: every passing query now prints the envelope it was reached under, --saturate raises the session count until the verdicts stop moving, and --auto-queries generates a query set from the model.
The second half of this post covers what shipped in the point releases between 1.0 and this release, none of which got a write-up at the time.
Verifpal finds Lowe’s attack now
The Needham-Schroeder public key protocol is from 1978. Gavin Lowe broke it in 1995 with a man-in-the-middle attack in which nothing is forged and no key is broken, and it has been a standard teaching example ever since. Verifpal could not find it. Worse, Verifpal could not tell the broken protocol apart from the fixed one.
The attack cannot be written down without a way to say who a principal thinks it is talking to. Lowe’s attack needs Alice running the protocol twice at once, once with an honest Bob and once with Mallory, who is a legitimate participant whose private key has leaked. --sessions does not help here, because every session replicates the same cast.
1.3 lets you say who the peer is. The new scenarios[] block goes at the bottom of the model:
scenarios[
Alice[gpeer = gb]
Alice[gpeer = gm]
]Each entry binds constants inside one named principal, and scenario k is clone k of the whole model. Every principal and every message is cloned, and only the named principal’s bindings are substituted. Two scenarios therefore give you two whole-model configurations. One entry cannot rebind two principals at once. Alice talks to Bob in one copy and to Mallory in the other, concurrently, and the attacker is free to carry messages between them.
The bound knows declaration is dropped from the clone and the constant is replaced everywhere inside that principal. The value is then freshened like any other expansion copy, so Alice[gpeer = gm] in the second scenario uses gm@2, the copy that Mallory@2 assigns.
Run it against the unfixed protocol:
Warning ▲ Analysis performed over 2 declared peer scenarios: Warning ▲ Alice[gpeer = gb] (honest peer) Warning ▲ Alice[gpeer = gm] (corrupt peer) Fail ✗ confidentiality? nr ╭─ Attack trace: │ 1. Attacker replaced m1 with PKE_ENC(gb, CONCAT(ni@2, ga)), │ after which m2 resolved to PKE_ENC(ga, CONCAT(ni@2, nr)). │ 2. Attacker replaces m2@2 (sent by Bob@2 to Alice@2) with │ PKE_ENC(ga, CONCAT(ni@2, nr)). (m2@2 was │ PKE_ENC(id_b@2, CONCAT(ni_b@2, nr@2))) │ 3. Alice@2's SPLIT(PKE_DEC(a, m2@2))? passes — the attacker │ controls one of its inputs. │ 4. Alice@2's ASSERT(SPLIT(PKE_DEC(a, m2@2))?, ni@2)? passes — │ the attacker controls one of its inputs. │ 5. Attacker observes m3@2 on the wire. │ 6. Attacker is handed mk by a leaks declaration. │ 7. Attacker opens m3@2 with mk, obtaining nr. ╰▸ nr (nr) is obtained by Attacker.
That is Lowe’s attack. Nothing in the model hints at it. The file describes the protocol and declares the two runs. The attacker lifts Alice’s nonce out of her run with Mallory, reseals it under Bob’s key carrying Alice’s own identity, and Bob’s identity check passes because the identity really is Alice’s. Bob finishes the protocol believing he spoke to Alice, while the attacker holds his nonce.
Add Lowe’s fix and the same query passes: spore_nsl_pk.vp reports PASS + confidentiality? nr [search exhausted at 2 sessions]. Getting that pair to separate was the acceptance criterion for the whole feature. Without a way to vary Alice’s peer, the two protocols are indistinguishable at every session count.
The engine did not change
Like --sessions, this is an expansion that happens before anything is analyzed. expand_scenarios rewrites the parsed model, then session expansion rewrites that, and only then does the model reach sanity checking and the engine. What the engine sees is an ordinary Verifpal model you could have typed out by hand, with Alice, Alice@2, Alice#2 and Alice@2#2 all written out as separate principals.
Verifpal’s soundness argument is about what the analysis path can reach, and a new front end adds nothing to that path, so peer scenarios inherit attack-soundness from the engine without needing an argument of their own. It also puts a ceiling on the feature: scenarios multiply with sessions, so p principals with s scenarios at k sessions analyze p × s × k principals, and the model has to stay under 128 principals with s × k at most 31. Ask for more and Verifpal tells you to declare fewer scenarios or lower --sessions.
Corruption is worked out for you
You never mark a scenario as corrupt. Verifpal seeds a set of compromised constants from the ones that are both leaked and secret, then closes over any assignment mentioning them. So gm = PUBKEY(mk) with leaks mk marks gm compromised, while leaks gb on an ordinary public key does not. A scenario binding a compromised value is a corrupt-peer run.
That decides two separate things, and conflating them is a bug in each direction. A clone talking to a corrupt peer will legitimately fail a checked primitive, because Alice sealing to a corrupt peer’s key means the honest responder cannot decrypt, so those failures must not be reported as modelling errors. Separately, a corrupt run’s own claims are not the protocol’s to keep, so its queries are not evaluated. Verifpal still explores the run for whatever the attacker learns there, which is the entire point of having it. Too strict and every protocol “fails” the moment you model a dishonest participant; too loose and you report a vacuous hold for everything. Scyther draws the same distinction.
Confidentiality gets one extra step. Attacker knowledge is global and monotone, so a secret first broken inside a corrupt run is still broken for the honest ones, and Verifpal re-runs the standard check at the end of each phase to make sure that lands on an honest principal. Without it, the Needham-Schroeder result would depend on which principal the search happened to reach last.
The block is checked before it expands
A scenarios[] block is validated against its own source span before any expansion happens. Accepting a bad one silently would change a verdict where an error belongs. During development, a typo in a principal name once turned the Needham-Schroeder c1 into a passing c0.
Six things are rejected: a principal the model does not declare, a target that principal does not knows, a value no principal declares, a target bound twice, a target that travels over the wire, and an identity binding that drops its declaration. The wire rule is the least obvious one. Substitution is per principal, so if the bound constant were sent, the recipient would go on naming a constant the sender no longer has.
sanity error: scenario names principal `Charlie`, which the model does not declare --> ns.vp:96:2 | 96 | Charlie[gpeer = gm] | ^^^^^^^^^^^^^^^^^^^ | = note: a scenario binds constants inside a principal that exists, so a name no principal carries would substitute nothing and silently analyze the model as written = help: declared principals: `Alice`, `Bob`, `Mallory`
The declared scenarios then travel into every output. The CLI prints the warning block shown further up, marking which peers are honest and which are corrupt. The same list reaches --format json, --format html and the language server, so a report or an editor shows the cast the verdicts were reached under.
Two limitations
Queries are not cloned per scenario. Sessions get per-session query variants; scenarios do not, so every query names the first scenario’s constants and an attack on nr@2 specifically is out of reach.
The honest run also seeds wire values from each principal’s untouched starting state. So a corrupt clone that halts partway through still lets the values it would have sent afterwards reach the attacker.
More of the classical corpus
Peer scenarios made a chunk of the standard benchmark set reachable, so three more protocols came over from Scyther’s SPORE corpus while we were in there: Otway-Rees, Wide-Mouth Frog and Yahalom. Needham-Schroeder now ships in both flavors, unfixed and Lowe-fixed, and neither ships a scenario-free variant, on purpose. A model that cannot state the attack it is named after teaches the wrong thing.
The verdict envelope
Verifpal now prints the conditions a search ran under alongside each pass:
Pass ✓ confidentiality? nr [search exhausted at 2 sessions]
Pass ✓ authentication? Bob -> Alice: data [search truncated: term depth]
Every result carries an envelope holding the session count and any reason the search declined to look further. There is one such reason so far, the term-depth bound, recorded at the same point that prints the notice about a declined branch. Across the whole test corpus only two models print truncated, so the qualifier carries real signal and does not decorate every line.
The envelope stamped on a result is the one in force at the end of the whole run, even when that particular verdict was recorded earlier. That is the conservative direction on purpose: a hold reached before a depth cut fired is still a hold reached inside a search that later stopped short.
“Exhausted” means the search space this engine defines was fully explored at these parameters. It does not mean no attack exists, and the wording stays away from “proof”, “verified” and “complete” on purpose, because Verifpal still carries narrowing sites that suppress real attacks and a completeness word here would be false. Attacks are never qualified this way: an attack is a witness and needs no caveat.
The envelope is serialized into the JSON report, shown on the HTML verdict row, and sent to the language server, so nothing downstream sees a bare pass any more.
--saturate
--saturate raises the session count from one upward and stops at the first count whose result code matches the previous count’s:
Info ● Verdicts were unchanged from 2 sessions through 3; analyzing at 3.
The output is the full analysis from the count it stopped at, with that count reported alongside. Each probe run is buffered while it happens, so the winning run is replayed from what it already produced and never analyzed twice.
It also refuses to overclaim. Hitting the ceiling without ever settling gets different wording: Verdicts were still changing at 4 sessions, the highest --saturate tries; analyzing there. Reporting that verdicts stopped changing when they never did would be a false claim about the protocol. And if an attack found at a lower session count vanishes at a higher one, that is a bug in Verifpal and the run says so. That invariant used to be something we re-ran by hand after engine changes.
This is evidence about the range that was searched, and the wording keeps it to that.
--auto-queries
--auto-queries throws away the model’s own queries block and generates one in its place. Three rules, applied after the model has been validated as written:
confidentiality?for everygeneratesand everyknows privateorknows passwordconstant that has a slot in the trace.authentication? S -> R: cfor every wire delivery whose recipient actually usescinside a primitive.freshness? cfor every constant that is genuinely sent and then used.
Each rule mirrors an existing sanity constraint, so a generated query can never be one the tool then rejects, and a corpus sweep holds that over every model that analyzes. unlinkability? and equivalence? are skipped, because both need a human to say which pair is interesting.
On a small test model it turns two written queries into eleven and reports a freshness failure on both long-term Diffie-Hellman public keys, which is correct and not very useful. The flag is there to explore a model you are still working on. The file on disk is never touched.
What shipped between 1.0 and 1.3
Authentication queries are now injective
Verifpal’s authentication query used to ask something weaker than its name suggested. The old rule: did the recipient end up using a value the named sender never sent? Forge something and the query failed, which is correct. But copy a message the sender really did send in one session and deliver it again somewhere else, and the old rule let it pass. Nothing had been forged, so nothing was reported, and replay attacks went unmentioned.
The new rule is injective agreement. For every time the recipient accepts a value, the sender has to have sent it a separate time. Alice sends once, Bob accepts twice: that is a failure even though the attacker made nothing up. There is no flag to turn it off.
Violating injectivity takes two runs. Verifpal analyzes two sessions of every principal by default, so it is in a position to see one, and the trace says exactly what happened:
Fail ✗ authentication? Alice -> Bob: ciphertext ╭─ Attack trace: │ 1. Attacker observes ciphertext#2 on the wire, where it is │ ENC(key, plaintext#2). │ 2. Attacker observes tag#2 on the wire, where it is │ MAC(key, ENC(key, plaintext#2)). │ 3. Attacker replays ciphertext (Alice to Bob) from another │ session, where it is ENC(key, plaintext#2). │ 4. Attacker replays tag (Alice to Bob) from another session, │ where it is MAC(key, ENC(key, plaintext#2)). │ 5. Bob's ASSERT(tag, tag)? passes — the attacker controls one │ of its inputs. ╰▸ ciphertext, which Alice sent in another session and not in this one, is successfully used within Bob's state: Alice sent it once, Bob accepts it twice, so agreement is not injective.
Twenty-four models in the test corpus flipped from pass to fail when this landed. We read every one of those traces to confirm each one is a genuine copied message.
Injective agreement also made TLS 1.3 resumption worth modelling, so tls13-0rtt.vp is new. RFC 9846 §2.3 names two ways 0-RTT early data is weaker than the rest of TLS: no forward secrecy, and no replay protection between connections. Both now appear as failures sitting next to holds for the 1-RTT traffic in the same file, against the same attacker:
Fail ✗ confidentiality? earlymsg Pass ✓ confidentiality? appmsg [search exhausted at 2 sessions] Fail ✗ authentication? Client -> Server: earlydata Pass ✓ authentication? Client -> Server: appdata [search exhausted at 2 sessions]
All four of those answers are claims RFC 9846 already makes about itself.
Three fixes to the solver
The solver can now forge structured ciphertexts. The attacker builds the fake encrypted flights it would need to impersonate a server, so Verifpal finds man-in-the-middle attacks on protocols shaped like TLS 1.3 that it used to miss.
It can now make two projections disagree. Mario Raso reported a completeness gap in equivalence queries: when both queried constants are halves of one bundle the attacker controls, the search never proposed a bundle whose halves differ. The cause: working out what shape would satisfy a SPLIT, the solver minted a separate free variable for each field, then filled every one of them with nil, and nil cannot disagree with itself. The fix gives each field its own value, drawn from a short ladder: nil, then HASH at every arity the specification declares. Divergence only needs the values to differ; which ones they are does not matter.
It can now assume a slot stays honest. Until now the search replaced every controllable slot with a variable, so the possibility that a slot is simply never touched could be guessed at but never reasoned about. Terms stopped reducing, the goals behind them were never generated, and guarding a wire could therefore be the thing that made an attack reachable, which is backwards. Holding one slot at its honest value while building terms fixes that, and it emptied the last remaining entry in the engine’s list of known missed attacks.
HTML and JSON reports
verify --format html renders a whole analysis as a single page: verdicts, an annotated protocol diagram, each attack trace drawn as a sequence diagram with the attacker’s own lane, and the model source syntax-highlighted with every query marked by its verdict. There are no external resources at all, so it opens identically offline and you can attach it to a review or mail it to a colleague. The full TLS 1.3 model comes out at 88 KB.
verify --format json emits the same report as machine-readable data, structured attack steps included. It replaces the old internal-json subcommand, which was never meant for humans and is now gone.
A language server
verifpal lsp speaks LSP over stdio: live diagnostics from parse and sanity errors, formatting, hover, completion, signature help, document symbols, definition, references, highlights, rename, folding, semantic tokens, inlay hints, code lenses, code actions, and a cancellable attacker analysis you can fire from the editor and watch report back.
The Visual Studio Code extension runs on it now, and there are two new ones: Neovim and Zed.
Tests
1.0 shipped with 441 tests over a corpus of 196 models. 1.3 has 824 tests over 360 models.
The bigger addition is a metamorphic harness. It transforms each model and asserts a relation between the two verdicts: remove a guard and no attack may disappear, add a leaks and no attack may disappear, alpha-rename every identifier and nothing may change at all. Twelve properties, several thousand comparisons. This catches the one thing every other check in the suite is blind to: a missed attack. For that question the tool’s own output cannot be its own oracle.
Two of the twelve properties are about peer scenarios. Binding a constant to itself has to expand to the model exactly as written, which is the no-op case for the whole front end, and adding a second copy of that scenario can only ever give the attacker more.
Both of the harness’s exception lists are currently empty. The missed-attack list held one entry, closed by the refinement search above. The bad-trace list held 28 entries across 18 models. All 28 traced back to four bugs.
Get it
brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install verifpal
Windows users can scoop install verifpal from the same repository, and there are release binaries for Windows, Linux, macOS and FreeBSD.
The paper has been renamed to From Toy to Instrument: Seven Years of Verifpal. It is the same eprint, and it remains the reference for what the engine covers and what it does not.