Reusable Formal Models for Secure Software Architectures
Formal modeling techniques are often disregarded as their semantics are too distant from the mainstream practice of software architecture design, which is dominated by the use of component based modeling and patterns. This paper advocates the need for formal modeling techniques for humans, i.e., software architects who need to precisely ascertain the security properties of their design models. The authors contribute a technique that enables architects to more easily construct verified, secure architecture designs by assembling already verified security pattern models. Their approach is illustrated with a pattern language for accountability.