article

Free access

A verified connection management protocol for the transport layer

Authors:

A. U. ShankarAuthors Info & Claims

ACM SIGCOMM Computer Communication Review, Volume 17, Issue 5

Pages 110 - 125

https://doi.org/10.1145/55483.55495

Published: 01 August 1987 Publication History

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

[1]

J.P. Courtiat, J. M. Ayache, and B. Algayres, "Petri Nets are Good for Protocols", Proc. A CAd SIC COMM '84, June 1984.

Digital Library

[2]

K.M. Chandy and J. Misra. "An Example of Stepwise Refinement of Distributed Programs," A CM Trans. on Prog. Lang. and Syst., Vol. 8, No. 3, July 1986.

Digital Library

[3]

E.W. Dijkstra, A Discipline of Programming, Prentice Hall, 1975.

Digital Library

[4]

Transmission Control Protocol, DDN Protocol Handbook: DoD Military Standard Protocols, DDN Network Information Center, SRI, MILSTI)1778, Aug 1983.

[5]

International Organization for Standardization, Information Processing Systems- Open Systems Interconnection - Transport Protocol Specification, ISO DIS 8073, 1985.

[6]

W. Jurgensen and S. T. Vuong, "Formal Specification and Validation of ISO Transport Protocol Components, Using Petri Nets", Proc. A CM SIGCOMM '84, Jun 1984.

Digital Library

[7]

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.

[8]

J. F. Kurose and Y. Yemini, "The Specification and Verification of a Connection Establishment Protocol Using Temporal Logic," Protocol Specification, Testing and Verification II, ed. C. A. Sunshine, 1982.

Digital Library

[9]

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.

Digital Library

[10]

H.P. Lin, "Modeling a Transport Layer Protocol Using First-Order Logic", Proc. A CM SIGCOMM '8g, Aug 1980.

Digital Library

[11]

A. U. Shankar and S. S. Lam, "Timedependent distributed systems: proving safety, liveness and real-time properties," Tech. Rep. CS-TR-1586, Computer Science Dept., Univ. of Maryland, also TR-85-24, Computer Science Dept., Univ. of Texas, October 1985, revised October 1986, to appear in Distributed Computing.

Digital Library

[12]

A. U. Shankar, "A Verified Sliding Window Protocol with Variable Flow Control", Proc. A CM SIGCOMM '85, Aug 1986.

Digital Library

[13]

A. U. Shankar, "Verified data transfer protocols with variable flow control", CS-TR-1746, Dept. of Computer Science, University of Maryland, Mar 1987.

[14]

A. U. Shankar and S. S. Lam, "A Stepwise Refinement Heuristic for Protocol Construction'', CS-TR-1812, Dept. of Computer Science, University of Maryland, Mar 1987.

Digital Library

[15]

C.A. Sunshine and Y. K. Dalal, "Connection Management in Transport Protocols", Computer Networks, Vol.2(5), Dec 1978.

Cited By

Bishop SFairbairn MMehnert HNorrish MRidge TSewell PSmith MWansbrough K(2018)Engineering with LogicJournal of the ACM10.1145/324365066:1(1-77)Online publication date: 12-Dec-2018
https://dl.acm.org/doi/10.1145/3243650
Ridge TNorrish MSewell P(2008)A Rigorous Approach to NetworkingProceedings of the 15th international symposium on Formal Methods10.1007/978-3-540-68237-0_21(294-309)Online publication date: 26-May-2008
https://dl.acm.org/doi/10.1007/978-3-540-68237-0_21
Lam SShankar A(2005)Refinement and projection of relational specificationsStepwise Refinement of Distributed Systems Models, Formalisms, Correctness10.1007/3-540-52559-9_75(454-486)Online publication date: 4-Jun-2005
https://doi.org/10.1007/3-540-52559-9_75
Show More Cited By

Index Terms

A verified connection management protocol for the transport layer

Recommendations

A verified connection management protocol for the transport layer
SIGCOMM '87: Proceedings of the ACM workshop on Frontiers in computer communications technology

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 ...
Automated verification of connection management of NBS class 4 transport protocol

