Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by HASLab

2021

Zipping Strategies and Attribute Grammars

Authors
Macedo, JN; Viera, M; Saraiva, J;

Publication
CoRR

Abstract

2021

Green Software Lab: Towards an Engineering Discipline for Green Software

Authors
Abreu, R; Couto, M; Cruz, L; Cunha, J; Fernandes, JP; Pereira, R; Perez, A; Saraiva, J;

Publication
CoRR

Abstract

2021

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

Authors
Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Graham-Lengrand, S; Pacheco, H; Pereira, V;

Publication
CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY

Abstract
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.

2021

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

Authors
Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2021

Towards Formal Verification of Password Generation Algorithms used in Password Managers

Authors
Grilo, M; Ferreira, JF; Almeida, JB;

Publication
CoRR

Abstract

2021

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

Authors
Bacelar Almeida, JC; Barbosa, M; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V;

Publication
CoRR

Abstract

  • 46
  • 255