Teaching Formal Methods in Application Domains: A Case Study in Computer and Network Security

By Achim D. Brucker and Diego Marmsoler.

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).

Keywords:
Formal Methods and Security, Protocol Verification, OFMC, Research-led Teaching

Please cite this work as follows:
A. D. Brucker and D. Marmsoler, “Teaching formal methods in application domains: A case study in computer and network security,” in Formal methods teaching (FMTea 2024), L. Ribeiro and E. Sekerinski, Eds. Heidelberg: Springer-Verlag, 2024. doi: 10.1007/978-3-031-71379-8_8. Author copy: http://logicalhacking.com/publications/brucker.ea-fm-teaching-2024/

BibTeX
@InCollection{ brucker.ea:fm-teaching:2024,
  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).},
  keywords  = {Formal Methods and Security, Protocol Verification, OFMC,
               Research-led Teaching},
  location  = {Milan, Italy},
  author    = {Achim D. Brucker and Diego Marmsoler},
  booktitle = {Formal Methods Teaching (FMTea 2024)},
  language  = {English},
  doi       = {10.1007/978-3-031-71379-8_8},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {14939},
  editor    = {Leila Ribeiro and Emil Sekerinski},
  title     = {Teaching Formal Methods in Application Domains: A Case Study
               in Computer and Network Security},
  areas     = {formal methods, security, pedagogy},
  year      = {2024},
  isbn      = {978-3-642-38915-3},
  note      = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-fm-teaching-2024/}},
}