ADV_RCR.3 Formal correspondence demonstration
Application notes
The developer must either demonstrate or prove correspondence, as described in the requirements below, commensurate with the level of rigour of presentation style. For example, correspondence must be proven when corresponding representations are formally specified.
Dependencies:
No dependencies.
Developer action elements:
ADV_RCR.3.1D The developer shall provide an analysis of correspondence between all adjacent pairs of TSF representations that are provided.
ADV_RCR.3.2D For those corresponding portions of representations that are formally specified, the developer shall prove that correspondence.
Content and presentation of evidence elements:
ADV_RCR.3.1C For each adjacent pair of provided TSF representations, the analysis shall prove or demonstrate that all relevant security functionality of the more abstract TSF representation is correctly and completely refined in the less abstract TSF representation.
ADV_RCR.3.2C For each adjacent pair of provided TSF representations, where portions of one representation are semiformally specified and the other at least semiformally specified, the demonstration of correspondence between those portions of the representations shall be semiformal.
ADV_RCR.3.3C For each adjacent pair of provided TSF representations, where portions of both representations are formally specified, the proof of correspondence between those portions of the representations shall be formal.
Evaluator action elements:
ADV_RCR.3.1E The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence.
ADV_RCR.3.2E The evaluator shall determine the accuracy of the proofs of correspondence by selectively verifying the formal analysis.