???global.info.a_carregar???
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 INESC TEC. My research interests lie in Cryptography and Information Security and Formal 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, École Normale Supérieure, Inria Sophia-Antipolis and Bar-Ilan University. I have been working on the development of high-assurance cryptographic implementations for more than 10 years, bridging 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.
Ler resumo completo ↓
Identificação

Identificação pessoal

Nome completo
Manuel Barbosa

Nomes de citação

  • Barbosa, Manuel

Identificadores de autor

Ciência ID
481F-471F-BDDA
ORCID iD
0000-0002-6848-5564
Google Scholar ID
https://scholar.google.com/citations?user=jQp2AGAAAAAJ&hl=en
Researcher Id
C-3095-2008
Scopus Author Id
13609819600

Moradas

  • Departamento de Ciência de Computadores, Fauldade de Ciências da Universidade do Porto, Rua Campo Alegre 1055, 4169-007, Porto, Porto, Portugal (Profissional)

Websites

Domínios de atuação

  • Ciências Exatas - Ciências da Computação e da Informação - Ciências da Computação
Produções

Publicações

Artigo em conferência
  1. Silva, AC; Barbosa, M; Florido, M. "Execution Time Program Verification with Tight Bounds". 2023.
    10.1007/978-3-031-24841-2_4
  2. Barbosa, M; Cirne, A; Esquível, L. "Rogue key and impersonation attacks on FIDO2: From theory to practice". 2023.
    10.1145/3600160.3600174
  3. Barbosa, M; Dupressoir, F; Grégoire, B; Hülsing, A; Meijers, M; Strub, PY. "Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $". 2023.
  4. Barbosa, M; Barthe, G; Doczkal, C; Don, J; Fehr, S; Grégoire, B; Huang, YH; et al. "Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium". 2022.
    10.1007/978-3-031-38554-4_12
  5. Barbosa, M; Barthe, G; Fan, X; Grégoire, B; Hung, SH; Katz, J; Strub, PY; Wu, X; Zhou, L. "EasyPQC: Verifying Post-Quantum Cryptography". Trabalho apresentado em ACM SIGSAC Conference on Computer and Communications Security - CCS, 2021.
    10.1145/3460120.3484567
  6. Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V. "Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head". Trabalho apresentado em ACM SIGSAC Conference on Computer and Communications Security - CCS, 2021.
    10.1145/3460120.3484771
  7. Barbosa, M; Barthe, G; Grégoire, B; Koutsos, A; Strub, PY. "Mechanized Proofs of Adversarial Complexity and Application to Universal Composability". Trabalho apresentado em ACM SIGSAC Conference on Computer and Communications Security - CCS, 2021.
    10.1145/3460120.3484548
  8. Abdalla, M; Barbosa, M; Katz, J; Loss, J; Xu, J. "Algebraic Adversaries in the Universal Composability Framework". Trabalho apresentado em ASIACRYPT, 2021.
    10.1007/978-3-030-92078-4_11
  9. Pontes, R; Portela, B; Barbosa, M; Vilaca, R. "CODBS: A cascading oblivious search protocol optimized for real-world relational database indexes". Trabalho apresentado em SRDS, 2021.
    10.1109/srds53918.2021.00026
  10. Barbosa, M; Ferreira, B; Marques, J; Portela, B; Preguica, N. "Secure Conflict-free Replicated Data Types". Trabalho apresentado em ICDCN, 2021.
    10.1145/3427796.3427831
  11. Barbosa, M; Barthe, G; Bhargavan, K; Blanchet, B; Cremers, C; Liao, K; Parno, B. "SoK: Computer-Aided Cryptography". Trabalho apresentado em IEEE Symposium on Security and Privacy, 2021.
  12. Barbosa, M; Boldyreva, A; Chen, S; Warinschi, B. "Provable Security Analysis of FIDO2". Trabalho apresentado em CRYPTO, 2021.
    10.1007/978-3-030-84252-9_5
  13. Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Koutsos, A; Laporte, V; Oliveira, T; Strub, PY. "The Last Mile: High-Assurance and High-Speed Cryptographic Implementations". Trabalho apresentado em IEEE Symposium on Security and Privacy, 2020.
    10.1109/sp40000.2020.00028
  14. Abdalla, M; Barbosa, M; Bradley, T; Jarecki, S; Katz, J; Xu, JY. "Universally Composable Relaxed Password Authenticated Key Exchange". Trabalho apresentado em CRYPTO, 2020.
    10.1007/978-3-030-56784-2_10
  15. Almeida, JB; Barbosa, M; Barthe, G; Laporte, V; Oliveira, T. "Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification". Trabalho apresentado em INDOCRYPT, 2020.
    10.1007/978-3-030-65277-7_6
  16. Barbosa, M; Catalano, D; Soleimanian, A; Warinschi, B. "Efficient Function-Hiding Functional Encryption: From Inner-Products to Orthogonality". Trabalho apresentado em RSA Conference Cryptographers Track, 2019.
    10.1007/978-3-030-12612-4_7
  17. Almeida, JB; Barbosa, M; Barthe, G; Campagna, M; Cohen, E; Gregoire, B; Pereira, V; et al. "A Machine-Checked Proof of Security for AWS Key Management Service". Trabalho apresentado em ACM SIGSAC Conference on Computer and Communications Security - CCS, 2019.
    10.1145/3319535.3354228
  18. Almeida, JB; Baritel Ruet, C; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; et al. "Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3". Trabalho apresentado em ACM SIGSAC Conference on Computer and Communications Security - CCS, 2019.
    10.1145/3319535.3363211
  19. Barbosa, M; Farshim, P. "Indifferentiable Authenticated Encryption". Trabalho apresentado em Advances in Cryptology CRYPTO, 2018.
    10.1007/978-3-319-96884-1_7
  20. Almeida, JB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B. "Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks". Trabalho apresentado em Computer Security Foundations (CSF), 2018.
    10.1109/csf.2018.00017
  21. Barbosa, M; Catalano, D; Fiore, D. "Labeled Homomorphic Encryption - Scalable and Privacy-Preserving Processing of Outsourced Data". Trabalho apresentado em European Symposium on Research in Computer Security, 2017.
    10.1007/978-3-319-66402-6_10
  22. Bahmani, R; Barbosa, M; Brasser, F; Portela, B; Sadeghi, AR; Scerri, G; Warinschi, B. "Secure Multiparty Computation from SGX". Trabalho apresentado em Financial Cryptography, 2017.
    10.1007/978-3-319-70972-7_27
  23. Almeida, JB; Barbosa, M; Barthe, G; Blot, A; Grégoire, B; Laporte, V; Oliveira, T; et al. "Jasmin: High-Assurance and High-Speed Cryptography". Trabalho apresentado em ACM Computer and Communications Security, 2017.
    10.1145/3133956.3134078
  24. Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Laporte, Vincent; Pereira, Vitor. "A Fast and Verified Software Stack for Secure Function Evaluation". Trabalho apresentado em ACM SIGSAC Conference on Computer and Communications Security - CCS, 2017.
    10.1145/3133956.3134017
  25. Arriaga, A; Barbosa, M; Farshim, P. "Private Functional Encryption: Indistinguishability-Based Definitions and Constructions from Obfuscation". Trabalho apresentado em INDOCRYPT, 2016.
    10.1007/978-3-319-49890-4_13
  26. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Emmi, M. "Verifying Constant-Time Implementations". Trabalho apresentado em USENIX Security, 2016.
  27. Barbosa, Manuel; Portela, Bernardo; Scerri, Guillaume; Warinschi, Bogdan. "Foundations of Hardware-Based Attested Computation and Application to SGX". Trabalho apresentado em IEEE European Symposium on Security and Privacy (EuroS&P), 2016.
    10.1109/eurosp.2016.28
  28. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F. "Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC". Trabalho apresentado em Fast Software Encryption, 2016.
    10.1007/978-3-662-52993-5_9
  29. Michael Backes; Manuel Barbosa; Dario Fiore; Raphael M. Reischuk. "ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data". Trabalho apresentado em IEEE Symposium on Security and Privacy, 2015.
    10.1109/sp.2015.24
  30. Barbosa, M; Farshim, P. "The Related-Key Analysis of Feistel Constructions". Trabalho apresentado em Fast Software Encryption, 2015.
    10.1007/978-3-662-46706-0_14
  31. Barbosa, M; Castro, D; Silva, PF. "Compiling CAO: From cryptographic specifications to C implementations". Trabalho apresentado em Principles of Security and Trust, 2014.
    10.1007/978-3-642-54792-8_13
  32. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F. "Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations". Trabalho apresentado em ACM Computer and Communications Security, 2013.
    10.1145/2508859.2516652
  33. Alwen, J; Barbosa, M; Farshim, P; Gennaro, R; Gordon, SD; Tessaro, S; Wilson, DA. "On the relationship between functional encryption, obfuscation, and fully homomorphic encryption". Trabalho apresentado em IMA Cryptography and Coding, 2013.
    10.1007/978-3-642-45239-0-5
  34. Barbosa, M.; Farshim, P.. "On the semantic security of functional encryption schemes". Trabalho apresentado em Public Key Cryptography, 2013.
    10.1007/978-3-642-36362-7_10
  35. Barbosa, M.; Pinto, A.; Gomes, B.. "Generically extending anonymization algorithms to deal with successive queries". Trabalho apresentado em Conference on Information and Knowledge Management,, 2012.
    10.1145/2396761.2398440
  36. Arriaga, A.; Barbosa, M.; Farshim, P.. "On the joint security of signature and encryption schemes under randomness reuse: Efficiency and security amplification". Trabalho apresentado em Applied Cryptography and Network Security, 2012.
    10.1007/978-3-642-31284-7_13
  37. Barbosa, M.; Moss, A.; Page, D.; Rodrigues, N.F.; Silva, P.F.. "Type checking cryptography implementations". Trabalho apresentado em Fundamentals of Software Engineering, 2012.
    10.1007/978-3-642-29320-7_21
  38. Almeida, J.B.; Barbosa, M.; Bangerter, E.; Barthe, G.; Krenn, S.; Béguelin, S.Z.. "Full proof cryptography: Verifiable compilation of efficient zero-knowledge protocols". Trabalho apresentado em ACM Computer and Communications Security (CCS), 2012.
    10.1145/2382196.2382249
  39. Brumley, B.B.; Barbosa, M.; Page, D.; Vercauteren, F.. "Practical realisation and elimination of an ECC-related software bug attack". Trabalho apresentado em RSA Conference Cryptographers Track, 2012.
    10.1007/978-3-642-27954-6_11
  40. Barbosa, M.; Farshim, P.. "Delegatable homomorphic encryption with applications to secure outsourcing of computation". Trabalho apresentado em RSA Conference Cryptographers Track, 2012.
    10.1007/978-3-642-27954-6_19
  41. Barbosa, M.; Farshim, P.. "Strong knowledge extractors for public-key encryption schemes". Trabalho apresentado em Australasian Conference on Information Security and Privacy, 2010.
    10.1007/978-3-642-14081-5_11
  42. Barbosa, M.; Farshim, P.. "Relations among notions of complete non-malleability: Indistinguishability characterisation and efficient construction without random oracles". Trabalho apresentado em Australasian Conference on Information Security and Privacy, 2010.
    10.1007/978-3-642-14081-5_10
  43. Almeida, J.B.; Bangerter, E.; Barbosa, M.; Krenn, S.; Sadeghi, A.-R.; Schneider, T.. "A certifying compiler for zero-knowledge proofs of knowledge based on Sigma-protocols". Trabalho apresentado em European Symposium on Research in Computer Security, 2010.
    10.1007/978-3-642-15497-3_10
  44. Almeida, J.B.; Barbosa, M.; Sousa Pinto, J.; Vieira, B.. "Verifying cryptographic software correctness with respect to reference implementations". Trabalho apresentado em Formal Methods for Industrial Critical Systems, 2009.
    10.1007/978-3-642-04570-7_5
  45. Barbosa, M.; Farshim, P.. "Security analysis of standard authentication and key agreement protocols utilising timestamps". Trabalho apresentado em Africacrypt, 2009.
    10.1007/978-3-642-02384-2_15
  46. Barbosa, M.; Farshim, P.. "Certificateless signcryption". Trabalho apresentado em ACM Symposium on Information, Computer and Communications Security, ASIACCS, 2008.
    10.1145/1368310.1368364
  47. Barbosa, M.; Brouard, T.; Cauchie, S.; De Sousa, S.M.. "Secure biometric authentication with improved accuracy". Trabalho apresentado em Australasian Conference on Information Security and Privacy, 2008.
    10.1007/978-3-540-70500-0-3
  48. Barbosa, M.; Farshim, P.. "Randomness reuse: Extensions and improvements". Trabalho apresentado em IMA Cryptography and Coding, 2007.
    10.1007/978-3-540-77272-9_16
  49. Barbosa, M.; Moss, A.; Page, D.. "Compiler assisted elliptic curve cryptography". Trabalho apresentado em On the Move to Meaningful Internet Systems, 2007.
    10.1007/978-3-540-76843-2_46
  50. Barbosa, M; Farshim, P. "Secure cryptographic workflow in the standard model". Trabalho apresentado em INDOCRYPT, 2006.
    10.1007/11941378_27
  51. Barbosa, M.; Page, D.. "On the automatic construction of indistinguishable operations". Trabalho apresentado em Cryptography and Coding, 2005.
    10.1007/11586821_16
  52. Barbosa, M.; Farshim, P.. "Efficient identity-based key encapsulation to multiple parties". Trabalho apresentado em Cryptography and Coding, 2005.
    10.1007/11586821_28
  53. Barbosa, Manuel B.M.; da Silva Carvalho, Adriano; Farsi, Mohammed. "CANopen I/O module: Simple and efficient system integration". Trabalho apresentado em Annual Conference of the IEEE Industrial Electronics Society (IECON), 1998.
