Security Proofs: Types and Techniques
Black-box versions of each of these techniques (black-box reduction, black-box simulation, etc.) are the strongest proofs. In a black-box proof, the adversary is treated as a "black box" (its inner workings are unknown), that is, the approach must work for any adversary. This affects the order of quantifiers in a proof ("There exists ⟨some technique⟩ such that for all adversaries, the scheme is secure" instead of "for all adversaries, there exists ⟨some technique⟩ such that the scheme is secure".)
- Hybrid argument
-
Often used in game-based proofs, but a similar technique is also used to break down the various changes between the simulator in the real-world protocol in simulation-based proofs. We start with a security game, then slowly replace pieces of the game (each modified game is a hybrid game/experiment) in a way that is induistinguishable to the adversary. Eventually we arrive at a simple game in which the adversary clearly has negligible advantage (or where this can be shown via a reduction).
Further Reading
"Sequences of Games: A Tool for Taming Complexity in Security Proofs" by Victor Shoup
- Reduction
-
We reduce the security of some scheme B to an assumption A, that is, we wish to show that the assumption A implies the security of scheme B (A ⇒ B).
This is done by contradiction: we instead prove the contrapositive, that if B is insecure, A does not hold (¬B ⇒ ¬A). Specifically, we assume the existence of an adversary \(A_1\) that breaks the security properties of B, and use it to construct an adversary \(A_2\) that can run \(A_1\)'s code as a subroutine to break the security of A.
Reduction tightness
A reduction is called tight if...
Proof by Simulation
Further Reading
How to Simulate It – A Tutorial on the Simulation Proof Technique by Yehuda Lindell
- Rewinding
- When a simulator "rewinds" the adversary to a previous step in its execution. A good way to think about this is to remember that the adversary is a (usually PPT) algorithm, and even if it is probabilstic the randomness can be programmed as an input. This means that the simulator can just re-run \(\mathcal{A}\) with the same inputs up until a certain point, when it can "branch" from the previous run and try a new response. An example is the proof of knowledge soundness of a Sigma protocol.
A simulator which does not use rewinding is called a straight-line.