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]
Verifpal 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 announcementVerifpal 1.4 closes four sources of false positives, including deliveries that no honest sender could have produced and attacks assembled from incompatible execution paths, and finds two classes of attack it previously missed: values forwarded unguarded across a guarded hop, and the 2007 Pi_Toy attack, which needs nested encryptions deeper than the honest protocol goes. AEAD_ENC and AEAD_DEC now take a nonce; knows password and PW_HASH are gone. Verdicts carry labels such as [attacker-supplied value] and [search exhausted at 2 sessions], and precondition now restricts a query to the executions in which the named message is sent.
Read the full announcementVerifpal 1.3 adds a scenarios[] block for assigning different peers to concurrent instances of a principal. This allows models to reproduce Lowe’s 1995 attack on Needham-Schroeder and distinguish the original protocol from Lowe’s correction. Query results now show session and term-depth limits. --saturate increases the session count until verdicts stabilize, and --auto-queries generates confidentiality, authentication and freshness queries.
Read the full announcementVerifpal 1.0 removes the beta warning introduced in 2020. It adds post-quantum key exchange, declared weakening assumptions and witness-based unlinkability. The accompanying paper presents a soundness theorem and a termination proof, and compares the readability of Verifpal attack traces with ProVerif and Tamarin.
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.