Solution (source code)

= Solution

In the <Dolev-Yao model>, an adversary controls the network: it can intercept, suppress, delay, replay and redirect messages, impersonate network senders, and construct messages from values it knows. In particular, it can concatenate or split unprotected tuples, and can apply <encryption> using any known <public key> or known symmetric key.

<Cryptography> is idealised. Without the required <private key> or symmetric key, the adversary cannot recover a protected <plaintext> or construct an otherwise unavailable protected value. It cannot invent an unknown long-term secret merely because the containing <ciphertext> is visible. <Protocol> failures arise from the arrangement of messages even when these cryptographic primitives behave perfectly.

$$
\boxed{\text{Complete network control, with perfect cryptographic operations.}}
$$