Documentation / Quickstart

Your first protocol analysis

Alice signs Bob’s challenge, and Bob checks the signature. This example shows how an attacker can still impersonate Alice if Bob has not authenticated her public key.

Open the model in Workbench Browse the language reference

The Workbench runs locally in your browser. To follow along in a terminal, install Verifpal first.

1. Write a model

A model is a text file ending in .vp. It starts with an attacker declaration, describes the principals and their messages, and ends with the properties you want to check.

Alice (left), the attacker (center), and Bob (right). Bob sends a fresh challenge; Alice keeps her signing key private.

quickstart.vp · complete model

attacker[active]

principal Alice[
	knows private sk
	pk = PUBKEY(sk)
]

principal Bob[
	generates challenge
]

Bob -> Alice: challenge

principal Alice[
	proof = SIGN(sk, challenge)
]

Alice -> Bob: pk, proof

principal Bob[
	_ = SIGNVERIF(pk, challenge, proof)?
]

queries[
	confidentiality? sk
	authentication? Alice -> Bob: proof
]

Download quickstart.vp

attacker[active]: The attacker can observe, intercept, replace and inject network values.
knows private sk: Alice starts with a private signing key. Bob’s generates challenge creates a fresh value for each of his sessions.
Alice -> Bob: pk, proof: The public key and signature cross the attacker-controlled network.
SIGNVERIF(...)?: The question mark makes the check mandatory: Bob stops if verification fails.

2. Run verification

In the Workbench, press Verify or Ctrl/⌘ + Enter. You can keep editing while analysis runs, or press Cancel to stop it. To use the command line, save the file and run:

verifpal verify quickstart.vp

The browser uses the default of two concurrent sessions per principal. With the command line, --sessions lets you choose a different count.

3. Read the verdicts

The result code is c0a1. Letters identify the query type in model order; 0 means no contradiction was found, and 1 means the query was contradicted.

Expected results for the unguarded model
Query	Result	Meaning
`confidentiality? sk`	No attack found	The attacker does not obtain Alice’s signing key in this search.
`authentication? Alice -> Bob: proof`	Attack found	Bob can successfully use a signature supplied by the attacker.

A pass means Verifpal found no attack within the reported search limits and assumptions. It does not prove that a deployed implementation is secure. See the results reference for details.

4. Inspect the attack

Bob verifies the signature with the public key that arrived beside it. Both values are unguarded. The attacker can replace the key with its own and sign Bob’s visible challenge using the matching private value.

Bob sends his challenge; the attacker observes it.
The attacker constructs a public key and a signature over that challenge.
It replaces Alice’s pk and proof on their way to Bob.
Bob’s signature check succeeds under the substituted key.

The trace shows what the attacker constructs and sends to Bob. You may see PUBKEY(nil): because nil is public, the attacker knows the input used as the private key. Alice’s own key remains secret.

5. Guard Alice’s public key

If the real system authenticates Alice’s public key to Bob before this exchange, express that assumption by guarding the key in the message:

Alice -> Bob: [pk], proof

Run the model again. The guarded version reports c0a0: neither query is contradicted in this search.

Run the guarded model Download the guarded model

A guard states a trust assumption; it does not implement key authentication. The attacker can still read the key. Use brackets only where the actual deployment ensures that the recipient receives the sender’s authenticated value.

Keep Bob’s checked signature verification. The trusted key identifies Alice, and the signature binds her response to Bob’s fresh challenge. Removing the ? changes the model to one that continues when verification fails.

Keep learning

Model structure: declarations, messages, guards and checked operations.
Security queries: confidentiality, authentication, freshness, equivalence and unlinkability.
All 25 primitives: argument order, output counts and supported assumptions.
Comparison: where Verifpal fits alongside ProVerif and Tamarin, and how to choose a tool.
Diffie–Hellman example: inspect a man-in-the-middle attack on key exchange.
Modeling guide: build a model and test its assumptions.
How analysis works: understand how Verifpal searches for attacks and checks them.
Protocol studies: Signal, Scuttlebutt and post-quantum key exchange.

For the full reading order, start with the introduction. Verifier source · Research paper