A State-Separating Proof for Yao’s Garbling Scheme

State-separating proofs (SSPs) are a recent proof and definition style for cryptographic security games in pseudo-code. SSPs allow to carry out computational security reductions for cryptography such that “irrelevant code” can be dealt with syntactically and does not require reasoning about execution semantics. Real-world protocols have notoriously long specifications, and the SSP style of breaking down security games and identifying subgames enables the analysis of such protocols. Indeed, SSPs have been used to analyze the key schedules of TLS (ePrint 2021/467) and MLS (S&P 2022). Similarly, secure multi-party computation (MPC) protocols tend to have lengthy specifications. In this work, we explore how to use SSP techniques in the MPC context and for simulation-based security. On the example of Yao’s circuit garbling scheme, we adapt the definitional style of SSPs and show that structuring the circuit and security proof in a layered way allows for a brief, compelling, syntactic construction of the reductions required in the hybrid proof of Yao’s garbling scheme.