mk : DolevYaoDolevYao : Type§3.1, p. 473 and §3.4, p. 474: The Dolev-Yao adversary model (symbolic/ProVerif).

A marker type indicating the analysis is carried out in the symbolic
model, where:
  - The adversary controls the network (active MitM): it can
    intercept, inject, replay, and modify all messages.
  - Cryptographic primitives are ideal black boxes — the
    adversary cannot break encryption, forge signatures, or invert
    hashes except by using the appropriate key.
  - The adversary may compromise long-term keys at any time
    (adaptive corruption).

Security properties are expressed as correspondence assertions:
  "if event A occurred (e.g. Bob completed a session with Alice),
   then event B must have occurred (e.g. Alice initiated it)."

In the post-quantum extension, the adversary is additionally given
the power to break DH (compute discrete logs) at some point in
time, modeling a future quantum computer. Security of sessions
completed *before* this point is then analyzed.

Since all primitives are ideal, no computational hardness
assumptions appear as hypotheses in the symbolic model.
Theorem 1 depends only on the protocol logic. 

NewSession : AKE_QueryAKE_Query : Type§3.2, p. 473 and §3.5, p. 475: Oracle queries available to the adversary
in the computational authenticated key exchange (AKE) security game.
This models the interface between the adversary and the challenger in CryptoVerif. 

Initiate a new protocol session between two identified parties.
Returns a session handle. 

Send : AKE_QueryAKE_Query : Type§3.2, p. 473 and §3.5, p. 475: Oracle queries available to the adversary
in the computational authenticated key exchange (AKE) security game.
This models the interface between the adversary and the challenger in CryptoVerif. 

Deliver a (possibly modified) message to a session, advancing
the protocol state. Models an active network attacker. 

Corrupt : AKE_QueryAKE_Query : Type§3.2, p. 473 and §3.5, p. 475: Oracle queries available to the adversary
in the computational authenticated key exchange (AKE) security game.
This models the interface between the adversary and the challenger in CryptoVerif. 

Obtain the long-term secret key of a named party.
Models key compromise / corruption. 

RevealSessionKey : AKE_QueryAKE_Query : Type§3.2, p. 473 and §3.5, p. 475: Oracle queries available to the adversary
in the computational authenticated key exchange (AKE) security game.
This models the interface between the adversary and the challenger in CryptoVerif. 

Obtain the session key of a completed session.
Models compromise of session-specific secrets. 

Test : AKE_QueryAKE_Query : Type§3.2, p. 473 and §3.5, p. 475: Oracle queries available to the adversary
in the computational authenticated key exchange (AKE) security game.
This models the interface between the adversary and the challenger in CryptoVerif. 

Challenge query: receive either the real session key or a
uniformly random key (determined by a hidden coin flip).
The adversary must guess which.