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 consistency and completeness of the SPM.