Modelling security aspects of a Message Handling System in LOTOS

Describes the formal specification of the security aspects of a Message Handling System (MHS). The authors chose the international standard formal description technique LOTOS to describe this system. The actual system being modelled, called LOCATOR, is a secure mobile MHS, and was developed within the UK´s Alvey programme. They outline the MHS, the security services, and describe the modelling of these services in LOTOS