Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89727
Título: | Machine-checked ZKP for NP relations: formally verified security proofs and implementations of MPC-in-the-head |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Correia, Manuel L. Eldefrawy, Karim Graham-Lengrand, Stéphane Pacheco, Hugo Pereira, Vitor |
Palavras-chave: | Zero-knowledge Secure multiparty computation Formal verification Implementation |
Data: | Nov-2021 |
Editora: | Association for Computing Machinery (ACM) |
Revista: | Proceedings of the ACM Conference on Computer and Communications Security |
Resumo(s): | MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/89727 |
ISBN: | 978-1-4503-8454-4 |
DOI: | 10.1145/3460120.3484771 |
ISSN: | 1543-7221 |
Versão da editora: | https://dl.acm.org/doi/pdf/10.1145/3460120.3484771 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
3460120.3484771.pdf | MPC-in-the-Head (CCS21) | 1,23 MB | Adobe PDF | Ver/Abrir |