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

Sergiu Bursuc

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

183 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationSymposium on Trustworthy Global Computing (TGC 2015)
Subtitle of host publication10th International Symposium, TGC 2015 Madrid, Spain, August 31 – September 1, 2015 Revised Selected Papers
PublisherSpringer
Pages1-15
Number of pages15
ISBN (Electronic)9783319287669
ISBN (Print)9783319287652
DOIs
Publication statusPublished - 5 Jan 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9533
ISSN (Print)0302-9743

Bibliographical note

Due to be published in 2016.

Keywords

  • Automated verification
  • , Security models, Cryptographic protocols

Fingerprint

Dive into the research topics of 'Secure two-party computation in applied pi-calculus: models and verification'. Together they form a unique fingerprint.

Cite this