On the formal specification and verification of a multiparty session protocol

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