Formal verification of tcp and t/tcp
Mark A. Smith, Nancy Ann Lynch · 1997
In this thesis we present a formal abstract specification for TCP/IP transport level protocols and formally verify that TCP satisfies this specification. We first verify a formal model of TCP where we assume it has unbounded counters. With bounded counters, TCP requires several timing mechanisms to function correctly. We also model TCP with these timing mechanisms and verify that it also satisfies our specification. We also present a formal description of an experimental protocol called T/TCP which is designed to provide the same service as TCP, but with optimizations to make it efficient for transactions. Even with unbounded counters this protocol does not provide the same service as TCP as it may deliver the same message twice. Even though the service provide by T/TCP is not exactly the same as TCP, its behavior may be acceptable for some applications. Therefore, we define a weaker specification that captures this behavior of T/TCP while maintaining the other correctness properties of our initial specification. We then verify that T/TCP satisfies this weaker specification. Our