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
IACR Commun. Cryptol., 2024
A Tight Security Proof for SPHINCS<sup>+</sup>, Formally Verified.
Proceedings of the Advances in Cryptology - ASIACRYPT 2024, 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
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