Network Security Policy Verification


Title: Network Security Policy Verification
Author: Cornelius Diekmann
Submission date: 2014-07-04
Abstract: We present a unified theory for verifying network security policies. A security policy is represented as directed graph. To check high-level security goals, security invariants over the policy are expressed. We cover monotonic security invariants, i.e. prohibiting more does not harm security. We provide the following contributions for the security invariant theory.
  • Secure auto-completion of scenario-specific knowledge, which eases usability.
  • Security violations can be repaired by tightening the policy iff the security invariants hold for the deny-all policy.
  • An algorithm to compute a security policy.
  • A formalization of stateful connection semantics in network security mechanisms.
  • An algorithm to compute a secure stateful implementation of a policy.
  • An executable implementation of all the theory.
  • Examples, ranging from an aircraft cabin data network to the analysis of a large real-world firewall.
  • More examples: A fully automated translation of high-level security goals to both firewall and SDN configurations (see Examples/Distributed_WebApp.thy).
For a detailed description, see
Change history: [2015-04-14]: Added Distributed WebApp example and improved graphviz visualization (revision 4dde08ca2ab8)
  author  = {Cornelius Diekmann},
  title   = {Network Security Policy Verification},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2014,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Automatic_Refinement, Transitive-Closure