Manuel Barbosa

Orcid: 0000-0002-6848-5564

According to our database1, Manuel Barbosa authored at least 83 papers between 2005 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Bare PAKE: Universally Composable Key Exchange from just Passwords.
IACR Cryptol. ePrint Arch., 2024

A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified.
IACR Cryptol. ePrint Arch., 2024

X-Wing: The Hybrid KEM You've Been Looking For.
IACR Cryptol. ePrint Arch., 2024

C'est très CHIC: A compact password-authenticated key exchange from lattice-based KEM.
IACR Cryptol. ePrint Arch., 2024

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch., 2024

X-Wing.
IACR Commun. Cryptol., 2024

2023
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.
ACM Trans. Priv. Secur., August, 2023

Formally verifying Kyber Episode IV: Implementation correctness.
IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023

Kyber terminates.
IACR Cryptol. ePrint Arch., 2023

The security of Kyber's FO-transform.
IACR Cryptol. ePrint Arch., 2023

Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$.
IACR Cryptol. ePrint Arch., 2023

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
IACR Cryptol. ePrint Arch., 2023

Formally verifying Kyber Part I: Implementation Correctness.
IACR Cryptol. ePrint Arch., 2023

Execution Time Program Verification with Tight Bounds.
Proceedings of the Practical Aspects of Declarative Languages, 2023

Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $.
Proceedings of the Advances in Cryptology - CRYPTO 2023, 2023

Rogue key and impersonation attacks on FIDO2: From theory to practice.
Proceedings of the 18th International Conference on Availability, Reliability and Security, 2023

2022
A formal treatment of the role of verified compilers in secure computation.
J. Log. Algebraic Methods Program., 2022

2021
CODBS: A cascading oblivious search protocol optimized for real-world relational database indexes.
IACR Cryptol. ePrint Arch., 2021

EasyPQC: Verifying Post-Quantum Cryptography.
IACR Cryptol. ePrint Arch., 2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
IACR Cryptol. ePrint Arch., 2021

Security Characterization of J-PAKE and its Variants.
IACR Cryptol. ePrint Arch., 2021

Algebraic Adversaries in the Universal Composability Framework.
IACR Cryptol. ePrint Arch., 2021

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

2020
Provable Security Analysis of FIDO2.
IACR Cryptol. ePrint Arch., 2020

Secure Conflict-free Replicated Data Types.
IACR Cryptol. ePrint Arch., 2020

Universally Composable Relaxed Password Authenticated Key Exchange.
IACR Cryptol. ePrint Arch., 2020

Decentralized Privacy-Preserving Proximity Tracing.
IEEE Data Eng. Bull., 2020

Decentralized Privacy-Preserving Proximity Tracing.
CoRR, 2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.
Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 2020

2019
SoK: Computer-Aided Cryptography.
IACR Cryptol. ePrint Arch., 2019

A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards.
IACR Cryptol. ePrint Arch., 2019

Perfect Forward Security of SPAKE2.
IACR Cryptol. ePrint Arch., 2019

Efficient Function-Hiding Functional Encryption: From Inner-Products to Orthogonality.
Proceedings of the Topics in Cryptology - CT-RSA 2019, 2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018
Indifferentiable Authenticated Encryption.
IACR Cryptol. ePrint Arch., 2018

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.
IACR Cryptol. ePrint Arch., 2018

2017
Labeled Homomorphic Encryption: Scalable and Privacy-Preserving Processing of Outsourced Data.
IACR Cryptol. ePrint Arch., 2017

A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch., 2017

Performance trade-offs on a secure multi-party relational database.
Proceedings of the Symposium on Applied Computing, 2017

SAFETHINGS: Data Security by Design in the IoT.
Proceedings of the 13th European Dependable Computing Conference, 2017

Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016
Foundations of Hardware-Based Attested Computation and Application to SGX.
IACR Cryptol. ePrint Arch., 2016

Secure Multiparty Computation from SGX.
IACR Cryptol. ePrint Arch., 2016

Private Functional Encryption: Indistinguishability-Based Definitions and Constructions from Obfuscation.
IACR Cryptol. ePrint Arch., 2016

