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 Manuel Barbosa

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

2019

Machine-Checked Proofs for Cryptographic Standards

Authors
Almeida, JB; Ruet, CB; Barbosa, M; Barthe, G; Dupressoir, F; Grégoire, B; Laporte, V; Oliveira, T; Stoughton, A; Strub, PY;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2019

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

Authors
Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Koutsos, A; Laporte, V; Oliveira, T; Strub, PY;

Publication
CoRR

Abstract

2018

hnforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

Authors
Almeida, JB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B;

Publication
IEEE 31ST COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2018)

Abstract
We give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that. enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against. an information-flow policy modelling (an upper bound to) their leakage. This allows non-experts to assess the impact of performance driven authorized disclosure of intermediate values. Specifications are then compiled to multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove security-preserving compilation: protocols only leak what. is allowed by the source policy. The proof exploits a natural but previously missing correspondence between simulation-based cryptographic proofs and (composable) probabilistic non-interference. Finally, we extend our framework to justify leakage cancelling, a domain-specific optimization that allows to first write an efficient specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic preprocessing that brings leakage to the acceptable range.

2017

A Fast and Verified Software Stack for Secure Function Evaluation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Grégoire, B; Laporte, V; Pereira, V;

Publication
IACR Cryptology ePrint Archive

Abstract

2022

Execution Time Program Verification With Tight Bounds

Authors
Silva, AC; Barbosa, M; Florido, M;

Publication
CoRR

Abstract

  • 18
  • 20