Model Checking Security Pattern Compositions

Security patterns capture best practice on secure software design and development. They document typical solutions to security problems. To ensure security, large software system design may apply many security patterns to solve different problems. Although each security pattern describes a good design guideline, the compositions of these security patterns may not be consistent and encounter problems and flaws. In this paper, we present an approach to model checking the compositions of security patterns. In this way, the properties of the security patterns can be checked by a model checker when they are composed. Composition errors and problems can be discovered early in the design stage. We also use a case study to illustrate our approach and show the detection of several errors.