Yao's garbling scheme
Yao's garbling scheme is a core tool for secure multi-party computation. The scheme first associates a pair of keys (a key for 0 and a key for 1) with the output (wire) of each gate and then double-encrypts the output keys of a gate under the "matching" input keys to obtain an unordered set of 4 ciphertexts so that, when holding keys corresponding to the input bits, one can decrypt one of the ciphertexts of each gate in the first layer of the circuit and, in this way, obtain keys corresponding to the wire values after the first layer etc. until the last layer.
Lindell and Pinkas gave the first security analysis of Yao's garbled circuit approach. Later, Bellare, Hoang and Rogaway introduced the garbling scheme abstraction and provided a code-based game-playing, modular analysis of Yao's garbling scheme. Recently, Brzuska and Oechsner also gave an SSP-style proof for Yao's garbling scheme, which we visualize here.
We recommend to check out the formalization of IND-CPA security in SSPs, which also provides an equivalence proof for two encodings of IND-CPA which will be used in the security proof for Yao's garbling scheme and can be studied and understood in isolation, all the while increasing familiarity with SSPs. Next, we encode garbling schemes and their security in SSPs as well as present Yao's garbling scheme construction here. Finally, we present Brzuska and Oechsner's SSP-style proof of Yao's garbling scheme.
All code and graphs relating to Yao's garbling scheme and its proof which we present here is identical to code provided by Brzuska and Oechsner.