Formal methods: transition from CC v3.1 to CC:2022

This state-of-the-art document provides requirements on the application of ADV_SPM.1 in the transition from Common Criteria version 3.1 (CC3.1) to Common Criteria version 2022 (CC:2022).

In CC:2022, the evaluation of formal models according to ADV_SPM.1 requires the formal modelling of the entire TOE security functionality (TSF). In the case of a single-assurance Security Target (ST), this means a formal model of the entire TSF as defined in the ST. For a ST that is conformant to a multi-assurance PP-Configuration, the parts of the TOE security functionality (sub-TSFs) to which ADV_SPM.1 applies must be entirely modelled. Experience has shown that a formal and comprehensive model (as in the case of a single-assurance ST) can be challenging for complex products due to the high efforts associated with development, proofing, evaluation and assessment. Regarding the second case, suitable multi-assurance PP-Configurations are not yet available.

To ensure a smooth transition from CC3.1 to CC:2022, this document establishes a practical interpretation allowing the optional formal modelling of parts of the security functionality of a TOE that are meaningful for assurance purposes.