A metamodel-based approach for analyzing security-design models

We have previously proposed an expressive UML-based language for constructing and transforming security-design models, which are models that combine design specifications for distributed systems with specifications of their security policies. Here we show how the same framework can be used to analyze these models: queries about properties of the security policy modeled are expressed as formulas in UML's Object Constraint Language and evaluated over the metamodel of the security-design language. We show how this can be done in a semantically precise and meaningful way and demonstrate, through examples, that this approach can be used to formalize and check non-trivial security properties of security-design models. The approach and examples presented have been implemented and checked in the SecureMOVA tool.