arXiv:1302.2123v3 [cs.LO] 4 Aug 2013
Belief Semantics of Authorization Logic
Andrew K. Hirsch
Department of Computer Science
George Washington University
Washington, D.C., United States
akhirsch@gwu.edu
Michael R. Clarkson
Department of Computer Science
George Washington University
Washington, D.C., United States
clarkson@gwu.edu
ABSTRACT
Authorization logics have been used in the theory of com-
puter security to reason about access control decisions. In
this work, a formal belief semantics for authorization logics
is given. The belief semantics is proved to subsume a stan-
dard Kripke semantics. The belief semantics yields a direct
representat ion of principals’ beliefs, without resorting to the
technical machinery used in Kripke semantics. A proof sys-
tem is given for the logic; that system is proved sound with
respect to the belief and Kripke semantics. The soundness
proof for the belief semantics, and for a variant of the Kripke
semantics, is mechanized in Coq.
Categories and Subject Descriptors
D.4.6 [Operating Syste ms]: Security and Protection—Ac-
cess controls; F.4.1 [Mathematical Logic and Formal
Languages]: Mathematical Logic—modal logic, model the-
ory, proof theory, mechanical theorem proving
Keywords
Authorization logic; NAL; CDD
1. INTRODUCTION
Authorization logics are used in computer security to rea-
son about whether principals—computer or human agents—
are permitted to take actions in computer systems. The dis-
tinguishing feature of authorization logics is their use of a
says connective: intuitively, if principal p believes that for-
mula φ holds, then formula p says φ holds. Access control
decisions can then be made by reasoning about (i) the be-
liefs of principals, (ii) how those beliefs can be combined to
derive logical consequences, and (iii) whether those conse-
quences entail guard formulas, which must hold for actions
to be permitted.
Many systems that employ authorization logics h ave been
proposed [5–9, 11, 12, 17, 23, 28, 29, 32– 35, 40, 44, 51], but few
authorization logics have been given a formal semantics [4,
Copyright 2013 Andrew K. Hirsch and Michael R. Clarkson.
18, 19, 22, 26]. Though semantics might not be immediately
necessary to deploy authorization logics in real systems, se-
mantics yield insight into the meaning of formulas, and se-
mantics enable proof systems to be proved sound—which
might require proof rules and axioms to be corrected, if t here
are any lurkin g errors in the proof system.
For the sake of security, it is worthwhile to carry out such
soundness proofs. Given only a proof system, we must trust
that the p roof system is correct. But given a proof system
and a soundness proof, which shows that any provable for-
mula is semantically valid, we now have evidence that the
proof system is correct, hence trustworthy. The soundness
proof thu s relocates trust from the proof system to the proof
itself—as well as to the semantics, which ideally offers more
intuition about formulas than the proof system itself.
Semantics of authorization logics are usually based on pos-
sible worlds, as used by Kripke [31]. Kripke semantics posit
an indexed accessibility relation on possible worlds. If at
world w, principal p considers world w
′
to be possible, then
(w, w
′
) is in p’s accessibility relation. We denote this as
w ≤
p
w
′
. Authorization logics use Kripke semantics to give
meaning to the says connective: semantically, p says φ holds
in a world w iff for all worlds w
′
such that w ≤
p
w
′
, formula
φ holds in world w
′
. Hence a princip al says φ iff φ holds in
all worlds the principal considers possible.
1
The use of Kripke semantics in authorization logic thus
requires installation of possible worlds and accessibility re-
lations into the semantics, solely to give meaning to says.
That’s useful for studying properties of logics and for build-
ing decision procedures. But, unfortunately, it doesn’t seem
to correspond to how principals reason in real-world systems.
Rather than explicitly considering possible worlds and rela-
tions between them, principals ty pically begin with some
set of base formulas they believe to hold—perhaps because
they have received digitally signed messages encoding those
formulas, or perhaps because they invoke sy stem calls that
return in formation—then proceed to reason from those for-
mulas. So could we instead stipulate that each principal p
have a set of beliefs ω(p), called the worldview of p, such
that p says φ holds iff φ ∈ ω(p)? That is, a principal says φ
iff φ is in the worldview
2
of the principal?
This paper answers that question in the affirmative. We
give two semantics for an authorization logic: a Kripke se-
1
The says connective is, therefore, closely related to the
mod al necessity operator ✷ [27] and the epistemic knowl-
edge operator K [15].
2
Worldviews were first employed by NAL [42], which pio-
neered an informal semantics based on them.
