Teaching formal methods in application domains: A case study in computer and network security

Abstract

In this paper, we report on our experience of teaching Formal Methods as part of an introductory computer and network security module. This module is part of an applied undergraduate computer science degree. As a consequence, we neither can rely on strong theoretical or mathematical foundations of the students, nor can we focus the whole term of applying Formal Methods in security. We address these challenges by integrating Formal Methods into a three weeks long section on security protocols. In these three weeks, we use a holistic approach for teaching the security objectives of security protocols, their analysis of actual implementations using a network sniffer, their formal verification using a model checker (and comparing it to an approaches based on interactive theorem proving).