Command center security-proving software correct

Many command center operations require the ability to process and safeguard information derived from multiple sources, often over wide geographical areas and from different security environments. Thus in the development or upgrade of a command center one may need to address a number of security issues such as confidentiality, authentication, availability, and integrity of data. This paper discusses how formal methods can be used to prove correctness of two command center security services: network security in relation to authentication protocols; and the automated transfer of data between separate systems operating at different security levels (i.e., guard systems). The proof process is supported by a collection of tools which constitute the Romulus Security Modeling Environment. To specify and analyze authentication protocols we use a formalism known as belief logic. We show how this can be used to specify and address aspects of confidentiality, authentication, integrity, and key distribution in the Kerberos Authentication protocol. We also discuss how belief logic can be used in conjunction with a process model formalism to reason about security in guards