Documentation / Modeling a protocol

Modeling a protocol

Build a protocol model from its participants, knowledge, messages, phases and peer scenarios.

This guide starts with an unauthenticated Diffie–Hellman exchange, compares passive and active attackers, then adds honest and malicious peers. For declarations and syntax, see the language reference.

A modeling workflow

Write down the security claim, then build the smallest model that can test it:

1. State the setting. Name the participants, trusted channels, pre-established keys and attacker capabilities. Distinguish an outside network attacker from a malicious participant with valid credentials.

2. Write the honest exchange. Give each key and message a descriptive name. Use knows private for shared long-term state and generates for a new value in each run. Write the checks in the order the implementation performs them.

3. Check the baseline. Run the model and fix parser or sanity errors. If an honest check fails, compare the arguments on both sides before changing the security assumptions.

4. Write the queries. Query the original secret for disclosure and the received field for authentication. If a claim depends on completing a later send, use that send as a precondition. Use --auto-queries to find questions you may have missed, then keep the ones relevant to your security claims.

5. Read every failure. Identify whether it is a disclosure, a chosen replacement, a duplicate acceptance, a static value or a disagreement between terms. Check whether the real protocol permits every step.

6. Test the dependencies. Change one assumption at a time: remove a guard, remove a check, leak a key, vary the peer or increase the session count. Record the variant and why its result should differ.

7. Keep a reproducible record. Save the model, Verifpal version, command, session count and complete report together. The result code alone does not record the assumptions or search limits.

A query may correctly fail for a replayable opening message, a deliberately public value or a discarded session key. Check whether the failure violates a requirement of the protocol. If it does, repair the protocol; otherwise, explain why that query is not a required guarantee.

A first protocol

Alice and Bob exchange public keys and derive a shared secret. Bob encrypts a message for Alice. Download the complete simple.vp model or follow the protocol and queries below.

attacker[active]

principal Alice[
	generates a
	ga = PUBKEY(a)
]

Alice -> Bob: ga

principal Bob[
	knows private m1
	generates b, n1
	gb = PUBKEY(b)
	ss_a = DH_KEX(ga, b)
	e1 = AEAD_ENC(ss_a, n1, m1, gb)
]

Bob -> Alice: gb, n1, e1

principal Alice[
	ss_b = DH_KEX(gb, a)
	e1_dec = AEAD_DEC(ss_b, n1, e1, gb)?
]

Alice sends ga; Bob combines it with his private b to derive ss_a. He encrypts m1 and returns gb, the nonce and ciphertext. Alice derives the matching ss_b and performs a checked decryption, using Bob’s public key as associated data.

What the queries reveal

The queries ask whether the attacker can obtain the ciphertext or plaintext, whether Alice authenticates Bob as the source of the ciphertext, and whether Alice and Bob derive equivalent shared secrets:

queries[
	confidentiality? e1
	confidentiality? m1
	authentication? Bob -> Alice: e1
	equivalence? ss_a, ss_b
]

Under a passive attacker, only the first query is contradicted because e1 is sent over the network. The plaintext remains secret, the source is not altered and both shared-secret terms are equivalent. Under an active attacker, all four queries are contradicted because the public keys are unauthenticated. Writing security queries explains each query and the corresponding attacks.

Scenarios

The models above use fixed peers. In a deployed system, a participant may run the protocol with several peers at once. One of those peers may be malicious while holding valid long-term keys. The protocol should prevent that peer from using its own run to compromise a run with an honest peer.

A scenarios block represents one principal running concurrently with different peers under a shared attacker.

An attack involving two peers

The Needham–Schroeder public-key protocol provides a standard example of an attack that requires two peers.

The initiator encrypts a nonce and its identity under the responder’s public key. The responder returns the initiator’s nonce together with a new nonce. The initiator then returns the responder’s nonce. Needham and Schroeder published the protocol in 1978; Lowe identified an attack in 1995. The attack requires two concurrent runs.

