Language reference

Attacker

attacker[active]

The first declaration selects active or passive. Both attackers observe network messages and derive values using the symbolic primitive rules. An active attacker can also intercept, replace and inject traffic.

Principals and prior knowledge

principal Alice[
	knows private sk
	knows public context
	generates nonce
]

A principal block describes local operations. Later blocks with the same name continue that principal’s state. A knows private value is initially available only to principals that declare it; repeat the same declaration to model a shared secret. knows public makes a value known to every principal and the attacker. Prior knowledge stays shared across sessions.

Fresh values and leaks

principal Alice[
	generates nonce
	leaks sk
]

generates creates a fresh value, private until disclosed, with a distinct copy in each session. leaks discloses a value the principal already knows to the attacker. To model delayed compromise, put the leak in a later phase.

Names, assignments and outputs

k_send, k_receive = HKDF(nil, secret, context)
tag = MAC(k_send, HASH(message))

Names use ASCII letters, digits and underscores and are case-insensitive. Constants have a global namespace and cannot be reassigned. Assignments introduce new names and require a primitive expression on the right; x = y is invalid. Nested calls are allowed. Bind multiple outputs in order, using the counts specified below.

Names cannot be keywords, primitive names, or start with attacker or unnamed. Each argument must be available to the principal. // starts a line comment; /* … */ encloses a block comment. There are no strings, general-purpose numeric data literals, loops, mutable variables or user-defined primitives.

nil and discarded outputs

_ = SIGNVERIF(pk, message, signature)?

nil is a built-in public constant, known to the attacker. Use it for an absent context or associated-data value; it is not a secret, fresh nonce or wildcard. _ discards the name of an output while still performing the computation and any check. Each underscore creates a separate anonymous output.

Messages and guards

Alice -> Bob: [pk], signature

Messages appear between principal blocks. The sender must know each named constant, and the recipient must not already know that field. Assign primitive expressions to names before sending them. ASCII -> and Unicode → arrows are accepted.

Brackets guard one transmitted value: the attacker can observe it but cannot replace the sender’s delivered copy. This assumes authentication provided by the deployment. A guarded relay can still forward an earlier attacker-substituted input; guarding a later hop does not authenticate the value’s original source.

Checked operations

_ = SIGNVERIF(pk, message, signature)?

A trailing ? halts the principal when a check fails. It is supported by ASSERT, SPLIT, AEAD_DEC, SIGNVERIF, RINGSIGNVERIF and KEM_DECAP. Place required checks before consuming the message.

DEC, PKE_DEC and UNBLIND cannot take this suffix. An unmatched unchecked call remains an unreduced symbolic term; it does not represent a real API returning that term as plaintext.

Phases and delayed compromise

phase[1]
principal Alice[
	leaks sk
]

The model starts in phase 0. Explicit phases increase by one. A later leak can reveal earlier recorded ciphertexts, but cannot justify an attacker action before the leak. Queries are judged at the end of each phase against what the execution has done by then. Phases do not erase keys, clear attacker knowledge or provide wall-clock timing.

Peer scenarios

scenarios[
	Alice[gpeer = gb]
	Alice[gpeer = gm]
]

Place the optional scenarios block immediately before queries. Each entry binds one principal’s prior-knowledge placeholders to declared values. Every principal and message is cloned per scenario, with a shared attacker, before session replication. This lets an honest-peer run interact with a run involving a corrupt peer.

A binding must name a constant declared with knows by that principal; it cannot bind a field sent over the network. Multiple bindings in one entry are comma-separated. Only the listed peer configurations are analyzed. Open the Lowe attack example.

Confidentiality

confidentiality? secret

Contradicted when the attacker can obtain the queried value as it resolves in any principal state reached during the search. If the attacker substituted that value, the query can fail even while the original secret remains private. The qualifier [attacker-supplied value] distinguishes that case. Query the original secret when its disclosure is your concern, or use a precondition for an accepted key.

Authentication

authentication? Alice -> Bob: proof

Checks the origin and duplicate acceptance of a value Bob successfully uses. The query fails if the used value came from neither Alice’s unchanged delivery, directly or through principals that forward it, nor a matching run that actually sent it. A value equal to what Alice would have sent does not count unless a run of Alice sent it. The query also fails if two recipient runs successfully use one sending.

The message must be received and used inside a primitive. Required checks determine successful use; an unrelated later halt does not automatically undo an earlier use. This is an injective use-origin test, not a claim of general agreement or protocol completion. [duplicate acceptance] identifies a replay, which need not involve a forgery.

Freshness

freshness? nonce_hash

Contradicted when a principal successfully uses the queried value and its resolved term contains no generated constant, or when the attacker delivers a value that another run of the same principal also accepts, as when a signed nonce is replayed from another session. This does not establish recency: a value from another session that no second run accepts still passes, and so does one that contains an old run’s generated nonce. Use authentication queries and the protocol’s actual challenge checks to investigate duplicate acceptance.

