7. Security Definitions
This chapter collects the security definitions and cryptographic assumptions used in the PQXDH security analysis (Bhargavan et al., USENIX Security 2024).
Each security property and cryptographic assumption is declared as an
opaque definition in Lean. This is a deliberate design choice:
opaque definitions state what a security notion requires without
committing to how it is realized. This lets the protocol theorems
depend on these assumptions abstractly, so the same proof works for
any concrete instantiation that satisfies the assumption. Opaque
definitions also prevent the simplifier from unfolding security
assumptions during proof search, keeping the proof structure close
to the paper's reasoning.