In recent years, the Transport Layer Security (TLS) protocol has enjoyed rapid growth as a security protocol for the Internet of Things (IoT). In its newest iteration, TLS 1.3, the Internet Engineering Task Force (IETF) has standardized a zero round-trip time (0-RTT) session resumption sub-protocol, allowing clients to already transmit application data in their first message to the server, provided they have shared session resumption details in a previous handshake. Since it is common for IoT devices to transmit periodic messages to a server, this 0-RTT protocol can help in reducing bandwidth overhead. Unfortunately, the sub-protocol has been designed for the Web and is susceptible to replay attacks. In our previous work, we adapted the 0-RTT protocol to strengthen it against replay attacks, while also reducing bandwidth overhead, thus making it more suitable for IoT applications. However, we did not include a formal security analysis of the protocol. In this work, we address this and provide a formal security analysis using OFMC. Further, we have included more accurate estimates on its performance, as well as making minor adjustments to the protocol itself to reduce implementation ambiguity and improve resilience.
Keywords: formal verification; network; protocol; security.