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 read 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 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, m1, HASH(galongterm, gblongterm, gae2))]Alice -> Bob: [galongterm], gae1, gae2, 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, e1, HASH(galongterm, gblongterm, gae2))?]queries[ confidentiality? m1 authentication? Alice -> Bob: e1]
Verifpal 1.0 deletes the beta warning that has headed every analysis since 2020, on the strength of a new paper: the modeling language now covers post-quantum key exchange, declared weakening assumptions and witness-based unlinkability, and the engine behind it comes with a soundness theorem that holds however the solver behaves, unconditional termination, and attack traces measured for readability against ProVerif and Tamarin.
Read the full announcementVerifpal 0.80.0 lets models declare cryptographic primitives as broken via weak and forgeable annotations instead of relying on approximations, and redesigns unlinkability queries to surface concrete link witnesses attackers can exhibit.
Read the full announcementVerifpal 0.70.0 removes Diffie-Hellman equations from the modeling language, adds a generic KEM for post-quantum and hybrid key exchange, and rebuilds the active attacker around a search that works backwards from each query instead of guessing forwards.
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, 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.verifpalThe restraint is deliberate, and it costs less than it sounds. Verifpal still models detailed protocols under an active attacker, and still answers queries for the properties people argue about: forward secrecy, key compromise impersonation, unlinkability, post-quantum key exchange. What it drops is the expressiveness that only ever paid off in a paper.
Signal, Scuttlebutt, TLS 1.3 and Telegram have all been modeled in it. The engine behind version 1.0 comes with a soundness theorem that holds however the solver behaves, and with unconditional termination. Verifpal is free and open source under the GPLv3.