, fun PS_crypto_AESCTREncrypt(key, iv, bitstring):bitstring. 9 reduc forall k:key, i:iv, m:bitstring; PS_crypto_AESCTRDecrypt( 10 k, i, PS_crypto_AESCTREncrypt(k, i, m)) = m

, letfun fun_AKEResponse(me:me, them:them, msg:msg) = 13 let e = PS_crypto_random32Bytes(string_80) in let ge = PS_crypto_DH25519(e, key_83) in 14 let shared = fun_TDH0(keypair_get_priv(me_get_identity(me)), e, them_get_identity(them), msg_get_prekey(msg), msg_get_ephemeral(msg

, Type_key_toBitstring( msg_get_prekey(msg)), msg_get_prekeySig(msg)), string_56) in 16 let validSig = PS_crypto_checkED25519(them_get_identity(them)

, 18 query attacker(secMsg1). query attacker(secMsg2)

, event Send(key, key, bitstring). event Recv(key, key, bitstring)

, them:them) = value of type plaintext and produces a value of type plaintext. This constructor is paired with a reductor, issecretdiff, that simply reveals whether its input value was constructed using secretdiff

, = bkdf(vk, capsulecorp) in 6 let pv = pvcalc(vsp

, new diffx:plaintext; 11 writeBlock(vk, w, sk, secretdiff(diffx))

, The writeBlock process is self-explanatory: 1 let writeBlock( 2 vk:key, w:principal, sk:key, vol.diffx, p.plaintext

, vek:key, vmk:key, vsp:key, vid:key

, Reader Client Processes The reader process running under participant identity R comes equipped with a value U V f p ?? HMAC(U V pk , U ) that serves as a fingerprint for authenticating public identities and their public signing keys out of band. Mirroring the writer processes above, the reader process begins by similarly generating the requisite values and communicating them over the network. Then, an unbounded execution of the readBlock process occurs, vol.1

, vek:key, vmk:key, vsp:key, vid:key

, = bkdf(vk, capsulecorp) in 8 let pv = pvcalc(vsp

, ProofSent(r, pv)

, !(readBlock(vk, r, ufp))

U. and U. V-pk-u-v-pv, with a header matching the V id value that the reader was able to obtain using the V k the process was initialized with. Then, the internal U V f p and U V pv are checked against the candidate values received over the network. If the check succeeds, a ProofVerified event is emitted. Then, an encrypted diff along with its signature is received over the network with a header matching, The readBlock process receives over the network a triple of candidate values for, vol.1

, = bkdf(vk, capsulecorp) in

, 11 let ufp0 = hmac(upk0, prin2bit(user0)) in 12 let upv = pvcalc(vsp, vid, user0, upk0) in 13 if ((ufp0 = ufp) && (upv0 = upv)) then ( 14 event ProofVerified

N. Unger, S. Dechand, J. Bonneau, S. Fahl, H. Perl et al., SoK: Secure messaging, IEEE Symposium on Security & Privacy (Oakland), 2015.

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

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

C. Garman, M. Green, G. Kaptchuk, I. Miers, and M. Rushanan, Dancing on the lip of the volcano: Chosen ciphertext attacks on apple imessage, USENIX Security Symposium, pp.655-672, 2016.

N. Borisov, I. Goldberg, and E. A. Brewer, Off-the-record communication, or, why not to use PGP, Proceedings of the 2004 ACM Workshop on Privacy in the Electronic Society, pp.77-84, 2004.

J. Bonneau and A. Morrison, Finite State Security Analysis of OTR Version 2, 2006.

P. Rösler, C. Mainka, and J. Schwenk, More is less: On the end-toend security of group chats in signal, whatsapp, and threema, 2018.

L. Armasu, Signal desktop affected by two similar remote code execution bugs, 2018.

J. Dunn, Serious xss vulnerability discovered in signal, 2018.

K. E. Hickman, The SSL protocol, IETF Internet Draft, 1995.

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.2. IETF RFC 5246, 2008.

D. Wagner and B. Schneier, Analysis of the SSL 3.0 protocol, USENIX Electronic Commerce, 1996.

B. Möller, T. Duong, and K. Kotowicz, This POODLE bites: exploiting the SSL 3.0 fallback, 2014.

N. Aviram, S. Schinzel, J. Somorovsky, N. Heninger, M. Dankel et al., DROWN: breaking TLS using SSLv2, USENIX Security Symposium, pp.689-706, 2016.

N. Alfardan, J. Daniel, K. G. Bernstein, B. Paterson, J. Poettering et al., On the security of RC4 in TLS, USENIX Security Symposium, pp.305-320, 2013.

M. Vanhoef and F. Piessens, All your biases belong to us: Breaking RC4 in WPA-TKIP and TLS, USENIX Security Symposium, pp.97-112, 2015.

J. Nadhem, K. G. Alfardan, and . Paterson, Lucky thirteen: Breaking the TLS and DTLS record protocols, 2013 IEEE Symposium on Security and Privacy (SP 2013), pp.526-540, 2013.

D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green et al., Imperfect forward secrecy: How Diffie-Hellman fails in practice, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.5-17, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01982426

K. Bhargavan and G. Leurent, Transcript collision attacks: Breaking authentication in TLS, IKE, and SSH, ISOC Network and Distributed System Security Symposium (NDSS), 2016.
URL : https://hal.archives-ouvertes.fr/hal-01244855

E. Rescorla, M. Ray, S. Dispensa, and N. Oskov, TLS renegotiation indication extension, IETF RFC, vol.5746, 2010.

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Pironti, and P. Strub, Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS, IEEE Symposium on Security & Privacy (Oakland), pp.98-113, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102259

N. Mavrogiannopoulos, F. Vercauteren, V. Velichkov, and B. Preneel, A cross-protocol attack on the TLS protocol, ACM CCS, 2012.

G. Kenneth, T. Paterson, and . Van-der-merwe, Reactive and proactive standardisation of TLS, Security Standardisation Research (SSR), pp.160-186, 2016.

U. Maurer and B. Tackmann, On the soundness of authenticate-thenencrypt: formalizing the malleability of symmetric encryption, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.505-515, 2010.

T. Kenneth-g-paterson, T. Ristenpart, and . Shrimpton, Tag size does matter: Attacks and proofs for the TLS record protocol, ASIACRYPT, pp.372-389, 2011.

T. Jager, F. Kohlar, S. Schäge, and J. Schwenk, On the security of TLS-DHE in the standard model, CRYPTO 2012, pp.273-293, 2012.

H. Krawczyk, K. G. Paterson, and H. Wee, On the security of the TLS protocol: A systematic analysis, CRYPTO 2013, pp.429-448, 2013.

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-207, 1983.

S. Chaki and A. Datta, Aspier: An automated framework for verifying security protocol implementations, 22nd IEEE Computer Security Foundations Symposium, pp.172-185, 2009.

K. Bhargavan, C. Fournet, R. Corin, and E. Z?linescu, Verified cryptographic implementations for TLS, ACM TOPLAS, vol.15, issue.1, p.32, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863381

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

G. Lowe, An attack on the needham-schroeder public-key authentication protocol, Information processing letters, vol.56, issue.3, 1995.

M. Roger, M. Needham, and . Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.

K. Bhargavan, A. Delignat-lavaud, and A. Pironti, Verified contributive channel bindings for compound authentication, Network and Distributed System Security Symposium (NDSS '15), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01114248

T. Perrin, The Noise protocol framework, 2015.

S. Chokhani, W. Ford, R. Sabett, C. Merrill, and S. Wu, Internet X.509 Public Key Infrastructure: Certificate Policy and Certification Practices Framework, RFC, vol.3647, 2003.

C. Forum, Baseline requirements for the issuance and management of policy-trusted certificates, v.1.1.5, 2013.

G. Markham, R. Sleevi, R. Barnes, and K. Wilson,

A. Olivier-levillain, B. Ébalard, H. Morin, and . Debar, One year of SSL Internet measurement, Proceedings of the 28th Annual Computer Security Applications Conference, ACSAC '12, pp.11-20, 2012.

A. Delignat-lavaud, M. Abadi, A. Birrell, I. Mironov, T. Wobber et al., Web pki: Closing the gap between guidelines and practices, NDSS, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102254

. Google,

D. Basin, C. Cremers, T. Kim, A. Perrig, R. Sasse et al., Arpki: Attack resilient public-key infrastructure, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pp.382-393, 2014.

, Let's encrypt overview, 2016.

, Let's encrypt statistics, 2016.

R. Barnes, J. Hoffman-andrews, and J. Kasten, Automatic certificate management environment (acme, 2016.

V. Cheval and B. Blanchet, Proving more observational equivalences with ProVerif, International Conference on Principles of Security and Trust, pp.226-246, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863377

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, pp.1-135, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01423760

B. Blanchet, CryptoVerif: Computationally sound mechanized prover for cryptographic protocols, Dagstuhl seminar Formal Protocol Verification Applied, p.117, 2007.

S. Schneider, Using CSP for protocol analysis: the Needham-Schroeder public-key protocol, 1996.

G. Lowe, Lowe's fixed version of needham-schroder public key, 1995.

B. Blanchet, Security protocol verification: Symbolic and computational models, Principles of Security and Trust (POST), pp.3-29, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863388

B. Blanchet, A computationally sound mechanized prover for security protocols, IEEE Transactions on Dependable and Secure Computing, vol.5, issue.4, pp.193-207, 2008.

M. Abadi, B. Blanchet, and C. Fournet, The applied pi calculus: Mobile values, new names, and secure communication, J. ACM, vol.65, issue.1, p.41, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01423924

P. Syverson, C. Meadows, and I. Cervesato, Dolev-Yao is no better than machiavelli, 2000.

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The avispa tool for the automated validation of internet security protocols and applications, International conference on computer aided verification, pp.281-285, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000408

V. Cortier, S. Kremer, and B. Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems, Journal of Automated Reasoning, vol.46, issue.3-4, pp.225-259, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00379776

B. Blanchet, B. Smyth, and V. Cheval, Proverif 1.90: Automatic cryptographic protocol verifier, user manual and tutorial, 2014.

V. Shoup, Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive, 2004.

M. Bellare and P. Rogaway, The security of triple encryption and a framework for code-based game-playing proofs, Advances in Cryptology (Eurocrypt), pp.409-426, 2006.

M. Abdalla, P. Fouque, and D. Pointcheval, Password-based authenticated key exchange in the three-party setting, IEEE Proceedings Information Security, vol.153, pp.27-39, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00918401

B. Blanchet, Automatically verified mechanized proof of one-encryption key exchange, 25th IEEE Computer Security Foundations Symposium (CSF'12), pp.325-339, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00863386

Y. C. Thomas, S. S. Woo, and . Lam, A semantic model for authentication protocols, Proceedings IEEE Symposium on Research in Security and Privacy, pp.178-194, 1993.

B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, IEEE Computer Security Foundations Symposium (CSF), pp.97-111, 2007.

B. Dowling, M. Fischlin, F. Günther, and D. Stebila, A cryptographic analysis of the TLS 1.3 handshake protocol candidates, ACM Conference on Computer and Communications Security (CCS), pp.1197-1210, 2015.

H. Krawczyk and H. Wee, The OPTLS protocol and TLS 1.3, IEEE European Symposium on Security & Privacy (Euro S&P), 0978.
URL : https://hal.archives-ouvertes.fr/hal-01378195

X. Li, J. Xu, Z. Zhang, D. Feng, and H. Hu, Multiple handshakes security of TLS 1.3 candidates, IEEE Symposium on Security and Privacy (Oakland), pp.486-505, 2016.

C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. Van-der-merwe, A comprehensive symbolic analysis of TLS 1.3, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS '17, pp.1773-1788, 2017.

. Jason-a-donenfeld, WireGuard: next generation kernel network tunnel, 24th Annual Network and Distributed System Security Symposium, NDSS, 2017.

B. Lipp, A Mechanised Computational Analysis of the WireGuard Virtual Private Network Protocol

J. Donenfeld and K. Milner, Formal verification of the WireGuard protocol, 2017.

B. Dowling and K. G. Paterson, A cryptographic analysis of the WireGuard protocol, Cryptology ePrint Archive, 2018.

N. Kobeissi, K. Bhargavan, and B. Blanchet, Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach, IEEE European Symposium on Security and Privacy, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575923

K. Bhargavan, B. Blanchet, and N. Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, Security and Privacy (SP), 2017 IEEE Symposium on, pp.483-502, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01575920

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse, Verified interoperable implementations of security protocols, ACM Transactions on Programming Languages and Systems, vol.31, issue.1, 2008.

M. Avalle, A. Pironti, R. Sisto, and D. Pozza, The Java SPI framework for security protocol implementation, Availability, Reliability and Security, p.2011

, Sixth International Conference on, pp.746-751, 2011.

K. Bhargavan, A. Delignat-lavaud, and S. Maffeis, Language-based defenses against untrusted browser origins, USENIX Security Symposium, pp.653-670, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00863372

D. Cadé and B. Blanchet, Proved generation of implementations from computationally secure protocol specifications, Journal of Computer Security, vol.23, issue.3, pp.331-402, 2015.

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, ACM Symposium on Principles of Programming Languages (POPL), pp.445-456, 2010.

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignatlavaud et al., Dependent types and multi-monadic effects in F*, ACM Symposium on Principles of Programming Languages (POPL), pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

J. Karim-zinzindohoue, E. Bartzia, and K. Bhargavan, A verified extensible library of elliptic curves, IEEE Computer Security Foundations Symposium (CSF), pp.296-309, 2016.

R. Küsters, T. Truderung, and J. Graf, A framework for the cryptographic verification of Java-like programs, IEEE Computer Security Foundations Symposium (CSF), pp.198-212, 2012.

K. Bhargavan, A. D. Lavaud, C. Fournet, A. Pironti, and P. Y. Strub, Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS, IEEE Symposium on Security & Privacy (Oakland), pp.98-113, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102259

T. Frosch, C. Mainka, C. Bader, F. Bergsma, J. Schwenk et al., How Secure is TextSecure?, IEEE European Symposium on Security and Privacy (Euro S&P), 2016.

H. Krawczyk, HMQV: A High-performance Secure Diffie-Hellman Protocol, International Conference on Advances in Cryptology (CRYPTO), pp.546-566, 2005.

N. Durov, Telegram mtproto protocol, 2015.

O. Schirokauer, The number field sieve for integers of low weight. Mathematics of Computation, vol.79, pp.583-602, 2010.

D. Gillmor, Negotiated Finite Field Diffie-Hellman Ephemeral Parameters for Transport Layer Security (TLS)

A. Rad and J. Rizzo, A 2 64 attack on Telegram, and why a super villain doesn't need it to read your telegram chats, 2015.

J. Jakobsen and C. Orlandi, On the cca (in)security of mtproto, Cryptology ePrint Archive, 1177.

H. Krawczyk, Cryptographic extraction and key derivation: The HKDF scheme, Advances in Cryptology (CRYPTO), pp.631-648, 2010.

N. Kobeissi, SP code repository, 2017.

H. Krawczyk, SIGMA: The 'SIGn-and-MAc' approach to authenticated DiffieHellman and its use in the IKE-protocols, Advances in Cryptology-CRYPTO 2003, 23rd Annual International Cryptology Conference, vol.2729, pp.400-425, 2003.

T. Okamoto and D. Pointcheval, The gap-problems: a new class of problems for the security of cryptographic schemes, Practice and Theory in Public Key Cryptography (PKC), pp.104-118, 2001.

A. Fujioka and K. Suzuki, Designing efficient authenticated key exchange resilient to leakage of ephemeral secret keys, Topics in Cryptology (CT-RSA), pp.121-141, 2011.

J. Daniel and . Bernstein, Curve25519: New Diffie-Hellman speed records, Public Key Cryptography (PKC), pp.207-228, 2006.

S. Goldwasser, S. Micali, and R. Rivest, A digital signature scheme secure against adaptive chosen-message attacks, SIAM Journal of Computing, vol.17, issue.2, pp.281-308, 1988.

Y. Jean-sébastien-coron, C. Dodis, P. Malinaud, and . Puniya, Merkle-Damgård revisited: How to construct a hash function, Advances in Cryptology (CRYPTO), pp.430-448, 2005.

M. Bellare, New proofs for NMAC and HMAC: Security without collisionresistance, Advances in Cryptology (CRYPTO), pp.602-619, 2006.

A. David, J. Mcgrew, and . Viega, The security and performance of the Galois/Counter Mode (GCM) of operation, Progress in Cryptology-INDOCRYPT, vol.3348, pp.343-355, 2004.

P. Rogaway, Authenticated-encryption with associated-data, Ninth ACM Conference on Computer and Communications Security (CCS-9, pp.98-107, 2002.

Y. Dodis, T. Ristenpart, J. Steinberger, and S. Tessaro, To hash or not to hash again? (In)differentiability results for H2 and HMAC, Advances in Cryptology (Crypto), pp.348-366, 2012.

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

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

K. Cohn-gordon, C. Cremers, L. Garratt, J. Millican, and K. Milner, On ends-to-ends encryption: asynchronous group messaging with strong security guarantees, 2017.

K. Bhargavan, E. Rescorla, and R. Barnes, Tree-based KEM for group key management, 2018.

R. Hamilton, J. Iyengar, I. Swett, and A. Wilk, QUIC: A UDP-based multiplexed and secure transport, 2016.

C. Cremers, M. Horvat, S. Scott, and T. Van-der-merwe, Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication, IEEE Symposium on Security and Privacy (Oakland), pp.470-485, 2016.

M. Fischlin, F. Günther, B. Schmidt, and B. Warinschi, Key confirmation in key exchange: A formal treatment and implications for TLS 1.3, IEEE Symposium on Security and Privacy (Oakland), pp.452-469, 2016.

H. Krawczyk, A unilateral-to-mutual authentication compiler for key exchange (with applications to client authentication in TLS 1.3), ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1438-1450, 2016.

K. Bhargavan, C. Brzuska, C. Fournet, M. Green, M. Kohlweiss et al., Downgrade resilience in key-exchange protocols, IEEE Symposium on Security and Privacy (Oakland), pp.506-525, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01425962

T. Jager, J. Schwenk, and J. Somorovsky, On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 encryption, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1185-1196, 2015.

D. Bleichenbacher, Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS# 1, Annual International Cryptology Conference, vol.1462, pp.1-12, 1998.

C. Meyer, J. Somorovsky, E. Weiss, J. Schwenk, S. Schinzel et al., Revisiting SSL/TLS implementations: New Bleichenbacher side channels and attacks, 23rd USENIX Security Symposium, pp.733-748, 2014.

K. Bhargavan and G. Leurent, On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.456-467, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01404208

R. Martin, K. Albrecht, and . Paterson, Lucky microseconds: A timing attack on Amazon's S2N implementation of TLS, EUROCRYPT, pp.622-643, 2016.

M. Ray, A. Pironti, A. Langley, K. Bhargavan, and A. Delignat-lavaud, Transport Layer Security (TLS) session hash and extended master secret extension

M. Fischlin and F. Günther, Multi-stage key exchange and the case of Google's QUIC protocol, ACM SIGSAC Conference on Computer and Communications Security (CCS), pp.1193-1204, 2014.

R. Lychev, S. Jero, A. Boldyreva, and C. Nita-rotaru, How secure and quick is QUIC? provable security and performance analyses, IEEE Symposium on Security & Privacy (Oakland), pp.214-231, 2015.

N. Fips, , 2009.

M. Hamburg, Ed448-Goldilocks, a new elliptic curve. Cryptology ePrint Archive, vol.625, 2015.

D. Gillmor, Negotiated finite field Diffie-Hellman ephemeral parameters for Transport Layer Security (TLS), 2016.

A. Langley, M. Hamburg, and S. Turner, Elliptic curves for security, IRTF RFC, vol.7748, 2016.

E. Rescorla, PR#875: Additional Derive-Secret stage, 2017.

D. Ivan-bjerre, A design principle for hash functions, Advances in Cryptology-CRYPTO89, pp.416-427, 1989.

M. Bellare and C. Namprempre, Authenticated encryption: Relations among notions and analysis of the generic composition paradigm, Advances in Cryptology-ASIACRYPT'00, pp.531-545, 2000.

M. Bellare, J. Kilian, and P. Rogaway, The security of the cipher block chaining message authentication code, Journal of Computer and System Sciences, vol.61, issue.3, pp.362-399, 2000.

B. Blanchet, Composition theorems for CryptoVerif and application to TLS 1.3, 31st IEEE Computer Security Foundations Symposium (CSF'18), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01947959

B. Schmidt, S. Meier, C. Cremers, and D. Basin, Automated analysis of DiffieHellman protocols and advanced security properties, IEEE Computer Security Foundations Symposium (CSF), pp.78-94, 2012.

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A tutorial, Foundations of Security Analysis and Design VII (FOSAD), vol.8604, pp.146-166, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01114366

M. José-bacelar-almeida, G. Barbosa, F. Barthe, and . Dupressoir, Verifiable Side-Channel Security of Cryptographic Implementations: ConstantTime MEE-CBC, Fast Software Encryption (FSE), pp.163-184, 2016.

C. A. Comodo and . Ltd, Comodo Certification Practice Statement, Comodo CA Ltd, 2015.

. Digicert, DigiCert Certification Practices Statement, 2016.

G. Inc, GeoTrust Certification Practice Statement, 2016.

C. A. Globalsign, GlobalSign CA Certification Practice Statement, 2016.

, Certification Practice Statement, 2016.

, Symantec Trust Network (STN) Certification Practice Statement, Symantec Corporation, 2016.

C. A. Startcom and . Ltd, StartCom Certificate Policy and Practice Statements, StartCom CA Ltd, 2016.

. Llc-network and . Solutions, Network Solutions Certification Practice Statement, Network Solutions, LLC, 2016.

, Top 1,000,000 sites, Alexa Internet Inc, 2013.

R. and T. Truderung, Using ProVerif to analyze protocols with DiffieHellman exponentiation, IEEE Computer Security Foundations Symposium (CSF), pp.157-171, 2009.

G. Ateniese and S. Mangard, A new approach to dns security (dnssec), Proceedings of the 8th ACM conference on Computer and Communications Security, pp.86-95, 2001.

P. Hoffman and J. Schlyter, The dns-based authentication of named entities (dane) transport layer security (TLS) protocol: TLSA, 2012.

K. Bhargavan, A. Delignat-lavaud, and S. Maffeis, Defensive JavaScript-building and verifying secure web components, Foundations of Security Analysis and Design (FOSAD VII), pp.88-123, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01102144

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

P. A. Gardner, S. Maffeis, and G. Smith, JavaScript. SIGPLAN Not, vol.47, issue.1, pp.31-44, 2012.

, Joyent Inc. and the Linux Foundation. Node.js, 2016.

N. Wilcox, Z. Wilcox-o'hearn, D. Hopwood, and D. Bacon, Report of Security Audit of Cryptocat, 2014.

, Signal for the browser, 2015.

. Github, Electron framework, 2016.

A. Chaudhuri, Flow: Abstract interpretation of javascript for type checking and beyond, ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2016.

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis et al., A trusted mechanised javascript specification, ACM Symposium on the Principles of Programming Languages (POPL), pp.87-100, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00910135

D. Stefan, Espectro project description, 2016.

G. Bierman, M. Abadi, and M. Torgersen, Object-Oriented Programming, Lecture Notes on Computer Science, vol.8586, pp.257-281, 2014.

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

C. Bansal, K. Bhargavan, A. Delignat-lavaud, and S. Maffeis, Discovering concrete attacks on website authorization by formal analysis, Journal of Computer Security, vol.22, issue.4, pp.601-657, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00863385

G. Bai, J. Lei, G. Meng, P. Sai-sathyanarayan-venkatraman, J. Saxena et al., AUTHSCAN: automatic extraction of web authentication protocols from implementations, Network and Distributed System Security Symposium (NDSS), 2013.

D. Fett, R. Küsters, and G. Schmitz, An expressive model for the web infrastructure: Definition and application to the browser id sso system, Security and Privacy (SP), 2014 IEEE Symposium on, pp.673-688, 2014.

L. Lamport, Password authentication with insecure communication, Communications of the ACM, vol.24, issue.11, pp.770-772, 1981.

, WebAssembly Core Specification, 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, p.17, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01672706

P. Wang, K. Bhargavan, J. Zinzindohoué, A. Anand, C. Fournet et al.,