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
About
Download Photo HD

About

I am a lecturer at the Department of Computer Science in the Faculty of Science of the University of Porto (DCC-FCUP) and a researcher at HASLab/INESC TEC. My research interests lie in Cryptography and Information Security and its intersection with Program Verification.

I hold a Ph.D. in Electrical and Electronic Engineering from the Newcastle University, an M.Sc. from the same University, and a degree in Electrical and Computer Engineering from the Faculty of Engineering of the University of Porto. In the past I have been a visiting researcher at the University of Bristol, IT Porto and École Normale Supérieure.

I have been working on the development of high-assurance cryptographic implementations for the last 10 years, aiming to bridge the gap between theoretical security and real-world security. I am particularly interested in provable security and its interplay with the formal verification of cryptographic proofs and cryptographic software implementations.

For information on my research, projects and publications, please see my page at HASLab.

For information on my teaching activities, please see my institutional page at FCUP.

Interest
Topics
Details

Details

  • Name

    Manuel Barbosa
  • Role

    Research Coordinator
  • Since

    01st November 2011
  • Nationality

    Portugal
  • Contacts

    +351253604440
    manuel.barbosa@inesctec.pt
008
Publications

2019

Efficient Function-Hiding Functional Encryption: From Inner-Products to Orthogonality

Authors
Barbosa, M; Catalano, D; Soleimanian, A; Warinschi, B;

Publication
Topics in Cryptology - CT-RSA 2019 - The Cryptographers' Track at the RSA Conference 2019, San Francisco, CA, USA, March 4-8, 2019, Proceedings

Abstract
We construct functional encryption (FE) schemes for the orthogonality (OFE) relation where each ciphertext encrypts some vector (Formula Presented) and each decryption key, associated to some vector (Formula Presented), allows to determine if (Formula Presented) is orthogonal to (Formula Presented) or not. Motivated by compelling applications, we aim at schemes which are function hidding, i.e. (Formula Presented) is not leaked. Our main contribution are two such schemes, both rooted in existing constructions of FE for inner products (IPFE), i.e., where decryption keys reveal the inner product of (Formula Presented) and (Formula Presented). The first construction builds upon the very efficient IPFE by Kim et al. (SCN 2018) but just like the original scheme its security holds in the generic group model (GGM). The second scheme builds on recent developments in the construction of efficient IPFE schemes in the standard model and extends the work of Wee (TCC 2017) in leveraging these results for the construction of FE for Boolean functions. Conceptually, both our constructions can be seen as further evidence that shutting down leakage from inner product values to only a single bit for the orthogonality relation can be done with little overhead, not only in the GGM, but also in the standard model. We discuss potential applications of our constructions to secure databases and provide efficiency benchmarks. Our implementation shows that the first scheme is extremely fast and ready to be deployed in practical applications. © 2019, Springer Nature Switzerland AG.

2019

A Machine-Checked Proof of Security for AWS Key Management Service

Authors
Almeida, JB; Barbosa, M; Barthe, G; Campagna, M; Cohen, E; Gregoire, B; Pereira, V; Portela, B; Strub, PY; Tasiran, S;

Publication
PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19)

Abstract
We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date.

2019

Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3

Authors
Almeida, JB; Baritel Ruet, C; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Oliveira, T; Stoughton, A; Strub, PY;

Publication
PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19)

Abstract
We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.

2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3

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

Publication
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019.

Abstract

2019

A Machine-Checked Proof of Security for AWS Key Management Service

Authors
Almeida, JB; Barbosa, M; Barthe, G; Campagna, M; Cohen, E; Grégoire, B; Pereira, V; Portela, B; Strub, PY; Tasiran, S;

Publication
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019.

Abstract

Supervised
thesis

2019

Trade-offs between privacy and efficiency on databases

Author
Rogério António da Costa Pontes

Institution
UP-FCUP

2019

High-speed and High-assurance Cryptographic Software

Author
Tiago Filipe Azevedo Oliveira

Institution
UP-FCUP

2019

Integrated verification of cryptographic security proofs and implementations

Author
Vitor Manuel Parreira Pereira

Institution
UP-FCUP

2018

Security Analysis of a Closed-Source Signal Protocol Implementation

Author
João Diogo Gaspar Alves

Institution
UP-FCUP

2018

Computação colaborativa segura num cenário de gestão de risco financeiro

Author
Tiago André Ferreira Fernandes

Institution
UP-FCUP