When it comes to the creation and evaluation of formal specifications in accordance with the applicable criteria (ITSEC, CC), experience shows that many questions remain open after reading the appropriate passages. The purpose of this guide is to help developers and evaluators gain a better understanding of this issue in the context of the criteria, particularly for the creation and evaluation of Formal Models of Security Policy (FMSP). In addition, it is intended to help identify the added value of Formal Models of Security Policy beyond the simple fulfilment of the criteria requirements.

For this purpose, the various requirements that are defined at different points in the criteria are first cited and differentiated in accordance with ITSEC and CC. A relation is established between these requirements and the characteristics of formal methods, as well as known and published Formal Models of Security Policy and experience from the development and evaluation of formal models. In particular, it becomes clear that the Bell-LaPadula and Biba models cited in the criteria documents each only define generic frameworks in which different security policies for access control are defined.

It is then apparent that the Formal Models of Security Policy are not isolated specifications, but must have a close and direct relation with other evaluation documents, e.g. with the functional specification (see CC, Description ADV_FSP).

As far as necessary to ensure understanding, the requirements for the Formal Models of Security Policy are not only defined in precise terms, but are also supported and explained with short extracts from an existing formal model for Integrated Circuit Cards with signature function in accordance with DIN V 66291-1.

All past experience shows that formal modelling of the security policy – as a Formal Model of Security Policy – can achieve increased trust in the security of the product operating in accordance with this security policy. One reason for this is that it has always been possible to discover vulnerabilities and errors on the basis of the informal security policies.

Until now, these results have always come at a price since the creation of Formal Models of Security Policy is seen as an isolated evaluation task at the end of product development and not part of the system development itself. If this were the case, many errors and security vulnerabilities would be prevented at an early stage and would not need to be fixed retrospectively at significant cost.

The previous guide has been incorporated into AIS document AIS 39.