You are looking at a specific version 20140813:234846 of this paper. See the latest version.

Paper 2014/618

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

Florian Böhl and Simon Greiner and Patrik Scheidecker

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 Kuesters 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.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Preprint. MINOR revision.
Keywords
cryptographic protocolsinteractive theorem-provingimplementation-level analysissimulation-based security
Contact author(s)
florian boehl @ kit edu
History
2014-08-13: received
Short URL
https://ia.cr/2014/618
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.