A Tool-Chain for High-Assurance Cryptographic Software.
ERCIM News, 2016

Verifying Constant-Time Implementations.
Proceedings of the 25th USENIX Security Symposium, 2016

2015
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.
IACR Cryptol. ePrint Arch., 2015

ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data.
Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

2014
CAOVerif: An open-source deductive verification platform for cryptographic software implementations.
Sci. Comput. Program., 2014

The Related-Key Analysis of Feistel Constructions.
IACR Cryptol. ePrint Arch., 2014

Verified Implementations for Secure and Verifiable Computation.
IACR Cryptol. ePrint Arch., 2014

Compiling CAO: From Cryptographic Specifications to C Implementations.
Proceedings of the Principles of Security and Trust - Third International Conference, 2014

2013
Formal verification of side-channel countermeasures using self-composition.
Sci. Comput. Program., 2013

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
IACR Cryptol. ePrint Arch., 2013

On the Semantic Security of Functional Encryption Schemes.
Proceedings of the Public-Key Cryptography - PKC 2013 - 16th International Conference on Practice and Theory in Public-Key Cryptography, Nara, Japan, February 26, 2013

On the Relationship between Functional Encryption, Obfuscation, and Fully Homomorphic Encryption.
Proceedings of the Cryptography and Coding - 14th IMA International Conference, 2013

2012
Semantically Secure Functional Encryption, Revisited.
IACR Cryptol. ePrint Arch., 2012

On the Joint Security of Signature and Encryption Schemes under Randomness Reuse: Efficiency and Security Amplification.
IACR Cryptol. ePrint Arch., 2012

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols.
IACR Cryptol. ePrint Arch., 2012

Generically extending anonymization algorithms to deal with successive queries.
Proceedings of the 21st ACM International Conference on Information and Knowledge Management, 2012

2011
Practical realisation and elimination of an ECC-related software bug attack.
IACR Cryptol. ePrint Arch., 2011

Delegatable Homomorphic Encryption with Applications to Secure Outsourcing of Computation.
IACR Cryptol. ePrint Arch., 2011

Type Checking Cryptography Implementations.
Proceedings of the Fundamentals of Software Engineering - 4th IPM International Conference, 2011

2010
Deductive verification of cryptographic software.
Innov. Syst. Softw. Eng., 2010

A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols.
IACR Cryptol. ePrint Arch., 2010

A Deductive Verification Platform for Cryptographic Software.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Strong Knowledge Extractors for Public-Key Encryption Schemes.
Proceedings of the Information Security and Privacy - 15th Australasian Conference, 2010

Relations among Notions of Complete Non-malleability: Indistinguishability Characterisation and Efficient Construction without Random Oracles.
Proceedings of the Information Security and Privacy - 15th Australasian Conference, 2010

2009
Constructive and Destructive Use of Compilers in Elliptic Curve Cryptography.
J. Cryptol., 2009

Using Compilers to Enhance Cryptographic Product Development.
Proceedings of the ISSE 2009, 2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations.
Proceedings of the Formal Methods for Industrial Critical Systems, 2009

Security Analysis of Standard Authentication and Key Agreement Protocols Utilising Timestamps.
Proceedings of the Progress in Cryptology, 2009

2008
Certificateless Signcryption.
IACR Cryptol. ePrint Arch., 2008

Secure Biometric Authentication With Improved Accuracy.
IACR Cryptol. ePrint Arch., 2008

2007
Compiler Assisted Elliptic Curve Cryptography.
IACR Cryptol. ePrint Arch., 2007

Randomness Reuse: Extensions and Improvements.
Proceedings of the Cryptography and Coding, 2007

2006
Secure Cryptographic Workflow in the Standard Model.
IACR Cryptol. ePrint Arch., 2006

2005
Recursion patterns and time-analysis.
ACM SIGPLAN Notices, 2005

On the Automatic Construction of Indistinguishable Operations.
IACR Cryptol. ePrint Arch., 2005

First Steps Toward a Cryptography-Aware Language and Compiler.
IACR Cryptol. ePrint Arch., 2005

Efficient Identity-Based Key Encapsulation to Multiple Parties.
IACR Cryptol. ePrint Arch., 2005


  Loading...