Built around the person writing the model.
Protocol verification tools have grown more expressive with every paper, and harder to pick up with every release. Most end up used by the group that built them and almost nobody else. Verifpal goes the other way: a small language you can read out loud, an active attacker, and output that names the attack instead of leaving you to reconstruct it.
attacker[active]principal Alice[ knows private alongterm galongterm = PUBKEY(alongterm)]principal Bob[ knows private blongterm, bs generates bo gblongterm = PUBKEY(blongterm) gbs = PUBKEY(bs) gbo = PUBKEY(bo) gbssig = SIGN(blongterm, gbs)]// The prekey bundle. In signal.vp this line reads [gblongterm].Bob -> Alice: gblongterm, gbssig, gbs, gboprincipal Alice[ _ = SIGNVERIF(gblongterm, gbs, gbssig)? generates ae1, ae2, m1, n_e1 gae1 = PUBKEY(ae1) gae2 = PUBKEY(ae2) amaster = HASH(DH_KEX(gbs, alongterm), DH_KEX(gblongterm, ae1), DH_KEX(gbs, ae1), DH_KEX(gbo, ae1)) ark, ack = HKDF(amaster, DH_KEX(gbs, ae2), nil) akenc = HKDF(nil, MAC(ack, nil), nil) e1 = AEAD_ENC(akenc, n_e1, m1, HASH(galongterm, gblongterm, gae2))]Alice -> Bob: [galongterm], gae1, gae2, n_e1, e1principal Bob[ bmaster = HASH(DH_KEX(galongterm, bs), DH_KEX(gae1, blongterm), DH_KEX(gae1, bs), DH_KEX(gae1, bo)) brk, bck = HKDF(bmaster, DH_KEX(gae2, bs), nil) bkenc = HKDF(nil, MAC(bck, nil), nil) m1_d = AEAD_DEC(bkenc, n_e1, e1, HASH(galongterm, gblongterm, gae2))?]queries[ confidentiality? m1 authentication? Alice -> Bob: e1]
Thirteen models, following ICAO Doc 9303 Part 11 and BSI TR-03110 Part 1, examine how an electronic passport protects its data. If the printed MRZ leaks after an inspection, Verifpal decrypts a recorded BAC session but not a PACE one, and an eavesdropper can link two BAC recordings of the same passport. Passive Authentication accepts genuine signed data supplied by the attacker, Active Authentication rejects a copied chip but not a relayed signature, and Terminal Authentication keeps fingerprints private only when the reader signs its Chip Authentication key. A dishonest website can relay a remote Active Authentication challenge to a bank; binding the signature to the verifier removes that attack at one session, and at two Verifpal finds a different one in the model’s simplified phone–bank connection.
Read the full announcementVerifpal 1.5 is about the correctness of the verifier itself. An audit carried out with frontier AI models found false attack reports, missed attacks, a crash and explanations the trace did not support, and added 39 regression models. Each value the attacker learns now records the executions that can produce it, so a disclosure can no longer be assembled from incompatible runs. The engine also stops publishing messages whose inputs never arrived, finds attacks that replace a value for only one of its recipients, and treats two THRESHOLD_SPLIT calls on the same secret as independent sharings. Findings the audit left open are listed in the announcement.
Read the full announcementVerifpal 1.4.6 analyzes a TLS 1.3 model covering mutual certificate authentication, application records, session tickets and KeyUpdate. With two concurrent sessions per principal and an active attacker, sixteen of nineteen queries find no attack and three produce expected confidentiality counterexamples. The walkthrough shows how authentication preconditions, compromised peers and timed key disclosures explain those results, with the full model and attack traces available in the generated report. Passing verdicts describe an incomplete search at the stated session bound.
Read the full announcementVerifpal 1.4.4 models threshold cryptography directly. THRESHOLD_SPLIT[n] replaces the fixed SHAMIR_SPLIT and produces up to sixteen shares for any threshold, THRESHOLD_SIGN produces a partial signature from one share, and THRESHOLD_JOIN reconstructs by symbolic Lagrange interpolation once enough distinct partials agree on their commitments and message. Reusing a nonce with the same share hands that share to the attacker, which is how the worked model forges a signature across a 3-of-5 boundary from one leaked share and two partials from an oracle.
Read the full announcement
The language reads close to how you would describe a protocol out loud to a colleague, while staying precise enough to analyze. Principals know things, generate things and send them to each other.
Alice -> Bob: e
You cannot define your own cryptographic primitives. Verifpal ships the functions instead, which takes an entire class of modeling mistakes off the table before analysis starts.
e = AEAD_ENC(k, n, m, ad)
When a query fails, Verifpal describes the attack in the protocol’s own terms: who sent what, what the attacker put in its place, and why nobody noticed the swap.
× authentication? Alice -> Bob: e
The Visual Studio Code extension highlights syntax, runs the queries as you type and draws the protocol as a diagram, so the analysis keeps up with the model while you are still writing it.
code --install-extension symbolicsoft.verifpalVerifpal models protocols against an active network attacker. It checks confidentiality, authentication, freshness, equivalence and unlinkability. Models can express forward secrecy, key-compromise impersonation, declared primitive failures and classical, post-quantum or hybrid key exchange.
Verifpal has been used to model Signal, Scuttlebutt, TLS 1.3 and Telegram. The version 1.0 paper formalizes its syntax, semantics and analysis, proves soundness independently of solver behavior, and proves unconditional termination. The software is free and open source under the GPLv3.