IACR News item: 06 August 2015
Sergiu Bursuc
ePrint ReportFurthermore, even for classic protocols such as Yao\'s (based on garbled circuits and oblivious transfer), we do not have adequate symbolic models for cryptographic primitives and protocol roles, that can form the basis for automated security proofs. We therefore propose new models in applied pi-calculus in order to address these gaps. Our contributions, formulated in the context of Yao\'s protocol, include:
- an equational theory for specifying the primitives of garbled computation and oblivious transfer;
- process specifications for the roles of the two parties in Yao\'s protocol;
- definitions of security that are more clear and direct: result integrity, input agreement (both based on correspondence assertions) and input privacy (based on observational equivalence).
We put these models together and illustrate their use with ProVerif, providing a first automated verification of security for Yao\'s two-party computation protocol.
Additional news items may be found on the IACR news page.