Automatic Verification of
Transmission Control Protocol Using NuSMV
Jingjing Lu Yuxiang Zhu
March 27, 2000
In this report we construct a model of the TCP state machine and verify it using NuSMV.
Also we check our model of TCP for some denial-of-services attacks. Finally we address
the issue whether NuSMV is a proper model checker for complex systems like TCP.
In this section, we explain the ideas of TCP and give a brief introduction to the model
checker NuSMV; finally, we introduce the basic concepts of TCP attacks.
1.1 A Brief Introduction to TCP
TCP (Transmission Control Protocol) is a very important and well-known network-level
protocol. Although TCP is always mentioned as part of the TCP/IP Internet protocol
suite, it is an independent, general-purpose protocol that can be adapted for use with other
delivery systems. TCP has been so popular that one of the International Organization for
Standardization’s open systems protocols, TP-4, has been derived from it.
TCP is a very complex, high level protocol. It specifies the format of the data and
acknowledgments that two computers exchange to achieve a reliable transfer, as well as
the procedures the computers use to ensure that the data arrives correctly. This reliable
stream delivery service guarantees to deliver a stream of data sent from one machine to
another without duplication or data loss. TCP ensures the reliability using positive
acknowledgment with retransmission. This technique requires a recipient to communicate
with the source, sending back an acknowledgment (ACK) message as it receives data.
The sender keeps a record of each packet it sends and waits for an acknowledgment
before sending the next packet. The sender also starts a timer when it sends a packet and
retransmits this packet if the timer expires before an acknowledgment arrives.
Figure 1 shows how the simplest positive acknowledgement protocol transfers data.
Figure 1 A protocol using positive acknowledgment with retransmission