Alice begins one run with Mallory, who is a legitimate participant with its own key. Mallory re-encrypts Alice’s nonce and identity under Bob’s key and starts a second run with Bob. Bob accepts the message because both the identity and nonce originated with Alice. He replies with Alice’s nonce and a new nonce. Mallory relays this response to Alice in the first run. Alice accepts it because it contains her nonce, then encrypts Bob’s nonce under Mallory’s key. Mallory decrypts the result. Bob completes the run believing that he communicated with Alice, while Mallory learns the nonce that Bob intended to share only with her.

The attack breaks no cryptographic primitive. Mallory uses its own private key to open a message Alice intended for it, then re-encrypts the contents for Bob and relays the responses between runs. Lowe’s repair includes the responder’s identity in the second message. Alice can then detect that a response naming Bob arrived in her run with Mallory.

Choose the peers

The complete scenarios.vp model gives Alice a gpeer placeholder. Its scenarios block binds that placeholder to Bob’s public key in one run and Mallory’s in another. Mallory’s private key is leaked, making the second peer corrupt. Both configurations share one attacker.

Scenario expansion

Verifpal sorts scenarios by how long their peers remain honest, with the longest first. See honest and corrupt peers below. The order in the model does not matter. The original query uses the first scenario’s identifiers. Each other scenario that is honest at phase 0 gets a copy of the query with its own identifiers. A failure in any copy fails the original query. A scenario that is corrupt from the start supplies executions and attacker knowledge, but gets no query of its own.

Honest and corrupt peers

Verifpal treats a peer as corrupt when the scenario’s bound values identify a secret the attacker can obtain. This includes secrets that are leaked, sent unencrypted, or computed from inputs the attacker holds: public values, values sent on the wire and compromised secrets. For example, binding gpeer to PUBKEY(mk) selects a corrupt peer if mk is leaked or sent as a message. Publishing the public key alone does not compromise its private key.

For an assigned secret, the attacker must have every ingredient needed to compute it. A key derived as HASH(a, b) does not become compromised merely because a leaks while b remains secret. A public certificate can nevertheless identify a corrupt peer if it names that peer’s compromised key; the attacker need not be able to forge the certificate.

A scenario becomes corrupt in the first phase where the attacker can obtain the relevant secret. It is honest before that phase. A peer whose key leaks in phase[1] is therefore an honest peer during phase 0, and phase 0 claims in its run are recorded. Only what a run held while its peer was honest can record a query violation, although the attacker keeps whatever it learns from a corrupt run. Each phase is judged as the execution stood at its end, so a value that run computes, receives or uses only in phase 1 is never a claim. What the run held at the end of phase 0 remains a claim in later phases, judged against what the attacker knows by then: a message encrypted to that peer in phase 0 is disclosed if the phase 1 leak opens it, which is how a model tests forward secrecy. Another run cannot answer for a value its own peer’s run holds either: when a query compares values held by different principals, each must be held by a run whose claims apply.

If every scenario is corrupt from the start, Verifpal evaluates queries in all runs. This prevents a pass caused solely by having no honest runs to check; the results may then include disclosures caused by every peer being corrupt. Every result lists the active scenarios and marks each as an honest or a corrupt peer.

A failed checked primitive in an honest execution normally indicates a modeling error: the modeled protocol cannot complete even without attacker interference. Verifpal therefore rejects it. A run with a corrupt peer may legitimately stop. For example, Bob should not be able to decrypt a message intended for Mallory. Verifpal requires successful checks in scenarios that are honest when the check runs, but permits a scenario to halt at a check in a phase where it is already corrupt.

Cost and limits

Scenario and session counts multiply. Two scenarios at the default of two sessions create four copies of each principal. The 128-principal limit applies after both expansions. Verifpal also limits the combined expansion to 31 copies and reports a valid session count if the requested combination is too large.

Use scenarios for properties that depend on peer identity, such as identity misbinding, unknown-key-share attacks, impersonation or attacks that require one party to communicate with two peers concurrently. A fixed set of principals is simpler and less expensive when the property does not depend on this distinction.

Each scenario binds constants for one named principal. It does not represent a role across an arbitrary population, and analysis covers only the declared peers. A model with two peers cannot expose an attack that requires three concurrent peers.