Formal Security Policy Model for a Common Criteria Evaluation

The common criteria (CC) is an international standard for evaluating secure, computer systems. The CC defines seven distinct evaluation assurance levels (EALs). The three highest EALs, the so-called high-assurance levels, require some degree of formalism, in development. The security policy model (SPM) is one of the documents required in formalism, in high-assurance levels. It is difficult to develop the formal SPM because the CC doesn´t specify how to make the document and industries have rarely published it. This paper shows a guideline for the development formal SPM and provides an example of formal SPM using Z, and proves the consistency and completeness of the SPM.