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 axiomsSecurity Logic starts with operators Ki that extend the box operator a-. For a proposition p, Kip is interpreted as saying that the ith agent knows p to be true. Glasgow et al chose the following axioms for inference regarding Ki.
Axiom K1: Ki I a' I
Axiom K2: Ki(I a' I) a' (Ki I a' Ki I)
Axiom K3: Ki I a' KiKi I
Axiom K4: Ki I a' Ki( Ki 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 axiomsTemporal logic is modal logic with operators interpreted as applying to propositions over time. Glasgow et al introduce three temporal operators: aa-, aa-, and afa-. Note that each of these is a single operator; there is no box or diamond operator in Security Logic.
aa-p means that p always holds, aa-p means that p eventually holds, and afa-p means that p sometimes holds.
The afa- and aa- operators are dual in the same sense that the basic modal operators a- and a- are dual:
afa-p 
aa- p
aa-p afa- p
Security Logic not give axioms for afa- because its behavior is determined by the axioms for aa-.
The three temporal logic axioms for Security Logic are as follows.
Axiom T1: I a' aa-I
Axiom T2: aa-(I a' I) a' (aa-I a' aa-I)
Axiom T3: aa-I a' aa- aa-I
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.
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.
Oi = OKi
Pi = PKi
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: Pi I for all propositional tautologies I.
Axiom SL2: Pi I a' I
Axiom SL3: (Pi I a Pi I) Pi (I a I)
Axiom SL4: Pi I a' Pi (I a I)
Axiom SL5: Oi I a' Pi 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.
[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.