Equivalence

equivalence? k_alice, k_bob

Compares two or more distinct named values after substitution and rewriting, as one principal copy sees them: the values it holds and, for a value it does not hold, the value held by the copy that computed it, provided that copy is also honest at that phase. This lets a query compare two parties’ keys. The query fails if eligible values differ under the symbolic equations. It excludes failed checked outputs and values that were never computed because a check failed. A pass does not show that both parties completed, and this query does not establish observational equivalence between protocols.

Unlinkability

unlinkability? token1, token2

Searches for evidence linking observable values whose honest versions are equal or share a secret-dependent subterm. Witnesses include observed equality, a shared identifying check, reconstruction from a common secret origin, and recognition of a secret tied to the other value. Attacker-manufactured relationships are excluded.

Use two or more distinct named constants. A pass means none of the supported witnesses was found; it is not a proof of indistinguishability. The query guide gives the precise observability and eligibility conditions.

Query preconditions

confidentiality? k_client[
	precondition[Client -> Server: request]
]

Restricts any query to executions in which the named sender reaches the specified send. To check a property only after acceptance, choose a message the protocol sends after the required checks.

The event is the send, not receipt. The property’s failure and the send must occur in the same execution. Several preconditions require every named send. Adding a precondition can remove contradictions; it does not strengthen the unconditional property.

ASSERT

_ = ASSERT(expected, received)?

Inputs

2

Outputs

1

Checked

Yes: ?

Assumptions

None

Compares terms for equality. Use the question mark to stop on a mismatch; discard the output when only the check matters.

CONCAT

packet = CONCAT(header, payload)

Inputs

2–5

Outputs

1

Checked

No

Assumptions

None

Builds a structured tuple. Anyone holding it can extract its components. Boundaries and nesting are preserved; this does not model ambiguous byte concatenation.

SPLIT

header, payload = SPLIT(packet)?

Inputs

1

Outputs

1–5

Checked

Yes: ?

Assumptions

None

Selects tuple components in order. The input must resolve to a suitable CONCAT; a checked call stops on malformed input. It does not flatten nested tuples.

HASH

digest = HASH(message, context)

Inputs

1–5

Outputs

1

Checked

No

Assumptions

weak

Produces a symbolic hash of its arguments, in order. Holding an ideal hash does not reveal its preimage. Repeating the same inputs produces the same term.

MAC

