A mathematically precise statement of a security policy. To be adequately precise, such a model must represent the initial state of a system, the way in which the system progresses from one state to another, and a definition of a “secure” state of the system. To be acceptable as a basis for a TCB, the model must be supported by, a formal proof that if the initial state of the system satisfies the definition of a “secure" state and if all assumptions required by the model hold, then all future states of the system will be secure. Some formal modeling techniques include: state transition models, denotational semantics models, and algebraic specification models. See Bell-La Padula model and security policy model.