From BuildSecurityIn

https://buildsecurityin.us-cert.gov/daisy/bsi/articles/tools/modeling/698-BSI.html

Security policy model is a traditional name for the combination of the

• specification of the security policy—normally constraints (or properties)
• specification of the behavior of the system—normally a high-level specification of the design¹
• argument showing the consistency of the two—normally this means showing that a software system always stays within security constraints

This need to show consistency has been already been mentioned. In the early days (1960s, 70s, and 80s), this was often written about in terms of formal proofs. In the 1980s the concept of levels of assurance mapped to different kinds of evidence for this consistency. The legacy of this work is seen in today’s Common Criteria. However, borrowing in part from experience in safety, this concept has been generalized to one of an assurance case, which in part tries to address its own uncertainty and is intended to provide grounds for justified confidence and decision making by stakeholders.

One example of tool use is Praxis’s use of Z/Eves to formally state security policy and show the consistency of the system’s high-level design with it, using mathematical logic [Hall 2002].

Hmm...