Modeling and validating the class security model using alloy

Abstract

Formalizing security models provide system designers and security engineers with evidence that they are constructing a consistent system that will meet the specifications as implemented. While it would be difficult to formalize every security model that has ever been developed or proposed, we present formal approving to ascertain secrecy properties of the Class Security Model. We use the Alloy language and analyzer for this formalism. We present the five model descriptions and show consistency proofs.