Browse Prior Art Database

Formal Specification and Verification of a Connection-Establishment Protocol

IP.com Disclosure Number: IPCOM000128663D
Original Publication Date: 1981-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 26 page(s) / 73K

Publishing Venue

Software Patent Institute

Related People

Daniel Schwabe: AUTHOR [+3]

Abstract

. I 1.1 Connection-Establishment Protocols. 1.2 Overview of SPEX . . . . . . . . . . . . . . . . 1.3 Overview of Algebraic Specification of Data Types and of Affirm . . . . , . . . . . . . . . .............. 6 1.4 Relation to Other Work 9 2. SPECIFICATION OF THE THREE-WAY HANDSHAKE IN SPEX 3. VERIFICATION " 3.1 Introduction . . . . . . .

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 5% of the total text.

Page 1 of 26

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Formal Specification and Verification of a Connection-Establishment Protocol

Daniel Schwabe

ISIlRR-81-91 April 19$ INFORMATION SCIENCES INSTITUTE

* 4G7< Admiralty WaylMarinadel ReylCalifoswia 90291 UNIVERSITY of SOUTHERNCALIFORNIA l2l.;) g22_)SlI This research is supported by the Defense Advanced Research Projects Agency under Contract No. DAHC15 72 C 0308. Views and conclusions contained in this report are the author's and should not 'be interpreted as representing the official opinion or policy of DARPA, the U.S. Government, or any person or agency connected with them.

This document is approved for public release and sale; distribution is unlimited.

CONTENTS

ACKNOWLEDGMENTS . . . . . . . . . . . .. . . . . . . . . . . .. .. . . . . .. .. . . . . . . . iv

1.INTRODUCTION . I

1.1 Connection-Establishment Protocols.

1.2 Overview of SPEX . . . . . . . . . . . . . . . .

1.3 Overview of Algebraic Specification of Data Types and of Affirm . . . . , . . . . . . . . . ..............
6 1.4 Relation to Other Work 9 2. SPECIFICATION OF THE THREE-WAY HANDSHAKE IN SPEX 3. VERIFICATION "

3.1 Introduction . . . . . . .

3.2 Functional Correctness

3.3 Liveness.

4. CONCLUSIONS ........................... II 23 I. SPEXIFICATION OF THE THREE-WAY
HANDSHAKE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

II. AXIOMS GENERATED FROM THE SPEXIFICATION OF THE THREE-WAY HANDSHAKE
11.1 Three-Way Handshake ..........................................

11.2 Auxiliary Data Type Definitions. REFERENCES. ...................... 33

40 FIGURES Figure 1-1: Three-way handshake state-transition diagram . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . , . . . . . . . . . Figure 1-2: Signature of type QueueOflnteger . . . . . . . . . . . . . . . ,. , .
. , . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Figure 1-3: Some axioms far type QueueOflnteger , . . .
. . . . . . . . . . . . .`. . , . . , . , . . . . . . . . . . . . . . . . . . . . . Figure 3-1: Prooftreefar the functional

University of Southern California Page 1 Dec 31, 1981

Page 2 of 26

Formal Specification and Verification of a Connection-Establishment Protocol

correctness of the three-way handshake Figure 3-1: Proof tree (continued) . . . . . . . . . . . . . . . . .
. .

4 7 8 .................... 17 ......................................... 18 Figure 3-2: Theorems and definitions used
in the proof of thethree-way handshake . . . . . . . . . . . . . . . . . . . 19 Figure 3-3: Example of a
liveness error in the three-way handshake . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

ACKNOWLEDGMENTS

I wish to thank Carl Sunshine for his constructive criticism of the work presented in this report and careful review of the report itself; Jon Postel for taking the time to answer all those naive questions about TCP; the members of the Program Verification group at ISI, in particular Susan Gerhart,...