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 called a hybrid game or hybrid 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 Y to an assumption X, that is, we wish to show that the assumption X implies the security of scheme Y (X ⇒ Y).

This is done by contradiction: we instead prove the contrapositive, that if Y is insecure, X does not hold (¬Y ⇒ ¬X). Specifically, we assume the existence of an adversary \(\mathcal{A}_1\) that breaks the security properties of Y, and use it to construct an adversary \(\mathcal{A}_2\) that can run \(\mathcal{A}_1\)'s code as a subroutine to break the security of X.

Reduction tightness

A reduction is called tight if the running time and advantage of \(\mathcal{A}_2\) is "close to" that of \(\mathcal{A}_1\) (see here for some discussion on what is "close").

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.

Universal Composability (UC) Framework

Introduced by [Canetti'01].