Subject: Formalizing the TCP

From: [email-masked] (A. Udaya Shankar)
Date: Thu, 23 Mar 1995 10:44:45 -0500

Leo Marcus ([email-masked]) on March 21:
> Can anyone refer me to work on formal specification and analysis of
> the TCP? (Your reply via email would be appreciated.)
> 
> Many thanks,
> 
> Leo Marcus

TCP has two interacting functions:
   connection management (CM) and data transfer (DT).
We can distinguish two levels of faults:
  - X: loss/reordering/duplication channels
  - Y: host/channel failures and crashes that cause aborts

There are several (formal) treatments of DT in isolation assuming only X,
i.e. assuming zero initial sequence numbers.
CM is more intricate and there are far fewer thorough treatments of it,
e.g. including connection establishment and closing, choosing initial seq
num, balanced opeining, etc.  Plus TCP balanced opening has some flaws.

You may want to look at IEEE TCOM Dec 91, Transport layer: Service
specification and protocol construction.  It gives an alternative
simplpler protocol that offers TCP service, and references OF TCP
treatments.

udaya shankar