Example Secure System Specified Using the Terry-Wiseman Approach.

摘要

This report presents the specification of operations for a secure document handling system (SERCUS). The specification uses the Terry-Wiseman Security Policy Model and therefore acts as an example of the modelling approach. The specification uses the mathematical notation Z, and consequently also acts as an example of the use of Z in specifying secure systems. However, it must be noted that an appreciation of SERCUS, the model and modelling approach can usefully be gained even if the formal specifications are not read. The Terry-Wiseman Model and its interpretation are given as an Annex to this report. SERCUS is essentially an electronic registry system which controls the creation of, and access to, classified documents and mail messages. In the usual way, the users are assigned clearances which limit their ability to observe and modify the information in the system. In addition to their clearance, the users have a designated role to play. The possible roles are security officer and ordinary user, although there were also registry clerks in the original, longer, specification. Certain operations may only be performed by users with the appropriate role. For example, only security officers may create new legal users or review journalled information and, in the original specification, only registry clerks could create files or add documents to files. Although the model does allow systems to be specified where individuals can have more than one role, this is not required in the SERCUS application, and each user is assigned a single fixed role.