Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
Logic in Computer Science
2024-01-01 v1
Abstract
In this paper we present an efficient approach to implementing model checking in the Higher Order Logic (HOL) of Isabelle. This is a non-trivial task since model checking is restricted to finite state sets. By restricting our scope to considering security attacks, we achieve an efficient executable specification of a model checking algorithm for attack trees. We provide the existing background, the necessary theory and illustrate its application. Theory and application are fully formalized in Isabelle thus providing an executable model checking algorithm.
Cite
@article{arxiv.2312.17555,
title = {Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security},
author = {Florian Kammüller},
journal= {arXiv preprint arXiv:2312.17555},
year = {2024}
}
Comments
arXiv admin note: text overlap with arXiv:1803.06494