Security modeling in the Ulysses environment

The authors give an overview of how the Ulysses system can be used for security modeling. The default theory of security permits the security analysis of complex designs by decomposing them into their parts. System specifications may be made by using a specialized graphical language interface and a textual inteface. In addition, there are a number of support tools which aid the modeler. One of these tools is the natural language component, which allows users to automatically generate short English descriptions of a graphical design. There is also a library component that facilitates the reuse of secure designs. In addition, there are mechanisms for adding security theories and other mathematical facts to augment the power of the theorem prover.