Furthermore, 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.Category / Keywords: formal verification, automated security proofs, security models Original Publication (with minor differences): 10th Symposium on Trustworthy Global Computing (TGC 2015) Date: received 6 Aug 2015, last revised 7 Aug 2015 Contact author: s bursuc at bristol ac uk Available format(s): PDF | BibTeX Citation Version: 20150807:125840 (All versions of this report) Short URL: ia.cr/2015/782 Discussion forum: Show discussion | Start new discussion