In the field of cryptography, there has been an ongoing interest in writing easy verifiable and correct security proofs. However, this has proven a difficult task according to Bellare and Rogaway: “In our opinion, many proofs in cryptography have become essentially unverifiable. Our field may be approaching a crisis of rigor.” The EasyCrypt toolset is being developed to solve this issue. It is a proof assistant that supports the construction and verification of cryptographic proofs. In our project, we aim at extending the EasyCrypt framework by formalizing secure multiparty computation (MPC), which is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function.
The talk will give a short introduction to the EasyCrypt toolset and how to prove a statement in EasyCrypt. The second part of the talk will contain a presentation of the initial work on extending the EasyCrypt framework with a formalization of MPC. Here we look at a simple passive secure MPC protocol for addition presented by Maurer in 2004.
Since Augist 2015 Helene is a PhD student in the Cryptography Group at Aarhus University under the supervision of Claudio Orlandi and Ivan Damgård. Her subject is: Advanced Encryption Schemes and Multiparty Computation