publicações selecionadas
-
artigo académico
- Formally verifying Kyber Episode IV: Implementation correctness. IACR Transactions on Cryptographic Hardware and Embedded System. 2023
- A formal treatment of the role of verified compilers in secure computation. Journal of Logical and Algebraic Methods in Programming. 2022
- A Tool-Chain for High-Assurance Cryptographic Software. ERCIM NEWS. 2016
- Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. IACR Cryptology ePrint Archive. 2015
- Verified Implementations for Secure and Verifiable Computation. IACR Cryptology ePrint Archive. 2014
- Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. IACR Cryptology ePrint Archive. 2013
- Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. IACR Cryptology ePrint Archive. 2012
- Partial derivative automata formalized in coq. Computational Methods in Applied Sciences. 2011
- A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols. IACR Cryptology ePrint Archive. 2010
- A certifying compiler for zero-knowledge proofs of knowledge based on ¿-protocols. Computational Methods in Applied Sciences. 2010
- Verifying cryptographic software correctness with respect to reference implementations. Computational Methods in Applied Sciences. 2009
- Bounded version vectors. Computational Methods in Applied Sciences. 2004
-
artigo de conferência
- Verified Password Generation from Password Composition Policies 2022
- Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head 2021
- Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. Computational Methods in Applied Sciences. 2020
- The Last Mile: High-Assurance and High-Speed Cryptographic Implementations 2020
- A Machine-Checked Proof of Security for AWS Key Management Service 2019
- Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3 2019
- Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks. Proceedings IEEE Computer Security Foundations Symposium. 2018
- Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report) 2018
- A Fast and Verified Software Stack for Secure Function Evaluation. Proceedings of the ACM Conference on Computer and Communications Security. 2017
- Jasmin: High-Assurance and High-Speed Cryptography. Proceedings of the ACM Conference on Computer and Communications Security. 2017
- On the Formalization of Some Results of Context-Free Language Theory. Computational Methods in Applied Sciences. 2016
- Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. Computational Methods in Applied Sciences. 2016
- Verifying Constant-Time Implementations 2016
- Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations. Proceedings of the ACM Conference on Computer and Communications Security. 2013
- Deductive Verification of Cryptographic Software 2009
-
artigo de revista
- Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages. Electronic Notes in Theoretical Computer Science. 2019
- Formalization of the Pumping Lemma for Context-Free Languages. Journal of Formalized Reasoning. 2016
- Formal verification of side-channel countermeasures using self-composition. Computational Methods in Applied Sciences. 2013
- CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Computational Methods in Applied Sciences. 2012
- Deductive verification of cryptographic software. Innovations in Systems and Software Engineering. 2010
- A Tool for Programming with Interaction Nets. Electronic Notes in Theoretical Computer Science. 2008
- Token-passing Nets for Functional Languages. Electronic Notes in Theoretical Computer Science. 2008
- A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. Electronic Notes in Theoretical Computer Science. 2007
-
documento
-
livro