Database of Case Studies Achieved Using CADP

Specification and Verification of TCP extended with the Window Scale Option

Organisation: VU University Amsterdam (THE NETHERLANDS)

Method: μCRL

Tools used: LTSmin
CADP (Construction and Analysis of Distributed Processes)

Domain: Networks.

Period: 2016

Size: 3,296,792 states and 11,010,169 transitions.

Description: The Transmission Control Protocol (TCP) plays an important role in the Internet, providing reliable transport of messages through a possibly faulty medium to many of its applications. TCP enables two parties to reliably communicate over a faulty network. Its responsibilities can roughly be divided into two categories: Connection management sets up the connections, manages the connection states and ensures that connections are closed in a safe manner; Data transmission involves the transfer of segments from the sender to the receiver.

TCP uses the Sliding Window Protocol for its data transfer. Both sender and receiver maintain a window of n sequence numbers, ranging from 0 to n-1, from which they can send or where they can receive data items. The sender may send as many bytes as the size of its window before it has to wait for an acknowledgement from the receiver. Once the receiver sends an acknowledgement for m bytes, its window slides forward m sequence numbers. Likewise, the sender's window slides m sequence numbers if this acknowledgement arrives.

The performance of TCP is directly influenced by the size of the send window: the larger it is, the more data a sender can send without having to wait for an acknowledgement. If the medium can hold more than the window size, unnecessary delay will be introduced into the communication due to the restriction on the window size. To resolve this issue, RFC 1323 proposes the Window Scale Option (WSO). If implemented, the send and receive windows are maintained as 32-bit numbers. Whenever an entity receives an acknowledgement, it applies the scale factor to the window size the before it updates its send window. Likewise, whenever an entity sends an acknowledgement it sets the window field of the outgoing segment to the size of its receive window.

The goal of this case-study was to verify that the TCP continues to function correctly in presence of the WSO. To this purpose, TCP was formally specified in μCRL, including the Data Transfer and Connection Teardown phases as specified in RFCs 793 and 1122, extended to include the WSO, as specified in RFC1 323. The LTS model was generated using the LTSmin toolset, and two properties regarding the successful completion of TCP connections were specified in regular alternation-free μ-calculus and checked on the LTS using the EVALUATOR model checker of CADP.

Conclusions: The TCP protocol is complex and its specification consists of many documents that mainly describe the proposed functioning of the protocol in natural language. A formal specification provides a more precise reference of the intended function of a protocol, and also a useful basis for formal verification.

Publications: [Lockefeer-Williams-Fokkink-16] L. Lockefeer, D. M. Williams, and W. Fokkink. "Formal Specification and Verification of TCP Extended with the Window Scale Option". Science of Computer Programming 118:3-23, March 2016.
Available on-line from https://doi.org/10.1016/j.scico.2015.08.005
Contact:
Wan Fokkink
Vrije Universiteit Amsterdam
Faculty of Sciences
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081
1081 HV Amsterdam
THE NETHERLANDS
Room: T429
Tel: +31 20 598 7735
Email: [email protected]
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page