Formalising MPC-in-the-head-based zero-knowledge
Recent work has focused on the formalization of Zero-Knowledge and Multi-Party Computations separately. Here we combine those two strands of research and use EasyCrypt to formalise the security of a new class of Multi-Party Computation protocols from which zero-knowledge protocols can be constructed. This class includes MPC-in-the-head protocols such as ZKBoo and picnic. Moreover, this restricted class of MPC protocols allow us to seamlessly define simulator-based proofs of security, something which has previously only been done in a formal setting for MPC protocols limited to one round, or replaced by non-interference-based definitions.