Enabling Security Testing from Specification to Code

摘要

In this paper, we present the idea of creating an intermediary model which is capable of being derived directly from the high-level, abstract model, but more closely resembles the actual implementation. The focus of our work is on the security properties of protocols. Not only do we show how an intermediary model can be constructed, but also how it can be used to automatically generate test sequences based on the security goals of the protocol being tested. Our aim is to show that by using this approach, we can derive test sequences suitable for a tester to use on a working implementation of the protocol.