Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security

Florian Kammüller

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 restri…