Cryptographic protocol verification

Verifpal®

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.

Try it in your browser Download Verifpal View source
signal-unguarded.vp verifpal analysis 
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]
confidentiality? m1 Contradiction found The attacker substitutes its own identity key and a prekey signed by that key. Alice accepts the signature, so the four X3DH secrets are derived using keys controlled by the attacker.
authentication? Alice → Bob: e1 Holds Bob’s checked decryption fails because Alice encrypted the message with a key derived from the attacker’s input. Bob therefore accepts no message.
Attack trace
| 1.Attacker constructs PUBKEY(nil) from nil.
| 2.Attacker constructs SIGN(nil, PUBKEY(nil)) from nil, PUBKEY(nil).
| 3.Attacker replaces gblongterm, gbs, gbo, gbssig (sent by Bob to Alice) with PUBKEY(nil), PUBKEY(nil), PUBKEY(nil), SIGN(nil, PUBKEY(nil)).
| 4.Alice’s SIGNVERIF(gblongterm, gblongterm, gbssig)? passes — its inputs are attacker-controlled.
| 5.Attacker observes e1 on the wire.
| 6.Attacker observes galongterm on the wire.
| 7.Attacker constructs DH_KEX(gblongterm, alongterm) from galongterm, nil.
| 8.Attacker observes gae1 on the wire.
| 9.Attacker constructs DH_KEX(gblongterm, ae1) from gae1, nil.
| 10.Attacker constructs amaster from DH_KEX(gblongterm, alongterm), DH_KEX(gblongterm, ae1), DH_KEX(gblongterm, ae1), DH_KEX(gblongterm, ae1).
| 11.Attacker observes gae2 on the wire.
| 12.Attacker constructs DH_KEX(gblongterm, ae2) from gae2, nil.
| 13.Attacker constructs ack from amaster, DH_KEX(gblongterm, ae2), nil.
| 14.Attacker constructs MAC(ack, nil) from ack, nil.
| 15.Attacker constructs akenc from nil, MAC(ack, nil), nil.
| 16.Attacker opens e1 with akenc, obtaining m1.
>m1 (m1) is obtained by Attacker.
Guarding gblongterm with brackets makes both queries hold. Read a full report Run this model yourself

Latest news

All announcements
  1. 1.3.0

    Verifpal 1.3: Who Alice Thinks She’s Talking To

    Verifpal 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 announcement
  2. 1.0

    Verifpal Reaches 1.0: A Toy Becomes an Instrument

    Verifpal 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
  3. 0.80.0

    Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability

    Verifpal 0.80.0 adds weak and forgeable annotations for declaring broken cryptographic primitives. Unlinkability queries now report concrete witnesses.

    Read the full announcement
  4. 0.70.0

    Post-Quantum Key Exchange, and an Attacker That Works Backwards

    Verifpal 0.70.0 replaces Diffie-Hellman equations with DH_KEX, adds a generic KEM for post-quantum and hybrid key exchange, and changes the active-attacker analysis to search backward from each query.

    Read the full announcement

Four design decisions

Read the manual

An intuitive protocol modeling language

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

Modeling that avoids user error

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)

Analysis output you can act on

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

Analysis inside your editor

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.verifpal

What Verifpal covers

Verifpal 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.