Security Policy Modeling using Z notation for Common Criteria version 3.1

The common criteria for information technology security evaluation (CC) is an international standard for evaluating secure computer systems. To obtain high evaluation assurance level, CC requires formalism in the development class. In the security policy modeling of CC v3.1, the use of formal methods is mandatory. This paper gives a guideline for developing formal security policy model with Z notation in CC v3.1. We compare CC v3.1 to CC v2.3 with respect to security policy model. We explain a structure of formal security policy model written in Z, and provide a formal security policy model of a smart card operating system as an example.