Specification and Verification of Security Policies

Computer security is the protection of the resources of a computer against events that can result in loss of availability, unauthorized access, or modification of data. The techniques devised to protect computers from these attacks are general purpose in nature and therefore cannot directly enforce security that has no universal definition. The high degree of assurance in security properties of systems used in security-critical areas such as military and commerce is usually achieved by verification. In this thesis we develop a framework for carrying out this verification in a formal and systematic manner.