Improving the security of industrial networks by means of formal verification

Computer networks are exposed to serious security threats that can even have catastrophic consequences from both the points of view of economy and safety if such networks control critical infrastructures, such as for example industrial plants. Security must then be considered as a fundamental issue starting from the earlier phases of the design of a system, and suitable techniques and tools should be adopted to satisfy the security-related requirements. The focus of this paper is on how formal methods can help in analysing the standard cryptographic protocols used to implement security-critical services such as authentication and secret keys distribution in critical environments. The analysis of the 802.11 shared key authentication protocol by S³A, a fully automatic software tool that is based on a formal approach, is illustrated as a case study, which also highlights the peculiarities of analysing protocols based on wireless channels.