Formal specification and verification of TCP extended with the Window Scale Option

• We provide a μCRL specification of TCP extended with the Window Scale Option.
• Our specification of Data Transfer is branching bisimilar to a FIFO queue.
• Connection Teardown is verified against requirements expressed in μ-calculus.
• We recommend a rewording of RFC 793 to avoid deadlocking implementations.

We formally verify that TCP satisfies its requirements when extended with the Window Scale Option. With the aid of our μCRL specification and the LTSmin toolset, we verify that our specification of unidirectional TCP Data Transfer extended with the Window Scale Option does not deadlock, and that its external behaviour is branching bisimilar to a FIFO queue for a significantly large instance. Separately, we verify that a connection may only be closed if both entities accept the CLOSE call from the Application Layer. Finally, we recommend a rewording of the specification regarding how a zero window is probed, ensuring deadlocks do not arise as a result of misinterpretation.