PROTOCOL VERIFICATION FOR A TRUSTED NETWORK ARCHITECTURE

Authors
  1. Soper, R.E.
  2. Lee, E.S.
  3. Boulton, P.I.P.
  4. Stumm, M.
  5. Thomson, B.
Corporate Authors
Toronto Univ, Toronto ONT (CAN) Computer Systems Research Inst;Chief of Research and Development, Ottawa ONT (CAN) Director of Research and Development Communications and Space
Abstract
The document is a report on the application of formal verification techniques to the authentication protocol discussed in the final Trusted Network Architecture (TNA) report. Authentication is a central issue in the design of secure computer networks, and proving that it can be reliably achieved is an important step. The TNA relies on the Trusted Network Controller (TNC) to arbitrate all communication between hosts. Establishment of a virtual circuit is accomplished through a negotiation protocol executed by the TNC and the two hosts that intend to communicate. One such protocol, the Basic Negotiation Protocol, is discussed in detail in the TNA report. The correctness of this protocol is sufficiently important to the secure operation of the TNA that work has been undertaken to prove that it operates properly. The report is a description of the tools used to achieve this proof, and the results that have been gathered.
Date of publication
15 Dec 1988
Number of Pages
24
DSTKIM No
89-02076
CANDIS No
59987
Format(s):
Hardcopy;Originator's fiche received by DSIS

Permanent link

Document 1 of 1

Date modified: