A verified connection management protocol for the transport layer

ABSTRACT

We specify and verify a connection management protocol for use between entities connected by channels that can lose, reorder, and duplicate messages. The protocol is symmetric. Each entity is in one of the following states: closed, listen, open, active opening, passive opening, or closing. The first three are stable states to be exited only by user request, while the last three are transient states. Each entity maintains a local incarnation number at all times, and a remote incarnation number only when opening, open, and closing. Our protocol employs the 3-way handshake used in TCP and ISO Transport Protocol (Class 4). We verify the safety property that when an entity is open, its remote incarnation number matches the remote entity's local incarnation number. This ensures that data messages from past connection instances are not delivered to the user. We verify the following progress properties: an actively opening entity will eventually establish a connection, provided that the remote entity is willing to communicate or is itself actively opening; the states of active opening, passive opening, and closing are transient; if the entities remain closed, the channels will eventually become empty, assuming messages have a maximum lifetime. This protocol specification can be immediately combined with the data transfer protocol specifications presented in [SHAN1, SHAN2, SHAN3] to provide a transport layer protocol with the functions of connection management and two-way data transfer. The verifications too can be immediately combined to provide a hierarchical verification of the multi-function protocol. The specifications and verifications can be combined because the connection management and data transfer protocols are images of the multi-function protocol. This illustrates the power of protocol projections in constructing multi-function protocols.

REFERENCES

• COUR: J. P. Courtiat , J. M. Ayache , B. Algayres, Petri nets are good for protocols, Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium, p.66-74, June 06-08, 1984, Montréal, Quebec, Canada, United States
• CHAN: Mani Chandy , Jayadev Misra, An example of stepwise refinement of distributed programs: quiescence detection, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.326-343, July 1986 [doi>10.1145/5956.5958]
• DIJK: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• DoD: Transmission Control Protocol, DDN Protocol Handbook: DoD Military Standard Protocols, DDN Network Information Center, SRI, MILSTI)1778, Aug 1983.
• ISO: International Organization for Standardization, Information Processing Systems- Open Systems Interconnection - Transport Protocol Specification, ISO DIS 8073, 1985.
• JUR1: Wolfgang JÜrgensen , Son T. Vuong, Formal specification and validation of ISO transport protocol components, using petri nets, Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium, p.75-82, June 06-08, 1984, Montréal, Quebec, Canada, United States
• JUR2: W. Jurgensen and S. T. Vuong, "CSP and CSP Nets: A Dual Model for Protocol Specification and Verification", Protocol Specification, Testing, and Verification IV, ed. Y. Yemini, R. Strom, and S. Yemini, 1984.
• KUR: James F. Kurose, The Specification and Verification of a Connection Establishment Protocol Using Temporal Logic, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.43-62, May 17-20, 1982
• LAM: S.S. Lam and A. U. Shankar, "Protocol verification via projections," IEEE Trans. on Soft. Eng., Vol. SE-10, No. 4, July 1984, pp. 325-342.
• LIN: H P Lin, Modeling a transport layer protocol using first-order logic, Proceedings of the ACM SIGCOMM conference on Communications architectures & protocols, p.92-100, August 05-07, 1986, Stowe, Vermont, United States
• SHAN0: A. U Shankar , Simon S. Lam, Time-Dependent Distributed Systems: Proving Safety, Liveness and Real-TimeProperties, University of Texas at Austin, Austin, TX, 1985
• SHAN1: A U Shankar, A verified sliding window protocol with variable flow control, Proceedings of the ACM SIGCOMM conference on Communications architectures & protocols, p.84-91, August 05-07, 1986, Stowe, Vermont, United States
• SHAN2: A. U. Shankar, "Verified data transfer protocols with variable flow control", CS-TR-1746, Dept. of Computer Science, University of Maryland, Mar 1987.
• SHAN3: A. Udaya Shankar , Simon S. Lam, A stepwise refinement heuristic for protocol construction, University of Maryland at College Park, College Park, MD, 1990
• SUN: C.A. Sunshine and Y. K. Dalal, "Connection Management in Transport Protocols", Computer Networks, Vol.2(5), Dec 1978.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  K. Computing Milieux
  K.1 THE COMPUTER INDUSTRY
      Subjects: Standards

General Terms:
Standardization, Verification