Cryptology ePrint Archive: Report 2021/1453

A State-Separating Proof for Yao’s Garbling Scheme

Chris Brzuska and Sabine Oechsner

Abstract: 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.

Category / Keywords: foundations / Yao's garbling scheme, state-separating proofs, foundations, composition, verification, secure multiparty computation

Date: received 28 Oct 2021, last revised 29 Oct 2021

Contact author: chris brzuska at aalto fi, s oechsner at ed ac uk

Available format(s): PDF | BibTeX Citation

Version: 20211029:183158 (All versions of this report)

Short URL: ia.cr/2021/1453


[ Cryptology ePrint archive ]