NDLI: A verified connection management protocol for the transport layer

Content Provider	ACM Digital Library
Author	Murphy, S. L. Shankar, A. U.
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.
Starting Page	110
Ending Page	125
Page Count	16
File Format	PDF
ISSN	01464833
DOI	10.1145/55483.55495
Journal	ACM SIGCOMM Computer Communication Review (CCRV)
Volume Number	17
Issue Number	5
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1993-07-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Computer Networks and Communications Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Automated verification of connection management of NBS class 4 transport protocol

Service specification and protocol construction for the transport layer

A verified connection management protocol for the transport layer

A distributed system security architecture:applying the transport layer security protocol

Modeling a transport layer protocol using first-order logic

Proposal for a connection-oriented internetwork protocol

A verified sliding window protocol with variable flow control

The transport layer

A multicast transport protocol

A verified connection management protocol for the transport layer

Similar Documents

Automated verification of connection management of NBS class 4 transport protocol

Service specification and protocol construction for the transport layer

A verified connection management protocol for the transport layer

A distributed system security architecture:applying the transport layer security protocol

Modeling a transport layer protocol using first-order logic

Proposal for a connection-oriented internetwork protocol

A verified sliding window protocol with variable flow control

The transport layer

A multicast transport protocol

A verified connection management protocol for the transport layer