In March 2000, 1 million litres of raw sewage was released into the water system of Maroochy Shire on Queensland’s sunshine coast. This environmental disaster was caused by a disgruntled ex-contractor using a radio transmitter to illicitly access the electronically controlled pumps in the control system. In 2007 CNN screened video footage of an experimental attack against a electrical generator. The attack caused the generator to shake and smoke, visually showing the damage caused by cyber attack. These attacks highlight the importance of securing the control systems which our critical infrastructures depend on. This thesis addresses securing control systems, focusing on securing the communications for supervisory control and data acquisition (SCADA) systems. We review the architectures of SCADA systems and produce a list of the system constraints that relate to securing these systems. With these constraints in mind, we survey both the existing work in information and SCADA security, observing the need to investigate further the problem of secure communications for SCADA systems. We then present risk modelling techniques, and model the risk in a simple SCADA system, using the ISM, a software tool for modelling information security risk. In modelling the risk, we verify the hypothesis that securing the communications channel is an essential part of an effective security strategy for SCADA systems. After looking at risk modelling, and establishing the value of securing communications, we move on to key management for SCADA systems. Appropriate key management techniques are a crucial part of secure communications, and form an important part of the contributions made in this work. We present a key management protocol that has been designed to run under the constraints specific to SCADA systems. A reductionist security proof is developed for a simplified version of the protocol, showing it is secure in the Bellare Rogaway model.

We study the problem of secure key establishment. We critically examine the security models of Bellare and Rogaway (1993) and Canetti and Krawczyk (2001) in the computational complexity approach, as these models are central in the understanding of the provable security paradigm. We show that the partnership definition used in the three-party key distribution (3PKD) protocol of Bellare and Rogaway (1995) is flawed, which invalidates the proof for the 3PKD protocol. We present an improved protocol with a new proof of security. We identify several variants of the key sharing requirement (i.e., two entities who have completed matching sessions, partners, are required to accept the same session key). We then present a brief discussion about the key sharing requirement. We identify several variants of the Bellare and Rogaway (1993) model. We present a comparative study of the relative strengths of security notions between the several variants of the Bellare-Rogaway model and the Canetti-Krawczyk model. In our comparative study, we reveal a drawback in the Bellare, Pointcheval, and Rogaway (2000) model with the protocol of Abdalla and Pointcheval (2005) as a case study. We prove a revised protocol of Boyd (1996) secure in the Bellare-Rogaway model. We then extend the model in order to allow more realistic adversary capabilities by incorporating the notion of resetting the long-term compromised key of some entity. This allows us to detect a known weakness of the protocol that cannot be captured in the original model. We also present an alternative protocol that is efficient in both messages and rounds. We prove the protocol secure in the extended model. We point out previously unknown flaws in several published protocols and a message authenticator of Bellare, Canetti, and Krawczyk (1998) by refuting claimed proofs of security. We also point out corresponding flaws in their existing proofs. We propose fixes to these protocols and their proofs. In some cases, we present new protocols with full proofs of security. We examine the role of session key construction in key establishment protocols, and demonstrate that a small change to the way that session keys are constructed can have significant benefits. Protocols that were proven secure in a restricted Bellare-Rogaway model can then be proven secure in the full model. We present a brief discussion on ways to construct session keys in key establishment protocols and also prove the protocol of Chen and Kudla (2003) secure in a less restrictive Bellare-Rogaway model. To complement the computational complexity approach, we provide a formal specification and machine analysis of the Bellare-Pointcheval-Rogaway model using an automated model checker, Simple Homomorphism Verification Tool (SHVT). We demonstrate that structural flaws in protocols can be revealed using our framework. We reveal previously unknown flaws in the unpublished preproceedings version of the protocol due to Jakobsson and Pointcheval (2001) and several published protocols with only heuristic security arguments. We conclude this thesis with a listing of some open problems that were encountered in the study.