Title :
On the formal specification and verification of a multiparty session protocol
Author :
Cheng, Pau-Chen ; Gligor, Virgil D.
Author_Institution :
Dept. of Electr. Eng., Maryland Univ., College Park, MD, USA
Abstract :
The formal specification and verification of the multiparty session protocol discussed by the authors previously (1988) are presented. The notion of intruder processes is introduced to model intruder actions and countermeasures of the trusted computing bases. It is argued that multilevel network security can be achieved and verified formally independent of the specific transport-layer protocols even in the presence of intruders through the use of (1) a multilevel secure session protocol and (2) a key-distribution protocol which helps establish message confidentiality and integrity across an untrusted network. Both the formal security-policy model and the formal top-level specification (FTLS) of the multiparty session protocol are written in Ina Jo. The inference rules of the logic of authentication are incorporated in Ina Jo transforms to demonstrate the correctness of the key-distribution protocol. Two detailed examples of formal proofs are included
Keywords :
formal specification; protocols; security of data; Ina Jo; countermeasures; formal specification; formal top-level specification; integrity; intruder processes; key-distribution protocol; message confidentiality; multilevel network security; multiparty session protocol; verification; Access protocols; Authentication; Computer networks; Educational institutions; Formal specifications; Information security; Internet; Logic; Transport protocols; Workstations;
Conference_Titel :
Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-2060-9
DOI :
10.1109/RISP.1990.63853