Paper 2015/782

Secure two-party computation in applied pi-calculus: models and verification

Sergiu Bursuc

Abstract

Secure two-party computation allows two mutually distrusting parties to compute a function together, without revealing their secret inputs to each other. Traditionally, the security properties desired in this context, and the corresponding security proofs, are based on a notion of simulation, which can be symbolic or computational. Either way, the proofs of security are intricate, requiring first to find a simulator, and then to prove a notion of indistinguishability. 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.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. Minor revision. 10th Symposium on Trustworthy Global Computing (TGC 2015)
Keywords
formal verificationautomated security proofssecurity models
Contact author(s)
s bursuc @ bristol ac uk
History
2015-08-07: revised
2015-08-06: received
See all versions
Short URL
https://ia.cr/2015/782
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2015/782,
      author = {Sergiu Bursuc},
      title = {Secure two-party computation in applied pi-calculus: models and verification},
      howpublished = {Cryptology ePrint Archive, Paper 2015/782},
      year = {2015},
      note = {\url{https://eprint.iacr.org/2015/782}},
      url = {https://eprint.iacr.org/2015/782}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.