This paper describes the formal specification of the security aspects of a Message Handling System (MHS). We 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 U.K.'s Alvey programme. Here we outline the MHS, the security services, and describe the modelling of these services in LOTOS.
|Number of pages||5|
|Journal||IEE Conference Publication|
|Publication status||Published - 1989|