. Flexclienthello and . Flexserverhello, receive(st,fch,nsc) in 9 let st,nsc,fcert = FlexCertificate.receive(st,Client,nsc) in 10 let st,nsc,fske = FlexServerKeyExchange.receiveDHE(st,nsc) 11 let st,fshd = FlexServerHelloDone.receive(st) in 12 let st,nsc,fcke = FlexClientKeyExchange.sendDHE(st,nsc) in 13 let st,_ = FlexCCS.send(st) in 14 15 (? Start encrypting ?) 16 let st = FlexState.installWriteKeys st nsc in 17 let st,ffC = FlexFinished.send(st,nsc,Client) in 18 let st,_,_ = FlexCCS.receive(st) in 19 20 (? Start decrypting ?) 21 let st = FlexState.installReadKeys st nsc in 22 let st,ffS= FlexFinished.receive(st,nsc,Server) in 23 24 (? Send and receive application data here ?) 25 let st = FlexAppData.send(st,utf8, Wustrow, S. Zanella-Béguelin, and P. Zimmermann. Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice, 2015.

B. Beurdouche, K. Bhargavan, A. Delignat-lavaud, C. Fournet, M. Kohlweiss et al., A messy state of the union, IEEE S&P (Oakland), 2015.
DOI : 10.1145/3023357

URL : https://hal.archives-ouvertes.fr/hal-01114250

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Pironti, and P. Strub, Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS, 2014 IEEE Symposium on Security and Privacy, p.2014
DOI : 10.1109/SP.2014.14

URL : https://hal.archives-ouvertes.fr/hal-01102259

K. Bhargavan, A. Delignat-lavaud, A. Pironti, A. Langley, and M. Ray, Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension, IETF Internet Draft, 2014.
DOI : 10.17487/RFC7627

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Strub, Implementing TLS with Verified Cryptographic Security, 2013 IEEE Symposium on Security and Privacy, p.2013
DOI : 10.1109/SP.2013.37

URL : https://hal.archives-ouvertes.fr/hal-00863373

K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub et al., Proving the TLS Handshake Secure (As It Is), CRYPTO, 2014.
DOI : 10.1007/978-3-662-44381-1_14

URL : https://hal.archives-ouvertes.fr/hal-01102229

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

D. K. Gillmor, Negotiated finite field Diffie-Hellman ephemeral parameters for TLS, IETF Internet Draft, 2015.

M. Kikuchi, How I discovered CCS Injection Vulnerability (CVE-2014-0224), 2014.

H. Krawczyk, K. G. Paterson, and H. Wee, On the Security of the TLS Protocol: A Systematic Analysis, CRYPTO, 2013.
DOI : 10.1007/978-3-642-40041-4_24

A. Langley, N. Modadugu, and B. Moeller, Transport layer security (TLS) false start, IETF Internet Draft, 2015.
DOI : 10.17487/RFC7918

E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1.3. Internet Draft, 2015.