cicyt UNIZAR
Full-text links:

Download:

Current browse context:

cs.CR

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Cryptography and Security

Title: Attack Trees in Isabelle -- CTL semantics, correctness and completeness

Abstract: In this paper, we present a proof theory for attack trees. Attack trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we succeed in developing a generic theory of attack trees with a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of attack trees and at the same time the developed proof theory enables application to case studies. A central correctness result proved in Isabelle establishes a connection between the notion of attack tree validity and a CTL attack statement. The application is illustrated on an insider attack on healthcare IoT systems.
Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO)
Cite as: arXiv:1803.06494 [cs.CR]
  (or arXiv:1803.06494v1 [cs.CR] for this version)

Submission history

From: Florian Kammueller [view email]
[v1] Sat, 17 Mar 2018 12:19:44 GMT (182kb,D)