Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2312.17555 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909057061748736 |
|---|---|
| author | Kammüller, Florian |
| author_facet | Kammüller, Florian |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2312_17555 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security Kammüller, Florian Logic in Computer Science 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. |
| title | Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2312.17555 |