, The lastpass password manager
The x3dh key agreement protocol, 2016. ,
The double ratchet algorithm, 2016. ,
Bringing the web up to speed with webassembly, ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.185-200, 2017. ,
Mechanising and verifying the webassembly specification, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.53-65, 2018. ,
The essence of javascript, European conference on Object-oriented programming, pp.126-150, 2010. ,
A trusted mechanised javascript specification, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.87-100, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00910135
Constant-time webassembly, 2018. ,
Verified low-level programming embedded in f*, Proceedings of the ACM on Programming Languages, vol.1, pp.1-17, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01672706
,
Dependent types and multimonadic effects in F*, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.256-270, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01265793
, Web cryptography api
A messy state of the union: Taming the composite state machines of TLS, IEEE Symposium on Security and Privacy, pp.535-552, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01114250
Implementing TLS with verified cryptographic security, IEEE Symposium on Security and Privacy, pp.445-459, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00863373
Implementing and proving the TLS 1.3 record layer, IEEE Symposium on Security and Privacy, pp.463-482, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01674096
Verified models and reference implementations for the TLS 1.3 standard candidate, IEEE Symposium on Security and Privacy, pp.483-502, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01575920
Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach, 2nd IEEE European Symposium on Security and Privacy, pp.435-450, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01575923
Modeling and verifying security protocols with the applied pi calculus and proverif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01423760
HACL*: A verified modern cryptographic library, ACM SIGSAC Conference on Computer and Communications Security (CCS), ser. CCS '17, pp.1789-1806, 2017. ,
Curve25519: new diffie-hellman speed records, Public Key Cryptography-PKC, pp.207-228, 2006. ,
Tweetnacl: A crypto library in 100 tweets, International Conference on Cryptology and Information Security in Latin America (LATINCRYPT), pp.64-83, 2014. ,
poly1305-x86.pl produces incorrect output, 2016. ,
Wrong results with Poly1305 functions, 2016. ,
Emscripten: An llvm-to-javascript compiler, ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion (OOPSLA), pp.301-312, 2011. ,
Automated analysis of security-critical javascript apis, IEEE Symposium on Security and Privacy, pp.363-378, 2011. ,
Defensive javascript, Foundations of Security Analysis and Design VII, pp.88-123, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01102144
Fully abstract compilation to javascript, ACM SIGPLAN Notices, vol.48, issue.1, pp.371-384, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00780803
Gradual typing embedded securely in javascript, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.425-438, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00940836
Dijkstra monads for free, ACM SIGPLAN Notices, vol.52, issue.1, pp.515-529, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01424794
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00415861
The security impact of a new cryptographic library, International Conference on Cryptology and Information Security in Latin America (LATINCRYPT), pp.159-176, 2012. ,
, Can i use: Webassembly
Mind the gap: Analyzing the performance of webassembly vs. native code, 2019. ,
Verifying constant-time implementations, USENIX Security Symposium, pp.53-70, 2016. ,
Secure compilation of sidechannel countermeasures: The case of cryptographic "constant-time, IEEE Computer Security Foundations Symposium (CSF), pp.328-343, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01959560
Ct-wasm: Type-driven secure cryptography for the web ecosystem, 2018. ,
On post-compromise security, IEEE 29th Computer Security Foundations Symposium (CSF), pp.164-178, 2016. ,
A formal security analysis of the signal messaging protocol, IEEE European Symposium on Security and Privacy, pp.451-466, 2017. ,
Ratcheted encryption and key exchange: The security of messaging, pp.619-650, 2017. ,
Optimal channel security against finegrained state compromise: The safety of messaging, CRYPTO, pp.33-62, 2018. ,
Towards bidirectional ratcheted key exchange, CRYPTO, pp.3-32, 2018. ,
The xeddsa and vxeddsa signature schemes, 2017. ,
Language-based defenses against untrusted browser origins, Proceedings of the 22th USENIX Security Symposium, pp.653-670, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00863372
, , pp.88-123, 2014.
Verified correctness and security of openssl HMAC, USENIX Security Symposium, pp.207-221, 2015. ,
Jasmin: Highassurance and high-speed cryptography, ACM SIGSAC Conference on Computer and Communications Security (CCS, pp.1807-1823, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01649140
Verification of a cryptographic primitive: Sha-256, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.37, issue.2, p.7, 2015. ,
Vale: Verifying high-performance cryptographic assembly code, Proceedings of the USENIX Security Symposium, 2017. ,
Automated verification of real-world cryptographic implementations, IEEE Security and Privacy, vol.14, issue.6, pp.26-33, 2016. ,