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 *i*th 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}=*P*K_{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

[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.

Lamport has done some brilliant work here with his TLA+, which is used super-aggressively at both Google and AWS as practical ways of checking program correctness — and security.

These things are below Coq and Agda, naturally and seem a lot easier to use.

There a number of excellent papers on this and it’s actually an exciting burgeoning field of practical application…