Artigo em revista
  1. Barbosa, M; Barthe, G; Gregoire, B; Koutsos, A; Strub, PY. "Mechanized Proofs of Adversarial Complexity and Application to Universal Composability". ACM TRANSACTIONS ON PRIVACY AND SECURITY (2023):
    10.1145/3589962
  2. Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; et al. "Formally verifying Kyber Episode IV: Implementation correctness". IACR Trans. Cryptogr. Hardw. Embed. Syst. (2023):
    10.46586/tches.v2023.i3.164-193
  3. Bacelar Almeida, JC; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B. "A formal treatment of the role of verified compilers in secure computation". Journal of Logical and Algebraic Methods in Programming (2022):
    10.1016/j.jlamp.2021.100736
  4. Silva, AC; Barbosa, M; Florido, M. "Execution Time Program Verification With Tight Bounds". CoRR (2022):
  5. Troncoso, C; Payer, M; Hubaux, JP; Salathé, M; Larus, JR; Bugnion, E; Lueks, W; et al. "Decentralized Privacy-Preserving Proximity Tracing". IEEE Data Eng. Bull. (2020):
  6. Bacelar Almeida, J.; Barbosa, M.; Pinto, J.S.; Vieira, B.. "Formal verification of side-channel countermeasures using self-composition". Science of Computer Programming 78 7 (2013): 796-812. http://www.scopus.com/inward/record.url?eid=2-s2.0-84877581548&partnerID=MN8TOARS.
    10.1016/j.scico.2011.10.008
  7. Almeida, J.B.; Barbosa, M.; Filliâtre, J.-C.; Pinto, J.S.; Vieira, B.. "CAOVerif: An open-source deductive verification platform for cryptographic software implementations". Science of Computer Programming (2012): http://www.scopus.com/inward/record.url?eid=2-s2.0-84867740990&partnerID=MN8TOARS.
    10.1016/j.scico.2012.09.019
  8. Barbosa, M; Pinto, JS; Filliâtre, JC; Vieira, B. "A Deductive Verification Platform for Cryptographic Software". ECEASST (2010):
  9. Almeida, J.B.; Barbosa, M.; Pinto, J.S.; Vieira, B.. "Deductive verification of cryptographic software". Innovations in Systems and Software Engineering 6 3 (2010): 203-218. http://www.scopus.com/inward/record.url?eid=2-s2.0-77956423308&partnerID=MN8TOARS.
    10.1007/s11334-010-0127-y
  10. Barbosa, M.; Moss, A.; Page, D.. "Constructive and destructive use of compilers in elliptic curve cryptography". Journal of Cryptology 22 2 (2009): 259-281. http://www.scopus.com/inward/record.url?eid=2-s2.0-64249159739&partnerID=MN8TOARS.
    10.1007/s00145-008-9023-0
  11. Barbosa, M.; Cunha, A.; Pinto, J.S.. "Recursion patterns and time-analysis". ACM SIGPLAN Notices 40 5 (2005): 45-54. http://www.scopus.com/inward/record.url?eid=2-s2.0-33745239605&partnerID=MN8TOARS.
    10.1145/1071221.1071226
  12. Farsi, M.; Ratcliff, K.; Barbosa, M.. "Overview of controller area network". Computing and Control Engineering Journal 10 3 (1999): 113-120. http://www.scopus.com/inward/record.url?eid=2-s2.0-0032651654&partnerID=MN8TOARS.
    10.1049/cce:19990304
  13. Farsi, M; Ratcliff, K; Barbosa, M. "An introduction to CANopen". COMPUTING & CONTROL ENGINEERING JOURNAL (1999):
    10.1049/cce:19990405
Atividades

Arbitragem científica em conferência

Nome da conferência Local da conferência
2021 - 2022 TCHES 2022
2021 - 2022 IEEE Computer Security Foundations Symposium (CSF) 2022
2021 - 2021 ASIACRYPT 2021 IACR
2021 - 2021 INDOCRYPT 2021
2020 - 2021 IEEE Computer Security Foundations Symposium (CSF)
2020 - 2021 Public Key Cryptography 2021 IACR
2020 - 2021 Conference on Cryptographic Hardware and Embedded Systems (CHES 2021) IACR
2020 - 2020 Security and Cryptography for Networks (SCN)
2019 - 2020 IEEE Computer Security Foundations Symposium (CSF)
2019 - 2019 Real World Cryptography
2019 - 2019 Advances in Cryptology CRYPTO
2018 - 2018 Security and Cryptography for Networks, (SCN)

Membro de associação

Nome da associação Tipo de participação
2015 - Atual International Association for Cryptologic Research (IACR)