Threat scenarios as a means to formally develop secure systems

Abstract

We introduce a new method for the formal development of secure systems that closely corresponds to the way secure systems are developed in practice. It is based on Focus, a general-purpose approach to the design and verification of distributed, interactive systems. Our method utilizes threat scenarios which are the result of threat identification and risk analysis and model those attacks that are of importance to the system's security. We describe the adversary's behaviour and influence on interaction. Given a suitable system specification, threat scenarios can be derived systematically from that specification. Security is defined as a particular relation on threat scenarios and systems. We show the usefulness of our approach by developing an authentic server component, thereby analysing two simple authentication protocols.