, The lastpass password manager

M. Marlinspike and T. Perrin, The x3dh key agreement protocol, 2016.

T. Perrin and M. Marlinspike, The double ratchet algorithm, 2016.

A. Haas, A. Rossberg, D. L. Schuff, B. L. Titzer, M. Holman et al., Bringing the web up to speed with webassembly, ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.185-200, 2017.

C. Watt, Mechanising and verifying the webassembly specification, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.53-65, 2018.

A. Guha, C. Saftoiu, and S. Krishnamurthi, The essence of javascript, European conference on Object-oriented programming, pp.126-150, 2010.

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis et al., 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

J. Renner, S. Cauligi, and D. Stefan, Constant-time webassembly, 2018.

J. Protzenko, J. Zinzindohoué, A. Rastogi, T. Ramananandro, P. Wang et al., 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

N. Swamy, C. Hricu, C. Keller, A. Rastogi, A. Delignat-lavaud et al.,

S. Zinzindohoue and . Zanella-béguelin, 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

B. Beurdouche, K. Bhargavan, A. Delignat-lavaud, C. Fournet, M. Kohlweiss et al., 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

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with verified cryptographic security, IEEE Symposium on Security and Privacy, pp.445-459, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863373

A. Delignat-lavaud, C. Fournet, M. Kohlweiss, J. Protzenko, A. Rastogi et al., 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

K. Bhargavan, B. Blanchet, and N. Kobeissi, 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

N. Kobeissi, K. Bhargavan, and B. Blanchet, 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

B. Blanchet, 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

J. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, HACL*: A verified modern cryptographic library, ACM SIGSAC Conference on Computer and Communications Security (CCS), ser. CCS '17, pp.1789-1806, 2017.

D. J. Bernstein, Curve25519: new diffie-hellman speed records, Public Key Cryptography-PKC, pp.207-228, 2006.

D. J. Bernstein, B. Van-gastel, W. Janssen, T. Lange, P. Schwabe et al., Tweetnacl: A crypto library in 100 tweets, International Conference on Cryptology and Information Security in Latin America (LATINCRYPT), pp.64-83, 2014.

D. Benjamin, poly1305-x86.pl produces incorrect output, 2016.

H. Böck, Wrong results with Poly1305 functions, 2016.

A. Zakai, Emscripten: An llvm-to-javascript compiler, ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion (OOPSLA), pp.301-312, 2011.

A. Taly, Ú. Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra, Automated analysis of security-critical javascript apis, IEEE Symposium on Security and Privacy, pp.363-378, 2011.

K. Bhargavan, A. Delignat-lavaud, and S. Maffeis, Defensive javascript, Foundations of Security Analysis and Design VII, pp.88-123, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102144

C. Fournet, N. Swamy, J. Chen, P. Dagand, P. Strub et al., Fully abstract compilation to javascript, ACM SIGPLAN Notices, vol.48, issue.1, pp.371-384, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00780803

N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen et al., 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

D. Ahman, C. Hri?cu, K. Maillard, G. Martínez, G. Plotkin et al., Dijkstra monads for free, ACM SIGPLAN Notices, vol.52, issue.1, pp.515-529, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01424794

X. Leroy, 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

D. J. Bernstein, T. Lange, and P. Schwabe, 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

A. Jangda, B. Powers, A. Guha, and E. Berger, Mind the gap: Analyzing the performance of webassembly vs. native code, 2019.

J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, and M. Emmi, Verifying constant-time implementations, USENIX Security Symposium, pp.53-70, 2016.

G. Barthe, B. Grégoire, and V. Laporte, 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

C. Watt, J. Renner, N. Popescu, S. Cauligi, and D. Stefan, Ct-wasm: Type-driven secure cryptography for the web ecosystem, 2018.

K. Cohn-gordon, C. J. Cremers, and L. Garratt, On post-compromise security, IEEE 29th Computer Security Foundations Symposium (CSF), pp.164-178, 2016.

K. Cohn-gordon, C. J. Cremers, B. Dowling, L. Garratt, and D. Stebila, A formal security analysis of the signal messaging protocol, IEEE European Symposium on Security and Privacy, pp.451-466, 2017.

M. Bellare, A. C. Singh, J. Jaeger, M. Nyayapati, and I. Stepanovs, Ratcheted encryption and key exchange: The security of messaging, pp.619-650, 2017.

J. Jaeger and I. Stepanovs, Optimal channel security against finegrained state compromise: The safety of messaging, CRYPTO, pp.33-62, 2018.

B. Poettering and P. Rösler, Towards bidirectional ratcheted key exchange, CRYPTO, pp.3-32, 2018.

T. Perrin, The xeddsa and vxeddsa signature schemes, 2017.

K. Bhargavan, A. Delignat-lavaud, and S. Maffeis, 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

-. and D. Javascript, , pp.88-123, 2014.

L. Beringer, A. Petcher, K. Q. Ye, and A. W. Appel, Verified correctness and security of openssl HMAC, USENIX Security Symposium, pp.207-221, 2015.

J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire et al., 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

A. W. Appel, Verification of a cryptographic primitive: Sha-256, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.37, issue.2, p.7, 2015.

B. Bond, C. Hawblitzel, M. Kapritsos, K. R. Leino, J. R. Lorch et al., Vale: Verifying high-performance cryptographic assembly code, Proceedings of the USENIX Security Symposium, 2017.

A. Tomb, Automated verification of real-world cryptographic implementations, IEEE Security and Privacy, vol.14, issue.6, pp.26-33, 2016.