Advertisement

Secure Two-Party Computation in Applied Pi-Calculus: Models and Verification

  • Sergiu BursucEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9533)

Abstract

Secure two-party computation allows two distrusting parties to compute a function, without revealing their 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 propose new models in applied pi-calculus 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.

Notes

Acknowledgement

We thank the reviewers for their valuable comments.

References

  1. 1.
    Yao, A.: Protocols for secure computations (extended abstract). In: FOCS, pp. 160–164. IEEE Computer Society (1982)Google Scholar
  2. 2.
    Yao, A.: How to generate and exchange secrets (extended abstract). In: FOCS, pp. 162–167. IEEE Computer Society (1986)Google Scholar
  3. 3.
    Lindell, Y., Pinkas, B.: An efficient protocol for secure two-party computation in the presence of malicious adversaries. In: Naor [35], pp. 52–78Google Scholar
  4. 4.
    Jarecki, S., Shmatikov, V.: Efficient two-party secure computation on committed inputs. In: Naor [35], pp. 97–114Google Scholar
  5. 5.
    Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS, pp. 136–145. IEEE Computer Society (2001)Google Scholar
  6. 6.
    Lindell, Y., Pinkas, B.: A proof of security of Yao’s protocol for two-party computation. J. Cryptol. 22(2), 161–188 (2009)CrossRefMathSciNetzbMATHGoogle Scholar
  7. 7.
    Abadi, M., Blanchet, B., Comon-Lundh, H.: Models and proofs of protocol security: a progress report. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 35–49. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Cortier, V., Kremer, S. (eds.): Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series. IOS Press, Amsterdam (2011)Google Scholar
  9. 9.
    Canetti, R., Herzog, J.: Universally composable symbolic security analysis. J. Cryptol. 24(1), 83–147 (2011)CrossRefMathSciNetzbMATHGoogle Scholar
  10. 10.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proceedings of the 10th ACM Conference on Computer and Communications Security, CCS 2003, Washington, DC, USA, 27–30 October 2003 (2003)Google Scholar
  11. 11.
    Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied pi calculus. In: Kannan, R., Narayan Kumar, K. (eds.), FSTTCS. LIPIcs, vol. 4, pp. 169–180 (2009)Google Scholar
  12. 12.
    Böhl, F., Unruh, D.: Symbolic universal composability. In: 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, LA, USA, 26–28 June 2013, pp. 257–271. IEEE (2013)Google Scholar
  13. 13.
    Dahl, M., Damgård, I.: Universally composable symbolic analysis for two-party protocols based on homomorphic encryption. In: Nguyen, P.Q., Oswald, E. (eds.) EUROCRYPT 2014. LNCS, vol. 8441, pp. 695–712. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  14. 14.
    Backes, M., Maffei, M., Mohammadi, E.: Computationally sound abstraction and verification of secure multi-party computations. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS. LIPIcs, vol. 8, pp. 352–363 (2010)Google Scholar
  15. 15.
    Rabin, M.O.: How to exchange secrets with oblivious transfer. IACR Cryptol. ePrint Arch. 2005, 187 (2005)Google Scholar
  16. 16.
    Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6), 637–647 (1985)CrossRefMathSciNetzbMATHGoogle Scholar
  17. 17.
    Huang, Y., Katz, J., Evans, D.: Efficient secure two-party computation using symmetric cut-and-choose. In: Canetti, R., Garay, J.A. (eds.) CRYPTO 2013, Part II. LNCS, vol. 8043, pp. 18–35. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  18. 18.
    Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game or a completeness theorem for protocols with honest majority. In: Aho, A.V. (eds.) STOC, pp. 218–229. ACM (1987)Google Scholar
  19. 19.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115, January 2001Google Scholar
  20. 20.
    Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop (CSFW 2001) (2001)Google Scholar
  21. 21.
    Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363–434 (2009)Google Scholar
  22. 22.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3–51 (2008)CrossRefMathSciNetzbMATHGoogle Scholar
  23. 23.
    Ryan, M., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series. IOS Press (2011)Google Scholar
  24. 24.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 243–320. MIT Press (1990)Google Scholar
  25. 25.
    Bursuc, S.: Secure two-party computation in applied pi-calculus: models and verification. Cryptology ePrint Archive, Report 2015/782 (2015). http://eprint.iacr.org/
  26. 26.
    Cortier, V., Delaune, S.: A method for proving observational equivalence. In: Computer Security Foundations Symposium (CSF), Port Jefferson, New York, USA, 8–10 July 2009, pp. 266–276. IEEE Computer Society (2009)Google Scholar
  27. 27.
    Lindell, Y., Pinkas, B.: Secure two-party computation via cut-and-choose oblivious transfer. J. Cryptol. 25(4), 680–722 (2012)CrossRefMathSciNetzbMATHGoogle Scholar
  28. 28.
    Damgård, I., Nielsen, J.B., Orlandi, C.: Essentially optimal universally composable oblivious transfer. In: Lee, P.J., Cheon, J.H. (eds.) ICISC 2008. LNCS, vol. 5461, pp. 318–335. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  29. 29.
    Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)zbMATHGoogle Scholar
  30. 30.
    Backes, M., Hriţcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: Computer Security Foundations Symposium (CSF), pp. 195–209. IEEE Computer Society (2008)Google Scholar
  31. 31.
    Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: 2004 IEEE Symposium on Security and Privacy (S&P 2004), 9–12 May 2004, Berkeley, CA, USA, p. 86. IEEE Computer Society (2004)Google Scholar
  32. 32.
    Bogetoft, P., Christensen, D.L., Damgård, I., Geisler, M., Jakobsen, T., Krøigaard, M., Nielsen, J.D., Nielsen, J.B., Nielsen, K., Pagter, J., Schwartzbach, M., Toft, T.: Secure multiparty computation goes live. In: Dingledine, R., Golle, P. (eds.) FC 2009. LNCS, vol. 5628, pp. 325–343. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  33. 33.
    Backes, M., Pfitzmann, B., Waidner, M.: The reactive simulatability (RSIM) framework for asynchronous systems. Inf. Comput. 205(12), 1685–1720 (2007)CrossRefMathSciNetzbMATHGoogle Scholar
  34. 34.
    Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied pi–calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 175–190. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  35. 35.
    Naor, M. (ed.): EUROCRYPT 2007. LNCS, vol. 4515, pp. 52–78. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.School of Computer ScienceUniversity of BristolBristolUK

Personalised recommendations