Formal Specification of a Secure Document Control System for SMITE

This document formally describes the requirements for a demonstration of a secure electronic registry control system Sercus to be implemented using the security attributes of the SMITE secure capability computer. The formal notation used in this specification is Z, which has been developed by the Programming Research Group at Oxford University. Sercus is intended to control the access to, and creation of, classified documents and files. In the paper world, all documents and files are centrally recorded and information as to who has had access to them is maintained. Sercus will enforce similar mechanisms. In addition to handling documents and files, users of Sercus will be able to send simple mail messages. When users are logged on to Sercus they are presented with a display that consists of a set of windows. All the window software will be completely trustworthy, but may be used to invoke untrusted software. While untrusted software is active in a window the classification of the data is prominently displayed. Sercus will monitor the movement of objects between these windows, and correctly maintain the classification levels Great Britain.