Your first protocol analysis

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.

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.

A passing query describes the explored search under its stated session bound and assumptions. Read the search limits beside the verdict; a pass is not an unbounded proof that a deployed implementation is secure. The results reference explains the scope.

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.

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

The trace shows the constructed terms and the replaced delivery. You may see PUBKEY(nil): nil is a public value, so the attacker knows the corresponding private input. Alice’s own key remains secret throughout.

5. State how Bob trusts Alice’s 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.

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.
• Diffie–Hellman example: inspect a man-in-the-middle attack on key exchange.
• Full user manual (PDF): detailed semantics, analysis limits and protocol walkthroughs.

This walkthrough uses the manual’s first protocol and guarded variant. Verifier source · Research paper