Security mutants for property-based testing

The last decade has witnessed impressive progress in terms of dedicated approaches to formally analyzing security properties of models. However, related approaches to generating tests generally rely on purely syntactic test selection criteria. In this paper, we consider models of protocols and describe an approach to generate tests from security properties. Security-specific mutation operators are defined and used to introduce potential security-specific leaks into the model. Then, if the leak is confirmed by a model analyzer, a test case for the security property is generated. We present examples for security-relevant mutants at the model level and show how they correspond to security-flawed implementations, thus providing evidence that model-level mutants are indeed useful for doing security testing.