A Security Model and Verified Implementation for the IETF QUIC Transport Protocol