A Security Model and Verified Implementation for the IETF QUIC Transport Protocol Antoine Delignat-Lavaud