Santiago Zanella Béguelin

According to our database1, Santiago Zanella Béguelin authored at least 43 papers between 2005 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).
IACR Cryptol. ePrint Arch., 2020


HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).
Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

Analyzing Information Leakage of Updates to Natural Language Models.
Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

2019
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch., 2019

Analyzing Privacy Loss in Updates of Natural Language Models.
CoRR, 2019

Imperfect forward secrecy: how Diffie-Hellman fails in practice.
Commun. ACM, 2019

2018
A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Verified low-level programming embedded in F.
Proc. ACM Program. Lang., 2017

A Monadic Framework for Relational Verification (Functional Pearl).
CoRR, 2017

Verified Low-Level Programming Embedded in F<sup>*</sup>.
CoRR, 2017


2016
Implementing and Proving the TLS 1.3 Record Layer.
IACR Cryptol. ePrint Arch., 2016

Downgrade Resilience in Key-Exchange Protocols.
IACR Cryptol. ePrint Arch., 2016

Dependent types and multi-monadic effects in F.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Formal Verification of Smart Contracts: Short Paper.
Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016

2014
Proving the TLS Handshake Secure (as it is).
IACR Cryptol. ePrint Arch., 2014

Probabilistic relational verification for cryptographic implementations.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk).
Proceedings of the VPT 2014. Second International Workshop on Verification and Program Transformation, 2014

2013
Probabilistic Relational Reasoning for Differential Privacy.
ACM Trans. Program. Lang. Syst., 2013

Verified indifferentiable hashing into elliptic curves.
J. Comput. Secur., 2013

Verified Computational Differential Privacy with Applications to Smart Metering.
Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, 2013

Smart meter aggregation via secret-sharing.
Proceedings of the SEGS'13, 2013

Fully automated analysis of padding-based encryption in the computational model.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

2012
Verified Security of Redundancy-Free Encryption from Rabin and RSA.
IACR Cryptol. ePrint Arch., 2012

Automated Analysis and Synthesis of Padding-Based Encryption Schemes.
IACR Cryptol. ePrint Arch., 2012

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

Computer-Aided Cryptographic Proofs.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs.
Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Computer-Aided Cryptographic Proofs.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Verified Security of Merkle-Damgård.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Verifiable Security of Boneh-Franklin Identity-Based Encryption.
Proceedings of the Provable Security - 5th International Conference, 2011

Beyond Provable Security Verifiable IND-CCA Security of OAEP.
Proceedings of the Topics in Cryptology - CT-RSA 2011, 2011

Computer-Aided Security Proofs for the Working Cryptographer.
Proceedings of the Advances in Cryptology - CRYPTO 2011, 2011

2010
Formal certification of game-based cryptographic proofs. (Certification formelle de preuves cryptographiques basées sur les séquences de jeux).
PhD thesis, 2010

Programming Language Techniques for Cryptographic Proofs.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Machine-Checked Formalization of Sigma-Protocols.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

2009
Formally Certifying the Security of Digital Signature Schemes.
Proceedings of the 30th IEEE Symposium on Security and Privacy (S&P 2009), 2009

Formal certification of code-based cryptographic proofs.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

2008
Formal Certification of ElGamal Encryption.
Proceedings of the Formal Aspects in Security and Trust, 5th International Workshop, 2008

2006
A Formal Specification of the MIDP 2.0 Security Model.
Proceedings of the Formal Aspects in Security and Trust, Fourth International Workshop, 2006

2005
Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method.
Proceedings of the Construction and Analysis of Safe, 2005


  Loading...