In this paper we show that the logical framework proposed by Becker et al. to reason about security policy behavior in a trust management context can be captured by an operational framework that is based on the language proposed by Miller to deal with scoping and/or modules in logic programming in 1989. The framework of Becker et al. uses propositional Horn clauses to represent both policies and credentials, implications in clauses are interpreted in counterfactual logic, a Hilbert-style proof is defined and a system based on SAT is used to proof whether properties about credentials, permissions and policies are valid in trust management systems, i.e. formulas that are true for all possible policies. Our contribution is to show that instead of using a SAT system, this kind of validation can rely on the operational semantics (derivability relation) of Miller's language, which is very close to derivability in logic programs, opening up the possibility to extend Becker et al.'s framework to the more practical first order case since Miller's language is first order.
Trust Management Systems (TMS) [BFL96] are perhaps the most common model to describe distributed access control. In this model, there are (1) policies that define under what conditions a subject is able to access resources, (2) credentials that are provided by the subject in order to fulfill policies and (3) decisions of whether a subject has particular permissions. One of the most popular ways to describe TMS is to use logic programming-like languages for definition of policies and credentials (see for example [DeT02], [JIM01],[LGF00],[LM03]).
tials.
Working under this framework, Becker et al. [BRS12] have recently proposed a logic system in which one can reason about TMS in general. In this system, a Hilbert-style axiomatization is defined and a system based on SAT solvers is used to prove automatically TMS properties. In their logic, policies and credentials are formalized using propositional logic programs, while permissions are propositional Boolean formulas. Trust management behavior, i.e. to determine whether a permission p is true under a policy P when presenting a set of credentials Q, is captured by proving that the statement Q p holds in the policy P.3 This statement is true if p holds in the policy P extended with those clauses in the credentials Q: P [ Q ` p.
that says ”if X paid the fee Fee for the music Music, X is able to download
paypal or by means of a wire transfer”.4 These statements represent schemes of policies for specific values of the arguments. Credentials for paying the fee presented by a subject X to request download permission can be written as follows:
(paypal(X ; 1:99$) X :paid(song; 1:99$)) X :download(song)
the credential (paypal(X ; 1:99$) X :paid(song; 1:99)) in a single program and then verify that the permission X :download(song) holds in it.
formulas in TMS. Informally, these are formulas that are true regardless of the policies and credentials that can be defined in the TMS. Hence, they are able to describe how to approach proofs such as proving attacks (i.e. discovering policies) in specific TMS systems, or general properties such as the transitivity of credential-based derivations.
The authors, however, argue that Hilbert style axiomatizations are difficult for building proofs because they are not goal oriented. Hence, they resort to an algorithm that interleaves syntactic transformations of formulas and calls to SAT solvers in order to do automatic verifications. In their paper there is an argument but not a proof that the mechanization is correct. A proof may be possible but probably not easy.
seller has access to paypal and the bank.
In this work we show that the logical framework proposed by Becker et al. can be captured by an operational framework that is based on a language proposed by Miller in 1989 to deal with scoping and/or modules in logic programming. Our contribution is to show that we can rely on the operational semantics (derivability relation) of Miller’s language, which is very close to derivability in logic programs, to do goal oriented formula verification. This connection also open the possibility of extending Becker et al.’s framework to the more practical first order case since Miller’s language is first order. 2
Trust management systems
Definition 1. Programs, clauses and goals are defined using the BNF presented below, where A, F, C, P and G range over (1) atoms, conjunctions of atoms, (2) clauses, (3) programs and (4) goals, respectively.
(1) F ::= true j A j F ^ F (3) P ::= C j C; P (2) C ::= F A (4) G ::= F j :G j P
G j G ^ G j G _ G Perhaps the most unusual definition is the definition of goals. A goal is either an expression of the form P G, where P is a program and (inductively) G a goal or an expression corresponding to a propositional formula built with the standard connectives :, ^ and _. We note that our goals are the formulas defined in Becker et al.’s. As usual, we define implication, G1 ! G2, as :G1 _ G2 and equivalence, G1 $ G2, as (G1 ! G2) ^ (G2 ! G1). Throughout the rest of the paper, we adopt the following conventions: P and Q denote programs. Clauses may be embraced in parenthesis. In a clause of the form true p we simply write p. 2.1
Reasoning in trust management systems
credentials and permissions. We denote this framework by Oˆ -TMF. The Oˆ -TMF framework is based on the language introduced in [Mil89]. The semantics is presented in terms of a derivation relation over sequents. A sequent is a pair of the form P ` G, where the program P is called the antecedent and the goal
implications is that, given a program P, to prove the query Q G it is necessary to prove G with the program P [ Q. This is formalized in [Mil89] using the following inference rule:
P [ Q ` G
P ` Q G 2.2
Oˆ - proof rules
as follows
P`POˆ`GOˆ1G_iG2 i = 1; 2 P`Oˆ :G1^:G2 P`Oˆ :(G1_G2)
P`Oˆ G1 P`Oˆ G2
P`Oˆ G1^G2 P`Oˆ :G1_:G2 P`Oˆ :(G1^G2)
P[Q`Oˆ G P`Q G
P`Oˆ A P`Oˆ ::A
P`Oˆ Q :G P`Oˆ :(Q G) An Oˆ -proof for P `Oˆ G is a tree in which nodes are labeled with sequents such that (i) the root node is labeled with P `Oˆ G, (ii) the internal nodes are instances of one of the above inference rules and (iii) the leaf nodes are labeled with initial sequents. An initial sequents is a sequent of the form P0 `Oˆ G0 where G0 is a propositional formula that is true in the minimal model of P0.
propositional atoms occurring in G. G is valid, `Oˆ G, in the Oˆ -TMF if and only if it is not possible to find a SG-policy D such that D `Oˆ :G
G = :a ^ d :e ^ (a b ^ c d) e ! c ^ d a where SG = fa; b; c; d; eg. Following Definition 2, `Oˆ G if and only if it is not possible to find SG-policy D such that D `Oˆ :G. Hence, we have to prove that there is not D such that D `Oˆ :(:a ^ d :e ^ (a b ^ c d) e ! c ^ d
D `Oˆ :a ^ d :e ^ (a b ^ c d) e ^ (:c _ :(d a) a)) Distributing ^ over _ we obtain that we have to prove there is no D such that: 1. D `Oˆ :a ^ d :e ^ (a b ^ c d)
e ^ :c (a) D `Oˆ :a: Since we are looking for a counter-example, we need to make this sequent an initial sequent, so we have to construct a policy D whose minimal model, MD, contains the valuation a = f alse. This is a 2= MD. It is worth to notice that the scoping of D is the whole formula. (b) D `Oˆ d :e: if and only if D [fdg `Oˆ :e and this is an initial sequent if the valuation e = f alse is in the minimal model of D [fdg. Hence, e 2= MD. (c) D `Oˆ (a b ^ c d) e: if and only if D [fa b; c dg `Oˆ e but this is not possible since :e holds in MD.
Therefore, D 0Oˆ :a ^ d :e ^ (a b ^ c d) e ^ :c 2. D `Oˆ :a ^ d :e ^ (a b ^ c d) e ^ :(d a). In this case, directly by item 1c above we get that D 0Oˆ :a ^ d :e ^ (a b ^ c d) e ^ :(d a) Since we cannot construct a (counter-example) policy for :G, then `Oˆ G. 3
Equivalence of Oˆ -TMF and Becker et al.’s TMS
equivalent to Becker et al.’s. First, we recall some definitions from [BRS12]. Let basic goals be atoms and classical propositional compound formulas expressed in terms of ^ and :. Let P be a policy, MP its minimal model and G a basic goal.
define that P Q G if and only if P [ Q G, where Q is a policy. A goal
Proposition 1. Let Q
P Q G if and only if P `Oˆ Q G The proof follows by induction by showing that P Q1 : : : Qk G iff P `Oˆ Q1 : : : Qk G using the definition of and the -Oˆ rule. As a corollary we also have
P G if and only if P `Oˆ G (1)
` j (2)
Oˆ G Theorem 1. Let G be a goal. Then, ` G if and only if Proof. From (1) and (2) it follows that ` G if and only if `Oˆ G
Final remarks
that not only atoms but also rules can be assumed in order to find Ds (see Def. 2).
tures following Miller’s models. In particular, Miller interprets a world of a Kripke’s model as a program and the knowledge at each world as its minimal model. This intuition can be explained in terms of two basic ideas of modal logic. The first one is the notion that a world may be considered to represent the “knowledge” that we have at a certain moment. The second idea is that a formula can be considered to hold if we can infer its truth from the knowledge that we have now or one that we may acquire in the “future”, capturing the idea of credentials. Details will appear in the full version of this paper.
An important consequence of the connections between Miller’s language and the propositional logic for reasoning in TMS is the possibility of lifting the results to policies, credentials and permissions with variables. We cannot apply directly Miller’s results because his logic doesn’t deal with negation. There is, however, an extensions to Miller’s logic that deals with normal logic programs [POPN12], but we need to work out the details of the axiomatization since the approach in [POPN12] uses a notion similar to Clark’s completion as opposed to minimal models. Complementary to these extensions we will also like to check how an implementation of validity using our approach will compare to the implementation of Becker et al.