@Article{	  basin.ea:automated:2008,
  abstract	= {We have previously proposed SecureUML, an expressive
		  UML-based language for constructing security-design models,
		  which are models that combine design specifications for
		  distributed systems with specifications of their security
		  policies. Here we show how to automate the analysis of such
		  models in a semantically precise and meaningful way. In our
		  approach, models are formalized together with scenarios
		  that represent possible run-time instances. Queries about
		  properties of the security policy modeled are expressed as
		  formulas in UML's Ob ject Constraint Language. The policy
		  may include both declarative aspects, i.e., static
		  access-control information such as the assignment of users
		  and permissions to roles, and programmatic aspects, which
		  depend on dynamic information, namely the satisfaction of
		  authorization constraints in the given scenario. We show
		  how such properties can be evaluated, completely
		  automatically, in the context of the metamodel of the
		  security-design language. We demonstrate, through examples,
		  that this approach can be used to formalize and check
		  non-trivial security properties. The approach has been
		  implementedin the SecureMOVA tool and all of the examples
		  presented have been checked using this tool.},
  author	= {David Basin and Manuel Clavel and J\"urgen Doser and
		  Marina Egea},
  copyright	= {Elsevier},
  journal	= {Information and Software Technology},
  language	= {USenglish},
  note		= {to appear.},
  title		= {Automated Analysis of Security-Design Models},
  year		= 2008,
  user		= {doserj}
}