Modal and temporal logic for computer security

In the previous post, I mentioned that modal logic has a lot of interpretations and a lot of axiom systems. It can also have a lot of operators. This post will look at Security Logic, a modal logic for security applications based on a seminal paper by Glasgow et al [1]. It illustrates how modal and temporal logic can be applied to computer security, and it illustrates how a logic system can have a large number of operators and axioms.

Knowledge axioms

Security Logic starts with operators K_i that extend the box operator □. For a proposition p, K_i p is interpreted as saying that the ith agent knows p to be true. Glasgow et al chose the following axioms for inference regarding K_i.

Axiom K1:   K_i φ → φ
Axiom K2:   K_i(φ → ψ) → (K_i φ → K_i ψ)
Axiom K3:   K_i φ → K_i K_i φ
Axiom K4:   ¬ K_i φ → K_i( ¬ K_i φ)

These can be interpreted as follows.

If you know something to be true, it’s true.
If you know one thing implies another, then knowing the first lets you know the other.
If you know something, you know that you know it.
If you don’t know something, you know that you don’t know it.

This is not to claim that these propositions are universal metaphysical truths, only modeling assumptions. It may be possible, for example, to know something without knowing that you know it, but that’s a subtle matter excluded from this model.

Temporal logic axioms

Temporal logic is modal logic with operators interpreted as applying to propositions over time. Glasgow et al introduce three temporal operators: ∀□, ∀◇, and  ∃□. Note that each of these is a single operator; there is no box or diamond operator in Security Logic.

∀□p means that p always holds, ∀◇p means that p eventually holds, and ∃□p means that p sometimes holds.

The ∃□ and ∀□ operators are dual in the same sense that the basic modal operators □ and ◇ are dual:

∃□p ↔︎ ¬ ∀□ ¬p
∀□p ↔︎ ¬ ∃□ ¬p

Security Logic not give axioms for ∃□ because its behavior is determined by the axioms for ∀□.

The three temporal logic axioms for Security Logic are as follows.

Axiom T1:  φ → ∀◇φ
Axiom T2:  ∀□(φ → ψ) → (∀□φ → ∀□ψ)
Axiom T3:  ∀□φ → ∀□ ∀□φ

These can be interpreted as follows.

If a proposition holds, it eventually holds.
If its always the case that one proposition implies another, then if the former always holds then the latter always holds.
If something always holds, then it always always holds.

Obligation and Permission

Finally, Security Logic introduces modal operators O and P for obligation and permission.

Obligation and permission are dual, just as necessity and possibility are dual and the always and sometimes operators are dual.

Op ↔︎ ¬ P ¬p
Pp ↔︎ ¬ O ¬p

When obligation and permission are combined with knowledge, Security Logic introduces the following abbreviations.

O_i = OK_i
P_i = PK_i

Axioms for Security Logic

The complete axioms for Security Logic are the four knowledge axioms above, the three temporal axioms above, and the five additional axioms below.

Axiom SL1:   P_i φ for all propositional tautologies φ.
Axiom SL2:  P_i φ → φ
Axiom SL3:  (P_i φ ∧ P_i ψ) ↔︎ P_i (φ ∧ ψ)
Axiom SL4:  P_i φ → P_i (φ ∨ ψ)
Axiom SL5:  O_i φ → P_i φ

These can be interpreted as follows.

You are permitted to know all tautologies.
Whatever is permitted must be true.
Permission holds through conjunction and disjunction.
Whatever is obligatory must be permissible.

Related posts

• Typesetting modal logic
• Automated theorem proving
• Passwords and power laws
• Data privacy

[1] Janice Glasgow, Glenn MacEwen, and Prakash Panangaden. A Logic for Reasoning About Security. ACM Transactions on Computer Systems, Vol 10 No 3, August 1992, pp 226–264.