Provable Security 12: Where Proofs Stop
Provable security notes / XII
Where proofs stop
A proof is strongest inside its model; the implementation must still satisfy the model it claims to instantiate.
Provable security is valuable because it makes assumptions explicit. It is also limited for the same reason: if the real system violates the model, the theorem may no longer apply.
Random-oracle boundary
A random-oracle proof assumes the adversary only sees a public random function through oracle queries. A concrete hash function is finite code with structure, encodings, state, and implementation behavior.
Common gaps
Missing domain separation, ambiguous encodings, length-extension behavior, cross-protocol reuse, and inconsistent transcript hashing can all break the connection between the random-oracle model and the deployed hash function.
Side channels
Game definitions usually return mathematical values: plaintext, key, signature, or \(\bot\). Implementations return timing, memory access patterns, power traces, cache behavior, branch behavior, logs, exceptions, and sometimes distinct network errors.
A CCA proof that models one rejection symbol does not cover an implementation that reveals why rejection occurred.
Nonce and randomness failure
Many theorems condition on fresh randomness. If randomness repeats, the theorem is often inapplicable rather than merely weaker.
| Failure | Consequence |
|---|---|
| Reused stream nonce | Reveals XOR of plaintexts. |
| Reused Schnorr nonce | Reveals signing key. |
| Biased padding randomness | May make RSA encodings searchable. |
| Reused KEM coins | Can correlate encapsulations outside the proof model. |
Malformed ciphertext behavior
CCA and KEM proofs are sensitive to how invalid ciphertexts behave. A decapsulation function that rejects uniformly in the proof but leaks timing differences in code gives the adversary a stronger oracle.
Two rejection paths
If a hybrid decryptor reports “KEM invalid” and “DEM tag invalid” separately, an adversary learns which layer failed. A proof that exposes only one symbol \(\bot\) does not automatically cover that behavior.
Multi-user and multi-session systems
A theorem for one key and one session may degrade with the number of users, sessions, or targets. A deployment with millions of public keys should not read a single-user bound as if the factor were free.
Final rule
A proof gives a map of what must be true. Implementation work is the task of ensuring the real system follows that map: same inputs, same distributions, same rejection behavior, same side-channel assumptions, same key separation, and same query limits.
Source note
The boundary issues here should be read together with the definitions and construction transforms in Smart’s Cryptography Made Simple, Chapters 11 and 16. The chapters define the abstract games and public-key transforms; this note records the places where deployed systems must still match those abstractions.