Transmission Control Protocol

TCP/IP is the most widely used protocol on the Internet for transmitting data. But how does it work in detail? This talk will explain the TCP protocol, from handshake over established to teardown in detail - and elaborate a bit on protocol adjustments over time and congestion control. I will briefly explain how computers talk to each other via the Internet Protocol (IP), and explain the transport protocols UDP and TCP, and their interaction with ICMP (for error and control messages). UDP is the user datagram protocol, an unreliable packet-oriented protocol. TCP provides a reliable stream of data, and includes connection establishment, feature negotiation, window management, and teardown. Over the last years at University of Cambridge I contributed to a formal model of TCP/IP and the Unix sockets API, developed in HOL4. We validated our HOL4 model with the FreeBSD-12 stack using Dtrace (packets, system calls, internal TCP state). In this research, we formalised a more exact TCP state machine than in initial RFCs or common literature (Stevens).