Computer aided proofs in cryptography: an overview
The goal of modern cryptography is to design efficient constructions that simultaneously achieve some desired functionality and provable security against resource bounded adversaries. Over the years, the realm of cryptography has expanded from basic functionalities such as encryption, decryption and key agreement, to elaborate functionalities such as zero knowledge protocols, secure multiparty computation, and more recently verifiable computation. In many cases, these elaborate functionalities can only be achieved through cryptographic systems, in which several elementary constructions interact. As a consequence of the evolution towards more complex functionalities, cryptographic proofs have become significantly more involved, and more difficult to check. Several cryptographers have therefore advocated the use of tool supported frameworks for building and verifying proofs; the most vivid recommendation for using computer support is elaborated in a farseeing article [5] in which Shai Halevi describes a potential approach for realizing this vision.