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.
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 language | English |
|---|---|
| Title of host publication | Symposium on Trustworthy Global Computing (TGC 2015) |
| Subtitle of host publication | 10th International Symposium, TGC 2015 Madrid, Spain, August 31 – September 1, 2015 Revised Selected Papers |
| Publisher | Springer |
| Pages | 1-15 |
| Number of pages | 15 |
| ISBN (Electronic) | 9783319287669 |
| ISBN (Print) | 9783319287652 |
| DOIs | |
| Publication status | Published - 5 Jan 2016 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 9533 |
| ISSN (Print) | 0302-9743 |
Bibliographical note
Due to be published in 2016.Keywords
- Automated verification
- , Security models, Cryptographic protocols