In a recent paper, the authors discussed verification of the connection management aspects of the NBS Class 4 transport protocol. An automated protocol development technique was used to verify a subset of the protocol with respect to the protocol ...
Automated verification of connection management of NBS class 4 transport protocol
SIGCOMM '84: Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium

In a recent paper, the authors discussed verification of the connection management aspects of the NBS Class 4 transport protocol. An automated protocol development technique was used to verify a subset of the protocol with respect to the protocol ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGCOMM Computer Communication Review

ACM SIGCOMM Computer Communication Review Volume 17, Issue 5

Oct./Nov. 1987

397 pages

ISSN:0146-4833

DOI:10.1145/55483

Editor:
J. J. Garcia-Luna-Aceves
SRI International, Menlo Park, CA

Issue’s Table of Contents

SIGCOMM '87: Proceedings of the ACM workshop on Frontiers in computer communications technology
August 1987
409 pages
ISBN:0897912454
DOI:10.1145/55482
Editor:
J. J. Garcia-Luna-Aceves
SRI International, Menlo Park, CA

Copyright © 1987 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1987

Published in SIGCOMM-CCR Volume 17, Issue 5

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
559
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)20

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bishop SFairbairn MMehnert HNorrish MRidge TSewell PSmith MWansbrough K(2018)Engineering with LogicJournal of the ACM10.1145/324365066:1(1-77)Online publication date: 12-Dec-2018
https://dl.acm.org/doi/10.1145/3243650
Ridge TNorrish MSewell P(2008)A Rigorous Approach to NetworkingProceedings of the 15th international symposium on Formal Methods10.1007/978-3-540-68237-0_21(294-309)Online publication date: 26-May-2008
https://dl.acm.org/doi/10.1007/978-3-540-68237-0_21
Lam SShankar A(2005)Refinement and projection of relational specificationsStepwise Refinement of Distributed Systems Models, Formalisms, Correctness10.1007/3-540-52559-9_75(454-486)Online publication date: 4-Jun-2005
https://doi.org/10.1007/3-540-52559-9_75
Murphy SShankar A(1991)Connection management for the transport layer: service specification and protocol verificationIEEE Transactions on Communications10.1109/26.12016339:12(1762-1775)Online publication date: Jan-1991
https://doi.org/10.1109/26.120163
Lam SShankar A(1990)A Relational Notation for State Transition SystemsIEEE Transactions on Software Engineering10.1109/32.5610116:7(755-775)Online publication date: 1-Jul-1990
https://dl.acm.org/doi/10.1109/32.56101
Bishop SFairbairn MMehnert HNorrish MRidge TSewell PSmith MWansbrough K(2018)Engineering with LogicJournal of the ACM10.1145/324365066:1(1-77)Online publication date: 12-Dec-2018
https://dl.acm.org/doi/10.1145/3243650
Bishop SFairbairn MNorrish MSewell PSmith MWansbrough K(2005)Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and socketsACM SIGCOMM Computer Communication Review10.1145/1090191.108012335:4(265-276)Online publication date: 22-Aug-2005
https://dl.acm.org/doi/10.1145/1090191.1080123
Bishop SFairbairn MNorrish MSewell PSmith MWansbrough KGuerin RGovindan RMinshall G(2005)Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and socketsProceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications10.1145/1080091.1080123(265-276)Online publication date: 22-Aug-2005
https://dl.acm.org/doi/10.1145/1080091.1080123
Murphy SShankar A(1988)Service specification and protocol construction for the transport layerACM SIGCOMM Computer Communication Review10.1145/52325.5233418:4(88-97)Online publication date: 1-Aug-1988
https://dl.acm.org/doi/10.1145/52325.52334
Murphy SShankar A(1988)Service specification and protocol construction for the transport layerSymposium proceedings on Communications architectures and protocols10.1145/52324.52334(88-97)Online publication date: 1-Aug-1988
https://dl.acm.org/doi/10.1145/52324.52334

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents