Modelling security aspects of a Message Handling System in LOTOS
Stacy Black, Claudio Calvelli, Vijay Varadharajan · International Conference on Software Engineering · 1989
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. >