A proof of security of Yao's protocol for two-party computation

Yehuda Lindell, Benny Pinkas
J Cryptology 2009 [pdf] [bibtex]

Gives a formal description and security proof of Yao's original 2PC protocol (Y86). Security is proven against semi-honest adversaries, and for deterministic, same-output functionalities. The gate-level cipher is realized as double-encryption {$E_{K_0}(E_{K_1}(M))$}, where {$E$} has an elusive and efficiently-verifiable range (i.e., it is hard to guess a valid ciphertext without the key, but easy to verify a valid ciphertext with the key).

See also: