2 Motivation

Motivation [Slide 2]

• Fusion Logic has be used to specify history based access control policies[2].
• History-based access control policies govern the behaviour of a system based on previously observed events in the execution of the system.
• The decision procedure can therefore be used to verify properties about access control policies.
• A ‘slightly’ modified version of the decision procedure[2] can be used to efficiently enforce these policies.

Motivation [Slide 3]

Temporal Logic:

• Reasoning about behaviours, i.e., sequences (traces) of system states

• Linear Temporal Logic (LTL):

  (next), in the next state,

  (previous), in the previous state,

  (always), all states in the behaviour,

  (has always been), all previous states in the behaviour,

  (sometimes), exist a state in the behaviour

• Interval Temporal Logic (ITL):

  skip, behaviour with exactly two states,

  ; (Chop), fusion of two behaviours,

  (past Chop), past fusion of two behaviours,

  ^∗ (chopstar), fusion of a finite number of behaviours

• Propositional Interval Temporal Logic (PITL):

  ITL with only propositional variables, i.e., Boolean values.

• Fusion Logic has both LTL and ITL operators.

Motivation [Slide 4]

Verification tools for Propositional Interval Temporal (PITL):

• Tempura , Ben Moszkowski, Roger Hale and Antonio Cau 1985. Executable specification, testing
• ITL Library for interactive theorem prover PVS , Antonio Cau, 1997. Axioms via Higher-order Logic
• AnaTempura , Antonio Cau, Shikun Zhou, 1999. Runtime verification, Tempura
• DCVALID , Paritosh Pandya, 2000. MONA, decision procedure for WS1S
• PITL2Mona[3], Rodolfo Gomez and Howard Bowman, 2004. MONA, decision procedure for WS1S
• JavaLite , Shinji Kono, 2008. BDD, Tableau-based
• PITL Library for automated theorem prover Prover9 , Antonio Cau, 2008. Algebra, proof search
• ITL library for Isabelle/HOL , Antonio Cau and David Smallwood, 2018. Axioms via Higher-order Logic