Verifpal 1.4.2 focuses on analysis correctness. It fixes several false positives caused by combining incompatible protocol runs, detects two previously missed attacks, and makes the precondition option behave as documented. It also adds labels to verdicts that need interpretation and removes knows password and PW_HASH from the language.
Most of the false positives had the same cause. Attacker knowledge in Verifpal is global and monotonic: once the attacker learns a value, it remains known for the rest of the analysis. That is appropriate for the attacker, but it does not make different executions of the same principal compatible. Earlier versions sometimes used a value learned by tampering with one run in another run where that tampering never occurred. Version 1.4.2 tracks where learned values came from and rejects these inconsistent combinations.
Scope of the audit
The audit began with seven known problem cases: three false reports, three missed attacks, and one correct but misleading verdict. Each case was reduced to a focused model and traced to the relevant part of the engine before being fixed. The changes were applied separately and checked against the full test corpus and the metamorphic harness.
Two results were also checked with other tools. Tamarin proves the property that the earlier engine incorrectly rejected in the incompatible-runs example, while ProVerif finds the Pi_Toy attack with two responder runs, as Verifpal now does. The audit also found related problems that were not in the original list.
Four false positives
Bob#2 is still Bob
attacker[active]
principal Alice[
knows private k
generates na
t1 = MAC(k, na)
]
Alice -> Bob: na, t1
principal Bob[
knows private k
_ = ASSERT(t1, MAC(k, na))?
generates nb
m2 = MAC(k, CONCAT(na, nb))
]
Bob -> Alice: nb, m2
principal Alice[
_ = ASSERT(m2, MAC(k, CONCAT(na, nb)))?
]
queries[
authentication? Bob -> Alice: m2
]Verifpal analyzes two sessions of each principal by default. The second copy is suffixed #2. Version 1.3.9 reported this model as follows:
Fail ✗ authentication? Bob -> Alice: m2 ╭─ Attack trace: │ 1. Attacker observes nb#2 on the wire. │ 2. Attacker replaced na#2 with na, t1#2 with t1, after which │ m2#2 resolved to MAC(k, CONCAT(na, nb#2)). │ 3. Attacker replaces m2 (sent by Bob to Alice) with │ MAC(k, CONCAT(na, nb#2)). (m2 was MAC(k, CONCAT(na, nb))) │ 4. Attacker replays nb (Bob to Alice) from another session, │ where it is nb#2. │ 5. Alice's ASSERT(MAC(k, CONCAT(na, nb#2)), MAC(k, CONCAT(na, nb#2)))? │ passes — the attacker controls one of its inputs. ╰▸ m2 (MAC(k, CONCAT(na, nb#2))), sent by Attacker and not by Bob, is successfully used in ASSERT(m2, MAC(k, CONCAT(na, nb)))? within Alice's state.
The trace does not contain a forgery. The attacker routes Alice’s authenticated challenge to Bob#2 instead of Bob, then sends Bob#2’s response back to Alice. Bob#2 is another run of the same principal and computes the MAC with Bob’s key. The attacker never learns k, and each accepted message has one matching Bob run, so injective agreement holds.
Version 1.3.9 classified any unexpected delivered value as attacker-sent. This made message routing look like forgery. Version 1.4.2 also checks for a matching sender run. It reruns the declared sender with the messages supplied by the recipient and checks whether that run produces the exact delivered value. If it does, the value remains attributed to the sender.
This exception does not apply when the attacker can construct the value independently. Before accepting a matching run, the engine removes everything observed from the sender’s runs and tries the derivation again. If it still succeeds, the value is treated as forged. The unguard metamorphic test caught an earlier version of this check that incorrectly excused a tag forged with a leaked key. Six regression models cover valid matching runs, and five more cover cases that must still fail, including leaked keys, attacker-built terms, and senders that halt before sending.
Incompatible runs
attacker[active]
principal Alice[
knows private msg
generates a
generates na
ga = PUBKEY(a)
]
principal Bob[
generates b
gb = PUBKEY(b)
]
Alice -> Bob: [ga]
Bob -> Alice: gb
principal Alice[
ka = DH_KEX(gb, a)
e = ENC(ka, na)
c = AEAD_ENC(na, msg, nil)
]
Alice -> Bob: e, c
principal Bob[
kb = DH_KEX(ga, b)
n = DEC(kb, e)
p = AEAD_DEC(n, c, nil)?
h = HASH(p)
]
queries[
authentication? Alice -> Bob: c
]Alice’s Diffie-Hellman share is guarded in transit; Bob’s is not. Alice encrypts a nonce with the shared key, then uses the nonce to seal a message. Bob recovers the nonce, opens the message, and hashes it.
The attacker has two incompatible choices for gb. If it delivers the honest value, Bob can decrypt e, but the attacker cannot and therefore never learns na. If it replaces gb with PUBKEY(nil), the attacker can derive Alice’s key and learn na, but Alice then encrypts e under a key Bob does not have. Bob cannot recover na, so a forged c encrypted under that nonce will not open. Version 1.3.9 combined na from the second execution with Bob’s unmodified e from the first:
Fail ✗ authentication? Alice -> Bob: c ╭─ Attack trace: │ 1. Attacker replaces c (sent by Alice to Bob) with │ AEAD_ENC(na, nil, nil). (c was AEAD_ENC(na, msg, nil)) │ 2. Bob's AEAD_DEC(n, AEAD_ENC(na, nil, nil), nil)? passes — the │ attacker controls one of its inputs. ╰▸ c (AEAD_ENC(na, nil, nil)), sent by Attacker and not by Alice, is successfully used in AEAD_DEC(n, c, nil)? within Bob's state.
The same protocol was checked in Tamarin, which proves that the query holds with one run per role. Extra sessions do not create the reported attack: na#2 is a different value, and the guard ties Bob#2 to Alice#2’s share. Version 1.4.2 reports that the query holds after exhausting the search at two sessions.
The engine now records what a sender would produce in an unmodified run for every received message. When the attacker tries to deliver a value learned in a run where that sender produced something different, the delivery is rejected. If the secret was exposed through a message to another principal, the engine reruns the sender with the original tampering and compares the results.
A companion regression model leaks the sealing key directly. In that case, learning the nonce does not change what Bob receives, so the forged ciphertext is a real attack and remains reported.
The same inconsistency could occur entirely within the attacker’s deductions, without another message delivery. The regression case is the shipped hybrid post-quantum handshake with one weakening annotation removed. The attacker learns Bob’s KEM seed only when Bob receives the attacker’s key, while Alice seals her payload only when Bob receives the honest key. The old engine combined the seed from the first run with the payload from the second and derived the honest session key.
When a deduction now combines facts from different runs, the engine replays a single run containing all the required tampering. It accepts the deduction only if every supporting fact is still reachable. The check tests reachability, not equality of the resulting values; requiring equal values caused four real attacks to be missed. A combination is also rejected if two facts require different values at the same point in one principal, or if the combined run cannot execute.
If ga is unguarded in the model above, the two parts of the attack apply to different principals. That is a valid man-in-the-middle attack, and Verifpal still reports it.
Messages used before they are sent
Within a phase, Verifpal made every message available to the attacker before running any principal. This allows traffic to be routed between sessions regardless of the order in which blocks are written. For an active attacker, however, it also allowed cyclic traces: a later message could satisfy an earlier check even when that later message was sent only after the check passed. This caused a false failure in the shipped Secure Scuttlebutt handshake model:
Fail ✗ authentication? Bob -> Alice: secretbox1bob ╭─ Attack trace: │ 1. Attacker observes secretboxm2bob on the wire, where it is │ AEAD_ENC(mastersecret2bob, m2, nil). │ 2. Attacker replaces secretbox1bob (sent by Bob to Alice) with │ AEAD_ENC(mastersecret2bob, m2, nil). (secretbox1bob was │ AEAD_ENC(mastersecret2bob, sig2bob, nil)) │ 3. Alice's AEAD_DEC(mastersecret2alice, AEAD_ENC(mastersecret2bob, │ m2, nil), nil)? passes — the attacker controls one of its inputs. │ [seven derivation steps omitted] │ Note: these are the substitutions the search recorded; no subset of │ them was confirmed to reproduce the violation on its own, so this │ trace is not a minimized witness. ╰▸ secretbox1bob (AEAD_ENC(mastersecret2alice, m2, nil)), sent by Attacker and not by Bob, is successfully used in AEAD_DEC(mastersecret2alice, secretbox1bob, nil)? within Alice's state.
Alice derives her master secret through Bob’s guarded long-term key, so only Bob can produce a ciphertext that opens under it. The trace uses secretBoxM2Bob, which Bob sends two messages later and only after Alice has accepted the earlier message and replied. The value needed at that point in the trace does not yet exist.
For each modified delivery, version 1.4.2 computes which later values depend on that delivery. This includes the recipient’s later work and any work triggered in other principals by the recipient’s later messages. Knowledge derived from those future values cannot be used for the current delivery. The check follows the origin of each value rather than comparing it with an honest execution, because a future value may itself depend on tampering. Values that the attacker can construct from information already available remain valid.
This change affects two verdicts in the corpus: the dedicated regression model and the Scuttlebutt query above. The Scuttlebutt server-authentication query is now the first of that model’s five authentication queries to pass.
A shared secret is not a ciphertext
Fail ✗ confidentiality? ksc_m ╭─ Attack trace: │ 1. Attacker is handed ksc_ss2 by a leaks declaration. │ 2. Attacker replaces ksc_ct1 (sent by Bob to Alice) with ksc_ss2. │ (ksc_ct1 was KEM_ENCAP(ksc_pk, ksc_r1)|2) │ 3. Alice's KEM_DECAP(ksc_sk, ksc_ss2)? passes — the attacker │ controls one of its inputs. │ 4. Attacker observes ksc_e on the wire. │ 5. Attacker opens ksc_e with ksc_ct1, obtaining ksc_m. ╰▸ ksc_m (ksc_m) is obtained by Attacker.
In step 3, Alice decapsulates a shared secret as though it were a ciphertext. KEM_ENCAP returns two values: a shared secret and a ciphertext. The old KEM_DECAP rule checked the key but did not check which output occupied the ciphertext position. An attacker could therefore replace Bob’s ciphertext with Charlie’s leaked shared secret. Alice would accept it and derive a key the attacker already knew, even though a KEM does not allow an attacker to choose a ciphertext that decapsulates to a selected secret.
Primitive rules can now specify which output of a multi-output primitive they accept. A companion model confirms that replaying a leaked ciphertext into the same slot still breaks the query.
The inverse error also existed. With the private key, a party can open an ML-KEM ciphertext and recover the shared secret and the randomness used to produce it, because ML-KEM’s re-encryption check derives that randomness again. The rule applies only to the ciphertext. Applying it to the shared secret incorrectly allowed a leaked secret and private key to reveal the randomness.
Two previously missed attacks
Forwarding through guarded messages
Square brackets around a message value prevent the attacker from changing that value in transit. Before 1.4.2, the engine also treated the guard as a constraint on how the sender could have computed the value. That interpretation missed two kinds of attack.
In the first case, Alice sends a fresh value to Bob without a guard. Bob and Carol then forward it to Dave over two guarded links. The attacker can replace the value on the first link and thereby control what Dave receives, without modifying either guarded message. In the second case, Carol sends a nonce to Alice without a guard. Alice authenticates it with a MAC under a secret key and sends the tag to Bob with a guard. The attacker cannot construct or directly inject MAC(k, nil), but it can give Alice nil and let Alice compute and send the tag. The previous search, which reran only one principal at a time, could not represent either sequence.
Reruns now propagate through the protocol. After rerunning the principal affected by tampering, the engine delivers that principal’s changed messages to their recipients, reruns those recipients, and continues until the state stops changing. Only messages that differ from the honest execution are propagated. A forwarded value keeps its actual sender, because that principal computed and sent it:
Pass ✓ authentication? Alice -> Bob: fen_tag [search exhausted at 2 sessions] Fail ✗ freshness? fen_tag ╭─ Attack trace: │ 1. No value fen_tag is built from is generated fresh: fen_k, nil. │ 2. Attacker replaces fen_n (sent by Carol to Alice) with nil. │ 3. Attacker observes MAC(fen_k, nil) on the wire. ╰▸ fen_tag (MAC(fen_k, nil)) is used by Bob in fen_h despite not being a fresh value.
The tag is not fresh, but Alice is still its sender. Attributing propagated values to the attacker would create false authentication failures, so a regression test checks that propagation does not change sender attribution.
Pi_Toy, from 2007
In 2007, Myrto Arapinis and Marie Duflot showed that attacks against a class of well-formed protocols can be found using messages no larger than those sent by the protocol itself (Bounding Messages for Free in Security Protocols, FSTTCS 2007). Their paper also gives a deliberately ill-formed counterexample, ΠToy, in which the attack requires a message larger than any honest message. Verifpal is intentionally untyped so that it can find type-confusion attacks, which means the theorem does not apply. Its previous depth bound excluded the Pi_Toy attack.
attacker[active]
principal Alice[
knows private a
ga = PUBKEY(a)
generates n
]
principal Bob[
knows private b
gb = PUBKEY(b)
]
principal Mallory[
knows private m
gm = PUBKEY(m)
generates x
leaks m
]
Alice -> Bob: [ga]
Bob -> Alice: [gb]
Bob -> Mallory: [gb]
Mallory -> Bob: [gm]
principal Alice[
inner_a = PKE_ENC(gb, n)
pair_a = CONCAT(inner_a, ga)
m1 = PKE_ENC(gb, pair_a)
]
Alice -> Bob: m1
principal Mallory[
inner_in = PKE_ENC(gb, x)
pair_in = CONCAT(inner_in, gm)
m_in = PKE_ENC(gb, pair_in)
]
Mallory -> Bob: m_in
principal Bob[
outer_b = PKE_DEC(b, m_in)
inner_b, peer_b = SPLIT(outer_b)?
x_b = PKE_DEC(b, inner_b)
inner_r = PKE_ENC(peer_b, x_b)
pair_r = CONCAT(inner_r, gb)
m2 = PKE_ENC(peer_b, pair_r)
]
Bob -> Mallory: m2
queries[
confidentiality? n
]Alice encrypts her nonce for Bob, pairs that ciphertext with her public key, and encrypts the pair for Bob again. Bob removes the outer encryption, decrypts the inner ciphertext, and returns the nonce encrypted to the public key contained in the pair. Mallory is a legitimate participant whose private key has leaked.
For the attack, Mallory pairs Alice’s complete m1 message with the attacker’s public key, encrypts the pair for Bob, and sends it as m_in. Bob removes one layer from Alice’s message and returns the result encrypted to the attacker. A second Bob run removes the remaining layer. The injected message has depth five, while the deepest honest protocol term has depth three.
Fail ✗ confidentiality? n ╭─ Attack trace: │ 1. Attacker observes gb on the wire. │ 2. Attacker observes m1 on the wire. │ 3. Attacker constructs PUBKEY(nil). │ 4. Attacker constructs CONCAT(m1, PUBKEY(nil)). │ 5. Attacker constructs PKE_ENC(gb, CONCAT(m1, PUBKEY(nil))). │ 6. Attacker replaces m_in (sent by Mallory to Bob) with │ PKE_ENC(gb, CONCAT(m1, PUBKEY(nil))). (m_in was PKE_ENC(gb, │ pair_in)) │ 7. Attacker observes PKE_ENC(PUBKEY(nil), │ CONCAT(PKE_ENC(PUBKEY(nil), pair_a), gb)) on the wire. │ 8. Attacker opens PKE_ENC(PUBKEY(nil), │ CONCAT(PKE_ENC(PUBKEY(nil), pair_a), gb)) with nil, obtaining │ CONCAT(PKE_ENC(PUBKEY(nil), pair_a), gb). │ 9. Attacker splits CONCAT(PKE_ENC(PUBKEY(nil), pair_a), gb) and │ takes PKE_ENC(PUBKEY(nil), pair_a). │ 10. Attacker opens PKE_ENC(PUBKEY(nil), pair_a) with nil, │ obtaining pair_a. │ 11. Attacker splits pair_a and takes inner_a. │ 12. Attacker constructs CONCAT(inner_a, PUBKEY(nil)). │ 13. Attacker constructs PKE_ENC(gb, CONCAT(inner_a, │ PUBKEY(nil))). │ 14. Attacker replaces m_in#2 (sent by Mallory#2 to Bob#2) with │ PKE_ENC(gb, CONCAT(inner_a, PUBKEY(nil))). (m_in#2 was │ PKE_ENC(gb#2, pair_in#2)) │ 15. Bob#2's SPLIT(outer_b#2)? passes — the attacker controls one │ of its inputs. │ 16. Attacker observes PKE_ENC(PUBKEY(nil), │ CONCAT(PKE_ENC(PUBKEY(nil), n), gb)) on the wire. │ 17. Attacker opens PKE_ENC(PUBKEY(nil), │ CONCAT(PKE_ENC(PUBKEY(nil), n), gb)) with nil, obtaining │ CONCAT(PKE_ENC(PUBKEY(nil), n), gb). │ 18. Attacker splits CONCAT(PKE_ENC(PUBKEY(nil), n), gb) and takes │ PKE_ENC(PUBKEY(nil), n). │ 19. Attacker opens PKE_ENC(PUBKEY(nil), n) with nil, obtaining n. ╰▸ n (n) is obtained by Attacker.
Step 5 builds the injected message, Alice’s complete m1 paired with the attacker’s public key and sealed for Bob, and step 6 delivers it in place of m_in. The fix has two parts:
-
The depth limit is now calculated per message. It starts with the protocol’s maximum term depth and adds the number of layers the recipient removes from that message. The extra depth can only contain terms already produced by the protocol, so it does not allow arbitrary new structures.
-
When a forged message contains a ciphertext slot, the search now tries each ciphertext the attacker knows under the same key. Increasing the depth limit alone was insufficient because the search did not previously propose this nested form.
The attack requires two responder runs in both Verifpal and ProVerif. With --sessions 1, confidentiality of the nonce remains unrefuted. The default two sessions find the attack.
Verdict labels
Version 1.4.2 adds three qualifiers to help distinguish different kinds of failed verdict.
[duplicate acceptance] marks a replay the recipient could have detected because the accepted value contains a nonce or key generated by that recipient. [duplicate acceptance: no recipient-generated context] marks a replay of an initial message to which the recipient contributed nothing, so separate recipient runs will accept the same message. An Info line explains the distinction once per query:
Info ● authentication? Bob -> Alice: e reports a duplicate that Alice cannot rule
out on its own: it contributes nothing to e before accepting it, so any
run of it takes the same message twice. Read it as a replay-protection
question about this flight rather than as a forgery.
The shipped corpus contains 87 such verdicts across 66 models. Suppressing initial-message replays would hide 40 of them, including the TLS 0-RTT replay in tls13-0rtt.vp that RFC 9846 explicitly identifies. Continuing the search after finding a duplicate did not change any verdicts and made three traces harder to minimize. Duplicate acceptance therefore remains a query failure, but the label explains how to interpret it. Running with --sessions 1 can help determine whether the result depends only on a cross-session replay.
[attacker-supplied value] marks a confidentiality failure over a value the attacker put there:
Fail ✗ confidentiality? cas_d [attacker-supplied value] ╭─ Attack trace: │ 1. Attacker observes cas_gb on the wire. │ 2. Attacker constructs PKE_ENC(cas_gb, nil). │ 3. Attacker replaces cas_c (sent by Alice to Bob) with │ PKE_ENC(cas_gb, nil). (cas_c was PKE_ENC(cas_gb, cas_m)) ╰▸ cas_d (nil) is obtained by Attacker, but that is the value the attacker put there: it carries nothing Bob generated or holds privately, so the honest cas_d is not shown to be disclosed. Pass ✓ confidentiality? cas_m [search exhausted at 2 sessions]
The failure remains valid because Bob computes with a value chosen by the attacker. The label clarifies that the result does not disclose the honest value of cas_d: the disclosed term contains nothing Bob generated or held privately. The underlying secret cas_m remains confidential. No other model in the shipped corpus currently receives this label. All three qualifiers are included in JSON reports as a subtype field, in HTML reports, and in language-server results.
Correct precondition semantics
The manual defines precondition as restricting a query to executions in which a later message is sent. Earlier versions evaluated the unrestricted query and only noted whether the later message was sent. Version 1.4.2 implements the documented behavior.
A query with precondition[P -> T: d] fails only when the query fails and P still sends d to T. In other words, the property must hold before P sends d. This makes it possible to express secrecy or agreement only for accepted sessions. The manual now includes this handshake example:
attacker[active]
principal Server[
knows private server_sk
server_pk = PUBKEY(server_sk)
]
Server -> Client: [server_pk]
principal Client[
generates c
gc = PUBKEY(c)
]
Client -> Server: gc
principal Server[
generates s
gs = PUBKEY(s)
sig = SIGN(server_sk, gs)
k_server = DH_KEX(gc, s)
]
Server -> Client: gs, sig
principal Client[
k_client = DH_KEX(gs, c)
_ = SIGNVERIF(server_pk, gs, sig)?
generates request
req = AEAD_ENC(k_client, request, nil)
]
Client -> Server: req
principal Server[
_ = AEAD_DEC(k_server, req, nil)?
]
queries[
confidentiality? k_client
confidentiality? k_client[
precondition[Client -> Server: req]
]
]As in TLS and Noise, the client derives the session key before verifying the server’s signature. It sends the encrypted request only after the signature check passes:
Fail ✗ confidentiality? k_client ╭─ Attack trace: │ 1. Attacker constructs PUBKEY(nil). │ 2. Attacker replaces gs (sent by Server to Client) with │ PUBKEY(nil). (gs was PUBKEY(s)) │ 3. Attacker observes gc on the wire. │ 4. Attacker constructs DH_KEX(gc, nil). ╰▸ k_client (DH_KEX(PUBKEY(nil), c)) is obtained by Attacker. Pass ✓ confidentiality? k_client[precondition[Client -> Server: req]] [search exhausted at 2 sessions]
The first query fails because the attacker can substitute its own share and make the client derive a known key. The client then stops at the signature check and never uses that key. The preconditioned query considers only executions in which the client sends req. In those executions the signature has verified, gs came from the server, and the session key remains secret. Version 1.3.9 failed both queries. Previously, the closest alternative was to query a value created after the check, such as request, and separately infer that the result also applied to the key.
Any of the five query kinds can have one or more preconditions. A precondition refers to the send event itself; delivery and sender authentication are separate properties. When a preconditioned query fails, the trace states that the required send still occurred:
Fail ✗ authentication? Bob -> Alice: e[precondition[Alice -> Carol: m2]] [duplicate acceptance: no recipient-generated context] ╭─ Attack trace: │ 1. Attacker observes e#2 on the wire, where it is ENC(psk, m#2). │ 2. Attacker replays e (Bob to Alice) from another session, where │ it is ENC(psk, m#2). │ 3. Attacker observes MAC(psk, ENC(psk, m#2)) on the wire. │ 4. Attacker observes MAC(psk, ENC(psk, m)) on the wire. ╰▸ e (ENC(psk, m#2)), which Bob sent in another session and not in this one, is successfully used in ASSERT(MAC(psk, e), h) within Alice's state: Bob sent it once, Alice accepts it twice, so agreement is not injective. ▲ Alice still sends m2 to Carol, so the failure counts.
Because a precondition restricts the executions being checked, adding one cannot introduce a new attack. The metamorphic harness now verifies this with a thirteenth property, restrict, which adds the model’s final message as a precondition to every query. Invalid preconditions are reported as sanity errors. This includes messages that are never sent, incorrect senders, self-addressed messages, and undeclared principals:
sanity error: Alice never sends `e` to Carol --> err_precondition_never_sent.vp:32:32 | 32 | precondition[Alice -> Carol: e] | ^ | = note: a precondition names a message the model sends, so that the query is evaluated only in executions where `e` goes out from Alice to Carol = help: add `Alice -> Carol: e` to the model, or name a message it already sends
This is a semantic change. Existing models with preconditions may stop reporting failures that occur only outside the executions selected by those preconditions.
Passwords are gone
knows password declared a guessable value. Values derived from it with ordinary primitives were treated as vulnerable to offline guessing unless the password first passed through PW_HASH, which represented a slow salted hash such as scrypt or Argon2. The feature was removed because its syntax was awkward, its formal model was inconsistent, and it saw little use.
The main problem was the model of offline guessing. Verifpal tried to recompute the complete term containing the password and compare it with a value already known to the attacker. Results therefore depended on unrelated details of the model. In the shipped HPKE pre-shared-key model, a PSK declared as a password remained safe when it appeared beside an unknown plaintext inside an AEAD, because the attacker had no known value against which to check a guess. Making the plaintext public immediately exposed the password. A real attacker could check the guess using the AEAD authentication tag, but the abstraction could not express that behavior.
Use knows private instead to model a successfully stretched password. The Userbase, Firefox Sync, and HPKE PSK models have been updated accordingly. In the revised Userbase model, all four queries pass with one session. With two sessions, both authentication queries fail because a new device can receive and accept stored blobs and salts from the other run of the same user’s key hierarchy. This is a cross-session replay that the previous password handling obscured.
Models that use the old syntax now receive a parse error:
parse error: unknown qualifier `password` --> err_unknown_qualifier.vp:11:8 | 11 | knows password pw | ^^^^^^^^ | = note: `knows` takes one of `private` or `public`
PW_HASH is also rejected as an unknown primitive, with the nearest known name suggested. The manual, Workbench, and extensions for Visual Studio Code, Zed, and Neovim no longer include either keyword.
Get it
brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install verifpal
Windows users can install Verifpal with scoop install verifpal from the same repository. Release binaries are available for Windows, Linux, macOS, and FreeBSD.