Documentation / Modeling a protocol

Modeling a protocol

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

Use the language reference for declarations and syntax. Here, build an unauthenticated Diffie–Hellman exchange, compare attacker models, and extend the setting to honest and malicious peers.

A modeling workflow

Start with a written security claim, then build the smallest model that can test it. A useful working sequence is:

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. Choose queries deliberately. Ask about the original secret when testing disclosure, the received field when testing authentication, and an actual later send when using a completion precondition. Use --auto-queries to look for omitted questions, then retain only those that express the intended 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. A passing result code alone loses the assumptions and search envelope.

Avoid changing a model merely to make every query pass. A replayable opening message, a deliberately public value or a discarded session key can produce a correct failure. Either repair the protocol or explain why that query does not express the 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

For A First Protocol, 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 a fixed set of peers. In a deployed system, one party may run the same protocol concurrently with several peers, including a malicious but authorized participant that owns valid long-term keys. A secure protocol should prevent such a participant from using one run to compromise another run with an honest peer.

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

A Two-Peer Attack

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 combines two concurrent runs rather than breaking either run in isolation.

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

Before expansion, Verifpal orders the scenarios so that the configurations that stay honest longest come first (Honest and Corrupt Counterparties); the order written in the model has no meaning. The written query keeps the identifiers of the first scenario in that order. Every other scenario that is honest at phase 0 receives a variant of each query, and a violation in any variant contradicts the written query. A scenario that is corrupt from the start contributes executions and attacker knowledge but no claim of its own.

Honest and Corrupt Counterparties

A scenario represents a corrupt counterparty when its bound values identify secret material available to the attacker. The classification includes secrets explicitly leaked, secrets sent bare on the wire, and assigned values computable from public or compromised inputs. 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.

Corruption is indexed by phase. A scenario is corrupt from the earliest phase in which the relevant secret becomes available, and honest before it. 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 runs that are honest at the current phase may record a query violation, although the attacker keeps whatever it learns from a corrupt run. If no scenario is honest at the current phase, Verifpal evaluates the queries in the corrupt-peer runs instead, so that the analysis does not report a vacuous pass; the result then includes disclosures that follow from 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 honest scenarios but permits a corrupt scenario to halt.

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.

Scenarios have two important bounds. First, each scenario binds constants for one named principal; it does not quantify a role over an arbitrary population. Second, analysis covers only the declared number of peers. A model with two peers cannot expose an attack that requires three concurrent peers.