Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy +3

MPC-in-the-Head (MitH) is a general framework that allows constructing efficient Zero Knowledge protocols for general NP-relations from secure multiparty computation (MPC) protocol…