tag = MAC(key, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

forgeable

Computes a keyed authenticator. Check a received tag with ASSERT(MAC(key, message), tag)? using the expected key and message.

HKDF

k_send, k_receive = HKDF(salt, secret, context)

Inputs

3

Outputs

1–5

Checked

No

Assumptions

None

Derives keys from a salt, input key material and context, in that order. Each output position gives a distinct key. Identical calls produce identical outputs in the same positions; new names alone do not make new keys.

PUBKEY

pk = PUBKEY(sk)

Inputs

1

Outputs

1

Checked

No

Assumptions

weak

Derives a public key from a private value. It does not publish that key. Used for signatures, public-key encryption, Diffie–Hellman and KEMs. The input cannot already be a PUBKEY or DH_KEX term.

DH_KEX

shared = DH_KEX(peer_public, my_private)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Combines the peer’s public key with your private value. DH_KEX(PUBKEY(a), b) equals DH_KEX(PUBKEY(b), a). The second argument cannot be a public key, and DH_KEX cannot be nested inside itself.

A received peer key must resolve to a PUBKEY term for this equality to apply. A wrongly shaped key can hide attacks on the intended exchange.

ENC

ciphertext = ENC(key, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

weak, malleable

Models symmetric encryption as a deterministic operation, without an explicit nonce, padding or mode. The malleable assumption lets the attacker replace the plaintext with a value it can construct.

DEC

message = DEC(key, ciphertext)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Reduces DEC(key, ENC(key, message)) to message. It has no checked-failure branch and cannot take a question mark.

Conversely, holding DEC(k, e) and k reveals e. Authenticated and public-key decryption have no such inverse deduction rule.

AEAD_ENC

ciphertext = AEAD_ENC(key, nonce, message, ad)

Inputs

4

Outputs

1

Checked

No

Assumptions

weak, forgeable

Authenticated encryption with associated data. Use a distinct generated nonce for every encryption under one key. Associated data is opaque inside this symbolic term; transmit it separately if it should be observable.

If the attacker obtains two distinct ciphertext terms under the same key and nonce in one execution, it can recover both plaintexts and forge ciphertexts under that pair without knowing the key or nonce. This rule models a worst case: a real attack may need known or guessable plaintext. The rule does not reveal the key or affect other nonces. Identical calls produce only one term and do not trigger it.

Try the disclosure and forgery experiments.

AEAD_DEC

message = AEAD_DEC(key, nonce, ciphertext, ad)?

Inputs

4

Outputs

1

Checked

Yes: ?

Assumptions

None

Authenticated decryption. Key, nonce and associated data must match the encryption. Use the question mark when failure must stop the principal. Attacker decryption also requires the nonce, so send it if the real protocol exposes it.

PKE_ENC

ciphertext = PKE_ENC(recipient_pk, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

weak

Encrypts for a recipient public key; decryption needs the corresponding private value. Anyone holding the public key can encrypt, so this does not authenticate the sender. The symbolic call is deterministic and has no randomness argument.

PKE_DEC

message = PKE_DEC(sk, ciphertext)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Reduces PKE_DEC(sk, PKE_ENC(PUBKEY(sk), message)) to message. It cannot take a question mark; an unmatched call remains unreduced.

SIGN

signature = SIGN(sk, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

forgeable

Signs a message using a private key. Verify against the corresponding PUBKEY(sk). Repeating the same inputs produces the same signature term.

SIGNVERIF

_ = SIGNVERIF(pk, message, signature)?

Inputs

3

Outputs

1

Checked

Yes: ?

Assumptions

None

Checks the signature against the given public key and message. On success it reduces to nil, not to the signed message. The question mark enforces rejection. Trust in the public key must be established separately.

RINGSIGN

signature = RINGSIGN(sk_a, pk_b, pk_c, message)

Inputs

4

Outputs

1

Checked

No

Assumptions

forgeable

Creates a three-member ring signature. The first argument is the actual signer’s private key; the next two are the other members’ public keys. Verification identifies membership of the ring without identifying which member signed.

RINGSIGNVERIF

_ = RINGSIGNVERIF(pk_a, pk_b, pk_c, message, signature)?

Inputs

5

Outputs

1

Checked

Yes: ?

Assumptions

None

Verifies with all three ring public keys. Their order may differ from the signing call, but the keys must correspond one-to-one to the signed ring. Add the question mark to stop on failure.

BLIND

blinded = BLIND(factor, message)

Inputs

2

Outputs

1

Checked

No

Assumptions

None

Blinds a message under a secret factor so that another principal can sign the blinded term without learning the message. Keep the factor secret.

The blinding factor also lets an attacker recover the message from a held blinded term.

UNBLIND

signature = UNBLIND(factor, message, blinded_signature)

Inputs

3

Outputs

1

Checked

No

Assumptions

None

Converts SIGN(sk, BLIND(factor, message)) to SIGN(sk, message). The blind signature is the third argument. Anyone holding the factor, message and blind signature can unblind it. This operation cannot be checked.

KEM_ENCAP

shared, ciphertext = KEM_ENCAP(recipient_pk, seed)

Inputs

2

Outputs

2

Checked

No

Assumptions

weak

Encapsulates to PUBKEY(sk) using an explicitly generated seed. Bind the shared secret first and ciphertext second. Reusing inputs repeats outputs. A KEM does not authenticate who encapsulated; authenticate the ciphertext separately when required.

An attacker that holds the ciphertext and its private decapsulation key can recover both the shared secret and the modeled seed. This rule represents decapsulation’s re-encryption check. The shared secret alone reveals neither ciphertext nor seed.

KEM_DECAP

shared = KEM_DECAP(sk, ciphertext)?

Inputs

2

Outputs

1

Checked

Yes: ?

Assumptions

None

Recovers the shared secret with the corresponding private decapsulation key. A checked call stops on a mismatched ciphertext. This deterministic symbolic interface does not model ML-KEM’s implicit rejection or probabilistic behavior.

THRESHOLD_SPLIT

s1, s2, s3 = THRESHOLD_SPLIT[2](secret)

Inputs

1

Outputs

2–16

Checked

No

Assumptions

None

Splits a secret into shares: any t distinct shares recover it, and fewer reveal nothing. Specify t in brackets. It must be between 2 and the number of assigned outputs. Shares can also be used with THRESHOLD_SIGN.

THRESHOLD_JOIN

secret = THRESHOLD_JOIN(s1, s3)

Inputs

2–16

Outputs

1

Checked

No

Assumptions

None

Combines at least t distinct shares of one split. Matching partial signatures combine into SIGN(secret, message), and public share keys combine into PUBKEY(secret). Too few pieces, repeated shares, or disagreeing signature contexts leave the call unreduced.

THRESHOLD_SIGN

partial = THRESHOLD_SIGN(share, nonce, commitments, message)

Inputs

4

Outputs

1

Checked

No

Assumptions

forgeable

Produces a FROST partial signature using one share and a fresh secret nonce. At least t partials over distinct shares with the same commitments and message combine through THRESHOLD_JOIN. Two distinct partials under one share and nonce reveal that share. Repeating an identical partial does not.

This simplifies FROST to one symbolic nonce, omitting nonce pairs, binding factors and scalar arithmetic. See the two-of-three signing example.