Skip to main content
SpringerLink
Log in

Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender

  • Conference paper
Cryptology and Network Security (CANS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 8813))

Included in the following conference series:

  • 1155 Accesses

Abstract

We provide a proof of correctness and security of a two-party-computation protocol based on garbled circuits and oblivious transfer in the presence of a semi-honest sender. To achieve this we are the first to combine a machine-assisted proof of correctness with advanced cryptographic primitives to prove security properties of Java code. The machine-assisted part of the proof is conducted with KeY, an interactive theorem prover.

The proof includes a correctness result for the construction and evaluation of garbled circuits. This is particularly interesting since checking such an implementation by hand would be very tedious and error-prone. Although we stick to the secure two-party-computation of an n-bit AND in this paper, our approach is modular, and we explain how our techniques can be applied to other functions.

To prove the security of the protocol for an honest-but-curious sender and an honest receiver, we use the framework presented by Küsters et al. for the cryptographic verification of Java programs. As part of our work, we add oblivious transfer to the set of cryptographic primitives supported by the framework. This is a general contribution beyond our results for concrete Java code.

This work was partially funded by the KASTEL project by the Federal Ministry of Education and Research, BMBF 01BY1172. Florian Böhl was supported by MWK grant “MoSeS”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnett, M., Rustan M. Leino, K., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71–90. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  4. Bellare, M., Hoang, V.T., Rogaway, P.: Foundations of garbled circuits. In: Yu, T., Danezis, G., Gligor, V.D. (eds.) ACM CCS 2012, pp. 784–796. ACM Press (October 2012)

    Google Scholar 

  5. Böhl, F., Greiner, S., Scheidecker, P.: Java sources and proofs for the implementation in this paper, http://formal.iti.kit.edu/~greiner/cans2014/CodeAndProofCANS2014.zip

  6. Böhl, F., Greiner, S., Scheidecker, P.: Proving correctness and security of two-party computation implemented in Java in presence of a semi-honest sender. IACR Cryptology ePrint Archive, 2014: 618 (2014), https://eprint.iacr.org/2014/618

  7. Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: 42nd FOCS, pp. 136–145. IEEE Computer Society Press (October 2001)

    Google Scholar 

  8. Canetti, R., Lindell, Y., Ostrovsky, R., Sahai, A.: Universally composable two-party and multi-party secure computation. In: 34th ACM STOC, pp. 494–503. ACM Press (May 2002)

    Google Scholar 

  9. Canetti, R., Rabin, T.: Universal composition with joint state. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 265–281. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Choi, S.G., Katz, J., Wee, H., Zhou, H.-S.: Efficient, adaptively secure, and composable oblivious transfer with a single, global CRS. In: Kurosawa, K., Hanaoka, G. (eds.) PKC 2013. LNCS, vol. 7778, pp. 73–88. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Erkin, Z., Franz, M., Guajardo, J., Katzenbeisser, S., Lagendijk, I., Toft, T.: Privacy-preserving face recognition. In: Goldberg, I., Atallah, M.J. (eds.) PETS 2009. LNCS, vol. 5672, pp. 235–253. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Filliâtre, J.-C., Marché, C.: The why/krakatoa/caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game or A completeness theorem for protocols with honest majority. In: Aho, A. (ed.) 19th ACM STOC, pp. 218–229. ACM Press (May 1987)

    Google Scholar 

  15. Greiner, S., Birnstill, P., Krempel, E., Beckert, B., Beyerer, J.: Privacy preserving surveillance and the tracking-paradox. In: Lauster, M. (ed.) Proceedings of the 8th Future Security. Security Research Conference, pp. 296–302. Fraunhofer Verlag, Berlin (2013)

    Google Scholar 

  16. Huang, Y., Evans, D., Katz, J., Malka, L.: Faster secure two-party computation using garbled circuits. In: USENIX Security Symposium (2011a)

    Google Scholar 

  17. Huang, Y., Malka, L., Evans, D., Katz, J.: Efficient privacy-preserving biometric identification. In: NDSS (2011b)

    Google Scholar 

  18. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for c and java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Jha, S., Kruger, L., Shmatikov, V.: Towards practical privacy for genomic computation. In: 2008 IEEE Symposium on Security and Privacy, pp. 216–230. IEEE Computer Society Press (May 2008)

    Google Scholar 

  20. Kolesnikov, V., Schneider, T.: Improved garbled circuit: Free XOR gates and applications. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 486–498. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Küsters, R., Scapin, E., Truderung, T., Graf, J.: Extending and applying a framework for the cryptographic verification of java programs. IACR Cryptology ePrint Archive, 2014:38 (2014)

    Google Scholar 

  22. Küsters, R., Truderung, T., Beckert, B., Bruns, D., Graf, J., Scheben, C.: A hybrid approach for proving noninterference and applications to the cryptographic verification of Java programs. In: Hammer, C., Mauw, S. (eds.) Grande Region Security and Reliability Day 2013, Luxembourg (2013)

    Google Scholar 

  23. Küsters, R., Truderung, T., Graf, J.: A framework for the cryptographic verification of java-like programs. In: CSF 2012, pp. 198–212. IEEE (2012)

    Google Scholar 

  24. Gary, T., Leavens, A.L.: Baker, and Clyde Ruby. Preliminary design of jml: A behavioral interface specification language for java. SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006) ISSN 0163-5948

    Google Scholar 

  25. Lindell, Y., Pinkas, B.: A proof of yao’s protocol for secure two-party computation. Electronic Colloquium on Computational Complexity (ECCC) (063) (2004)

    Google Scholar 

  26. Lindell, Y., Pinkas, B.: An efficient protocol for secure two-party computation in the presence of malicious adversaries. In: Naor, M. (ed.) EUROCRYPT 2007. LNCS, vol. 4515, pp. 52–78. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  27. Lindell, Y., Pinkas, B., Smart, N.P.: Implementing two-party computation efficiently with security against malicious adversaries. In: Ostrovsky, R., De Prisco, R., Visconti, I. (eds.) SCN 2008. LNCS, vol. 5229, pp. 2–20. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Malkhi, D., Nisan, N., Pinkas, B., Sella, Y.: Fairplay - secure two-party computation system. In: USENIX Security Symposium, pp. 287–302 (2004)

    Google Scholar 

  29. Nielsen, J.B., Orlandi, C.: LEGO for two-party secure computation. In: Reingold, O. (ed.) TCC 2009. LNCS, vol. 5444, pp. 368–386. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  30. Osadchy, M., Pinkas, B., Jarrous, A., Moskovich, B.: SCiFI - a system for secure face identification. In: 2010 IEEE Symposium on Security and Privacy, pp. 239–254. IEEE Computer Society Press (May 2010)

    Google Scholar 

  31. Peikert, C., Vaikuntanathan, V., Waters, B.: A framework for efficient and composable oblivious transfer. In: Wagner, D. (ed.) CRYPTO 2008. LNCS, vol. 5157, pp. 554–571. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  32. Rabin, M.O.: How to exchange secrets with oblivious transfer. In: Technical Report TR-81. Harvard University (1981)

    Google Scholar 

  33. Schmitt, P.H., Tonin, I.: Verifying the mondex case study. In: SEFM, pp. 47–58. IEEE Computer Society (2007) ISBN 978-0-7695-2884-7

    Google Scholar 

  34. Schulte, W., Songtao, X., Smans, J., Piessens, F.: A glimpse of a verifying c compiler. In: C/C++ Verification Workshop 2007 (2007)

    Google Scholar 

  35. Yao, A.C.-C.: Protocols for secure computations (extended abstract). In: 23rd FOCS, pp. 160–164. IEEE Computer Society Press (November 1982)

    Google Scholar 

  36. Yao, A.C.-C.: How to generate and exchange secrets (extended abstract). In: 27th FOCS, pp. 162–167. IEEE Computer Society Press (October 1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Theoretical Informatics, Karlsruhe Institute of Technology, Germany

    Florian Böhl & Simon Greiner

  2. FZI Research Center for Information Technology, Germany

    Patrik Scheidecker

Authors
  1. Florian Böhl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Simon Greiner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Patrik Scheidecker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, Athens University of Economics & Business, 76, Patission Str., 10434, Athens, Greece

    Dimitris Gritzalis

  2. Department of Informatics and Telecommunications, Panepistimiopolis, National and Kapodistrian University of Athens, 15784, Athens, Greece

    Aggelos Kiayias

  3. FORTH-ICS, Vassilika Vouton, P.O. Box 1385, 711 10, Heraklion, Crete, Greece

    Ioannis Askoxylakis

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Böhl, F., Greiner, S., Scheidecker, P. (2014). Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender. In: Gritzalis, D., Kiayias, A., Askoxylakis, I. (eds) Cryptology and Network Security. CANS 2014. Lecture Notes in Computer Science, vol 8813. Springer, Cham. https://doi.org/10.1007/978-3-319-12280-9_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12280-9_12

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12279-3

  • Online ISBN: 978-3-319-12280-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation