We define an Intuitionistic Conditional Logic for Access Control called CICL . The logic CICL is based on a conditional language allowing principals to be defined as arbitrary formulas and it includes few uncontroversial axioms of access control logics. We provide an axiomatization and a Kripke model semantics for the logic CICL , prove that the axiomatization is sound and complete with respect to the semantics, and define a sound, complete and cut-free labelled sequent calculus for it.
Introduction
Access control is concerned with the decision when to accept or deny a request from
a principal (e.g., user, program) to do an operation on an object. In practice, an access
control system is a product of several, often independent, distributed entities with
different policies that interact in order to determine access to resources. In order to specify
and reason about such systems, many formal frameworks have been proposed [
A common feature of most well-known approaches is the employment of
constructive logics enriched with formulas of the form A says ϕ, intuitively meaning that the
principal A asserts or supports ϕ to hold in the system. In [
The treatment of the operator “says” as a modality can be found in [
In this paper we show that conditional logics [
From the access control point of view, the says operator satisfies the axioms of
the “basic logic of access control” ICL [
The paper is structured as follows. In Section 2 we introduce the axiomatization and the semantics for the intuitionistic conditional logic CICL and we compare it with existing approaches. In Section 3 we show that the axiomatization is sound and complete with respect to the semantics. In Section 4 we define a cut-free sequent calculus for CICL and we prove its soundness and completeness. Section 5 contains the conclusions and a discussion of related work. 2
In this section, we introduce the conditional intuitionistic logic CICL for access control
by defining its axiomatization and Kripke semantics. Then we discuss some conditional
axioms which can be introduced to model properties of boolean principals, namely
compound principals formed by boolean connectives. Indeed, while the basic axioms
for access control are rather uncontroversial [
The formulation of the says modality as a conditional operator allows boolean principals to be modelled in a natural way, since in a conditional formula A says φ, both A and φ are arbitrary formulas. For instance, we can write, A ∧ B says φ to mean that principals A and B jointly say that φ, and A ∨ B says φ to mean that principals A and B independently say that φ. Indeed, conditional logics provide a natural generalization of multimodal logics to the case when modalities are labelled by arbitrary formulas. 2.1
Axiom System We define the language L of the logic CICL . Let ATM be a set of atomic propositions. The formulas of L are defined inductively as follows: if P ∈ ATM , then P ∈ L; ⊥ ∈ L, where ⊥ is a proposition which is always false; if A, ϕ, ϕ1 and ϕ2 are formulas of L, then ¬ϕ, ϕ1 ∧ ϕ2, ϕ1 ∨ ϕ2, ϕ1 → ϕ2, and A says ϕ are formulas of L.
The intended meaning of the formula A says ψ, where A and ψ are arbitrary
formulas, is that principal A says that ψ, namely, “the principal A asserts or supports ψ”
[
The axiom system of the logic CICL contains the following axioms and inference
rules:
all tautologies of intuitionistic logic
A says (α → β) → (A says α → A says β)
α → (A says α)
(A says (A says α)) → (A says α)
If ⊢ α and ⊢ α → β then ⊢ β
If ⊢ A ↔ B then ⊢ (A says γ) ↔ (B says γ)
If ⊢ α → β then ⊢ (A says α) → (A says β)
We say that a formula α is a theorem of the logic, and write ⊢ α if there is a derivation
of α from the above axioms and rules. We say that α can be derived from a set of
formulas Γ , and write Γ ⊢ α, if there are γ1, . . . γn in Γ such that ⊢ γ1 ∧ . . . ∧ γn → α.
The rule (MP) is modus ponens. (RCEA) and (RCK) are standard inference rules for
conditional logics. (RCK) plays the role of the rule of Necessitation (if ⊢ φ then ⊢ 2φ)
in modal/multimodal logic. The axiom (K) belongs to the axiomatization of all normal
modal logics and it is derivable in “normal” conditional logics. (UNIT), (K) and (C4)
are the characterizing axioms of the access control logics ICL [
Semantics The semantics of the logic CICL is defined as follows.
Definition 1. A CICL model has the form M = (S, ≤, {RA}, h) where: S 6= ∅ is a set of items called worlds; ≤ is a partial order over S; RA is a binary relation on S associated with the formula A; h is an evaluation function ATM −→ P ow(S) that associates to each atomic proposition P the set of worlds x in which P is true.
We define the truth conditions of formulas with respect to worlds in a model M, by the relation M, x |= φ, as follows. We use [|φ|] to denote {y ∈ S | M, y |= φ}. 1. M, t |= P ∈ ATM iff, for all s such that t ≤ s, s ∈ h(P ) 2. M, t |= ϕ ∧ ψ iff M, t |= ϕ and M, t |= ψ 3. M, t |= ϕ ∨ ψ iff M, t |= ϕ or M, t |= ψ 4. M, t |= ϕ → ψ iff for all s such that t ≤ s (if M, s |= ϕ then M, s |= ψ) 5. M, t |= ¬ϕ iff, for all s such that t ≤ s, M, s 6|= ϕ 6. M, t 6|= ⊥ 7. M, t |= A says ψ iff, for all s such that tRAs, M, s ψ.
We say that φ is valid in a model M if M, t |= φ for all t ∈ S. We say that φ is valid tout court (and write |= φ) if φ is valid in every model. We extend the notion of validity to a set of formulas Γ in the obvious way: for all t, M, t |= Γ if M, t |= ψ for all ψ ∈ Γ . Last, we say that φ is a logical consequence of Γ (and write Γ |= φ) if, for all models M, for all worlds t, if M, t |= Γ , then M, t |= φ.
The relations ≤ and RA must satisfy the following conditions: (a) ∀t, s, z ∈ S, if s ≤ t and tRAz then sRAz; (b) ∀t, s ∈ S, if sRAt, then s ≤ t; (c) ∀t, s ∈ S, if sRAt, then ∃z ∈ S such that sRAz and zRAt (d) if [|A|] = [|B|], then RA = RB , Conditions (b) and (c) are, respectively, the semantic conditions associated with the axioms (UNIT) and (C4), while condition (a) is needed to enforce the property that a formula true in a world t is also true in all worlds reachable from s by the relation ≤ (i.e., in all worlds s such that t ≤ s). Condition (d) is the well-known condition for normality in conditional logics, claiming that the accessibility relation RA is associated with the semantic interpretation of A.
Observe that, in the semantics above, the binary relation RA plays the role of the selection function f , which is used in most formulations of conditional logic semantics. In particular, sRAt corresponds to t ∈ f (A, s), and conditions (a), (b), (c) and (d) above are indeed conditions on the selection function f , as usual in conditional logics.
It is worth noticing that the notion of logical consequence defined above can be used to verify that a request ϕ of a principal A is compliant with a set of policies. Intuitively, given a set of formulas Γ representing policies, we say that A is compliant with Γ iff Γ, A says ϕ |= ϕ. For instance, if Γ contains the following formulas: we obtain that ((admin says deletefile1 ) → deletefile1 ) admin says (Bob says deletefile1 → deletefile1 ) Γ, Bob says deletef ile1 |= deletef ile1 2.3
Discussion
Before proving the soundness and completeness result for the logic CICL , we want
to comment about our approach for allowing boolean principals as compared with the
approach proposed by Garg and Abadi in [
Garg and Abadi [
In [
For what concerns non-atomic principals, Garg and Abadi [
The conditional logic we have defined is rather weak, as it does not contain
specific axioms which would enforce intended properties of boolean principals, as those
discussed in [
Concerning the statement A ∨ B says φ, we could expect that A and B disjointly (independently) say that φ if both A says φ and B says φ. This property can be captured by the following axiom:
which corresponds to the well known axiom (CA) of conditional logics [
holds. The two axioms together would enforce the property that A and B disjointly say
that φ if and only if A says that φ and B says that φ . Mutatis mutandis, this appears
to be a wanted property, according to [
which, however, is a very controversial axiom of conditional logics, called monotonicity.
The impact of the addition of the above axioms to the axiomatization of the logic CICL has to be studied. While we could expect the addition of the axiom (CA) and its converse to be armless, the same cannot be said for the monotonicity axiom, whose introduction could cause the logic to collapse or become inconsistent. 3
Soundness and Completeness In this section we prove that the axiomatization given above is sound and complete with respect to the semantics of Definition 1.
Theorem 1 (Soundness). The axiomatization of the logic CICL given in Section 2.1 is sound w.r.t. the semantics in Definition 1: given a formula ϕ ∈ L, if Γ ⊢ ϕ, then Γ |= ϕ.
Proof. It is easy to prove that each axiom is a valid formula and, for each inference
rule, if the antecedent of the rule is a valid formula, the consequence of the rule is also
a valid formula.
The completeness proof we present is based on the proof of completeness for the Kripke
semantics of intuitionistic logic in [
Lemma 1 (Saturated Extensions). Suppose Γ 6⊢ ϕ, then there is a saturated extension Γ ∗ of Γ such that Γ ∗ 6⊢ ϕ.
Lemma 2. Let Γ be a set of formulas and let Δ = {ϕ : A says ϕ ∈ Γ }. If Δ ⊢ ψ, then Γ ⊢ A says ψ.
Proof. Suppose there is a derivation of ψ from Δ. Then, there must be a finite set of formulas {ϕ1, . . . , ϕn} ⊆ Δ such that {ϕ1, . . . , ϕn} ⊢ ψ. By definition of ⊢, ⊢ ϕ1 ∧ . . . ∧ ϕn → ψ. By (RCK) and (K), ⊢ A says ϕ1 ∧ . . . ∧ A says ϕn → A says ψ, and from definition of ⊢ (and since A says ϕi ∈ Γ for all i = 1, . . . , n) we conclude that Γ ⊢ A says ψ. 2 Definition 4 (Canonical model construction). Let Γ0 be any saturated set of formulas. Then we define M = (S, ≤, {RA}, Γ0, h) such that: S is the set of all saturated Γ ⊇ Γ0; Γ1 ≤ Γ2 iff Γ1 ⊆ Γ2; Γ1RAΓ2 iff {α | A says α ∈ Γ1} ⊆ Γ2; for all P ∈ ATM , h(P ) = {Γ ∈ S | P ∈ Γ }.
Observe that in the above construction, Γ0 ∈ S.
Lemma 3. For all Γ ∈ S and each wff formula ϕ, we have that Γ |= ϕ iff ϕ ∈ Γ . Proof. By induction on the complexity of ϕ. In case ϕ is an atomic formula, the lemma holds by definition. For ϕ ≡ φ ∧ ψ the proof is easy and therefore omitted. For ϕ ≡ φ ∨ ψ, then Γ |= φ ∨ ψ ⇔ (Γ |= φ or Γ |= ψ) ⇔ (φ ∈ Γ or ψ ∈ Γ ) ⇔ φ ∨ ψ ∈ Γ (by the saturation of Γ ). For ϕ ≡ φ → ψ, suppose Γ |= φ → ψ. Then for all saturated Γ ′ ⊃ Γ we have that if Γ ′ |= φ, then Γ ′ |= ψ. Assume Γ 6⊢ φ → ψ, then Γ ∪ {φ} 6⊢ ψ; let Γ ′ be a saturated extension of Γ ∪ {φ} such that Γ ′ 6⊢ ψ, then Γ ′ |= φ but not Γ ′ |= φ (induction hypotesis); this contradicts Γ |= φ → ψ, hence Γ ⊢ φ → ψ. As Γ is saturated, by condition 2 in Definition 3, φ → ψ ∈ Γ . The converse is trivial. For ϕ ≡ A says φ, suppose Γ |= A says φ. Hence, for all Γ ′ such that Γ RAΓ ′, Γ ′ |= φ. By inductive hypothesis, φ ∈ Γ ′. Let Δ = {α : A says α ∈ Γ }. By construction, Γ ′ ⊇ Δ. Assume, for a contradiction, that A says φ 6∈ Γ . By condition 2 in Definition 3, Γ 6⊢ A says φ. Then, by Lemma 2, Δ 6⊢ φ. By Lemma 1, there is a saturated extension Δ∗ of Δ such that Δ∗ 6⊢ φ. This contradicts the fact that, for all Γ ′ such that Γ RAΓ ′, φ ∈ Γ ′. The converse is trivial. 2 Lemma 4. Let M be the canonical model as defined in Definition 4. M satisfies the semantic conditions (a), (b), (c), and (d).
Proof. We have to prove that (a) ∀Γ, Γ ′, Γ ′′ ∈ S, if Γ ≤ Γ ′ and Γ ′RAΓ ′′ then Γ RAΓ ′′ (b) ∀Γ, Γ ′ ∈ S, if Γ RAΓ ′ then Γ ≤ Γ ′. (c) ∀Γ, Γ ′ ∈ S, if Γ RAΓ ′, then ∃Γ ′′ ∈ S such that Γ RAΓ ′′ and Γ ′′RAΓ ′ (d) ∀Γ, Γ ′ ∈ S, if Γ RAΓ ′ and ⊢ A ↔ B then Γ RBΓ ′.
The proof is straightforward. As an example, let us prove point (b). Given a saturated set Γ , we have to show that if Γ RAΓ ′ then Γ ≤ Γ ′. Assume that Γ RAΓ ′ and let α ∈ Γ . By saturation of Γ and by (UNIT), α → A says α ∈ Γ . By (MP), A says α ∈ Γ . Hence, by construction of the canonical model, α ∈ Γ ′. Therefore, Γ ≤ Γ ′.
Theorem 2 (Completeness). The axiomatization of the logic CICL given in Section 2.1 is complete with respect to the semantics in Definition 1: given a formula ϕ ∈ L, if Γ |= ϕ, then Γ ⊢ ϕ.
Proof. For a contradiction, suppose Γ 6⊢ ϕ. Then by Lemma 1 there is a saturated extension Γ ∗ of Γ such that Γ ∗ 6⊢ ϕ. By Definition 4 and Lemmas 3 and 4, we conclude that there is a (canonical) model M = (S, ≤, {RA}, Γ ∗, h) such that M, Γ ∗ |= Γ ∗ and M, Γ ∗ 6|= ϕ. Since Γ ⊆ Γ ∗, also M, Γ ∗ |= Γ . It follows that ϕ is not a logical consequence of Γ , i.e. Γ 6|= ϕ. 2 2 4
In this section we present a sequent calculus for CICL . Our calculus is called SeqCICL
and it makes use of labels to represent possible worlds, following the line of [
In addition to the language L of the logic CICL , we consider a denumerable alphabet of labels A, whose elements are denoted by x, y, z, . . .. There are three types of labelled formulas: 1. world formulas, denoted by x : A, where x ∈ A and A ∈ L, used to represent that the formula A holds in a world x;
A 2. transition formulas, denoted by x −→ y, representing that xRAy; 3. order formulas of the form y ≥ x representing the partial order relation ≤. A sequent is a pair hΓ, Δi, usually denoted with Γ ⇒ Δ, where Γ and Δ are multisets of labelled formulas. The intuitive meaning of a sequent Γ ⇒ Δ is: every model that satisfies all labelled formulas of Γ in the respective worlds (specified by the labels) satisfies at least one of the labelled formulas of Δ (in those worlds). This is made precise by the notion of validity of a sequent given in the next definition: Definition 5 (Sequent validity). Given a model M = (S, ≤, {RA}, h) for L, and a label alphabet A, we consider a mapping I : A → S. Let F be a labelled formula, we define M |=I F as follows: – M |=I x : A iff M, I(x) |= A
A – M |=I x −→ y iff I(x)RAI(y) – M |=I y ≥ x iff I(x) ≤ I(y) We say that Γ ⇒ Δ is valid in M if, for every mapping I : A → S, if M |=I F for every F ∈ Γ , then M |=I G for some G ∈ Δ. We say that Γ ⇒ Δ is valid in CICL if it is valid in every M.
In Figure 1 we present the rules of the calculus SeqCICL for CICL . As usual, we say that a sequent Γ ⇒ Δ is derivable in SeqCICL if it admits a derivation. A derivation is a tree whose nodes are sequents. A branch is a sequence of nodes Γ1 ⇒ Δ1, Γ2 ⇒ Δ2, . . . , Γn ⇒ Δn, . . . Each node Γi ⇒ Δi is obtained from its immediate successor Γi−1 ⇒ Δi−1 by applying backward a rule of SeqCICL , having Γi−1 ⇒ Δi−1 as the conclusion and Γi ⇒ Δi as one of its premises. A branch is closed if one of its nodes is an instance of axioms, namely (AX ), (AX≥), and (AX⊥), otherwise it is open. We say that a tree is closed if all its branches are closed. A sequent Γ ⇒ Δ has a derivation in SeqCICL if there is a closed tree having Γ ⇒ Δ as a root.
As an example, in Figure 2 we show a derivation in SeqCICL of an instance of the axiom (UNIT). In order to show that the formula α → (A says α) is valid, we build a derivation in SeqCICL for the sequent ⇒ u : α → (A says α).
As an another example, in Figure 3 we show a derivation in SeqCICL of an instance of the axiom (C4).
The calculus SeqCICL is sound and complete for the logic CICL , that is to say a formula F ∈ L is valid in CICL if and only if the sequent ⇒ u : F is derivable in SeqCICL . In order to prove this, we first need to show some basic structural properties of the calculus. First, we introduce the notion of complexity of a labelled formula: Definition 6 (Complexity of a labelled formula cp(F )). We define the complexity of a A labelled formula F as follows: cp (x : A) = 2 ∗ | A |; cp (x −→ y) = 2 ∗ | A | +1; cp (y ≥ x) = 2, where | A | is the number of symbols occurring in the string representing the formula A.
By the above definition, we have that all the rules of SeqCICL introduce in the premise(s) only formulas having a smaller complexity with respect to the formula to which the rule is applied.
Lemma 5 (Height-preserving admissibility of weakening). Given any formula F , if a sequent Γ ⇒ Δ has a derivation of height h, then Γ ⇒ Δ, F and Γ, F ⇒ Δ have a derivation of height h′ ≤ h.
Lemma 6 (Height-preserving label substitution). If a sequent Γ ⇒ Δ has a derivation of height h, then Γ [x/y] ⇒ Δ[x/y] has a derivation of height h′ ≤ h, where Γ [x/y] ⇒ Δ[x/y] is the sequent obtained from Γ ⇒ Δ by replacing all occurrences of the label x by the label y.
(AX) Γ, F ⇒ Δ, F F either x : P,P ∈ ATM or y ≥ x y new Γ, y ≥ x, y : A ⇒ Δ, y : B
Γ ⇒ Δ, x : A → B Γ, y ≥ x ⇒ Δ, y : A, y : B (∨R)
Γ ⇒ Δ, x : A ∨ B y new y new Γ, y ≥ x, y : A ⇒ Δ (¬R)
Γ ⇒ Δ, x : ¬A Γ, y ≥ x, y −A→ z ⇒ Δ, z : B
Γ ⇒ Δ, x : A says B y and z new Γ, x : A says B ⇒ Δ, y ≥ x ⇒ u : A → B Γ, x −A→ y ⇒ Δ, x −B→ y (→ R) Γ, x : A → B ⇒ Δ, y ≥ x Γ, x : A → B ⇒ Δ, y : A Γ, x : A → B ⇒ Δ Γ, x : A → B, y : B ⇒ Δ (→ L) y new Γ, y ≥ x ⇒ Δ, y : A Γ, y ≥ x ⇒ Δ, y : B (∧R) Γ ⇒ Δ, x : A ∧ B Γ, x : A ∧ B ⇒ Δ, y ≥ x Γ, x : A ∧ B, y : A, y : B ⇒ Δ (∧L)
Γ, x : A ∧ B ⇒ Δ Γ, x : A ∨ B ⇒ Δ, y ≥ x Γ, x : A ∨ B, y : A ⇒ Δ Γ, x : A ∨ B ⇒ Δ
Γ, x : A ∨ B, y : B ⇒ Δ (∨L) y ≥ x ⇒ y ≥ x y −A→ w ⇒ y −A→ w
(AX) . . . , y −A→ w, w −A→ z, x : A says (A says α) ⇒ z : α y ≥ x, x ≥ u, y −A→ z, x : A says (A says α) ⇒ z : α x ≥ u, x : A says (A says α) ⇒ x : A says α ⇒ u : (A says (A says α)) → (A says α) Lemma 7 (Height-preserving invertibility of rules). Let Γ ⇒ Δ be an instance of the conclusion of a rule R of SeqCICL , with R different from (EQ). If Γ ⇒ Δ is derivable, then the premise(s) of R is (are) derivable with a derivation of (at most) the same height.
Lemma 8 (Height-preserving admissibility of contraction). If a sequent Γ ⇒ Δ, F, F is derivable in SeqCICL , then there is a derivation of no greater height of Γ ⇒ Δ, F , and if a sequent Γ, F, F ⇒ Δ is derivable in SeqCICL , then there is a derivation of no greater height of Γ, F ⇒ Δ.
Γ ⇒ Δ, F
Γ, F ⇒ Δ Γ ⇒ Δ (cut) where F is any labelled formula. We prove that this rule is admissible in the calculus SeqCICL . The standard proof of admissibility of cut proceeds by a double induction over the complexity of F and the sum of the heights of the derivations of the two premises of (cut), in the sense that we replace one cut by one or several cuts on formulas of smaller complexity, or on sequents derived by shorter derivations. However, in our calculus SeqCICL the standard proof does not work in one case, presented in the proof A of Theorem 3 below, namely the case in which F is a transition formula x −→ y, the left premise is obtained by an application of (EQ) and the right premise is obtained by an application of (C4). Therefore, in order to prove the admissibility of cut for SeqCICL , A A we proceed as follows. First of all, we represent with Γ [xi −→ yi] ⇒ Δ[uj −→ vj ] a sequent containing any number of transitions labelled with the formula A; moreover, if ⇒ u : A → A′ and ⇒ u : A′ → A are derivable, we denote with Γ ⋆ ⇒ Δ⋆ the sequent obtained by replacing any number of transitions labelled with A with the same
A A transitions labelled with A′ in Γ [xi −→ yi] ⇒ Δ[uj −→ vj ]. We prove that cut is admissible by “splitting” the notion of cut in two propositions: Theorem 3. In SeqCICL , the following propositions hold: – (A) If Γ ⇒ Δ, F and Γ, F ⇒ Δ are derivable, so Γ ⇒ Δ, i.e. the rule (cut) is admissible in SeqCICL ;
A A – (B) if (I) Γ [xi −→ yi] ⇒ Δ[uj −→ vj ] is derivable with a derivation of height h, (II) ⇒ u : A → A′ and (III) ⇒ u : A′ → A are derivable, so Γ ⋆ ⇒ Δ⋆ with a derivation of height h′ ≤ h.
Proof. By double mutual induction on the complexity of the cut formula and on the height of the derivation. To prove (A), the induction on the height is intended as usual as the sum of the heights of the premises of the cut inference; to prove (B), the induction on A A the height is intended as the height of the derivation of Γ [xi −→ yi] ⇒ Δ[uj −→ vj ]. We have several cases: • Base for (A): one of the two premises of (cut) is an axiom. To save space, we only present the case in which Γ ⇒ Δ, F is an instance of (AX ) since F ∈ Γ . We have that Γ = Γ ′, F ; the right premise of (cut) is, therefore, Γ ′, F, F ⇒ Δ and, since contraction is admissible (Lemma 8), we have that also Γ ′, F ⇒ Δ, i.e. Γ ⇒ Δ, is derivable. The other cases are omitted to save space.
A A • Base for (B): if Γ [xi −→ yi] ⇒ Δ[uj −→ vj ] is an axiom, so Γ ⋆ ⇒ Δ⋆, since axioms do not involve transition formulas. • Inductive step for (A): we distinguish the following two cases: - the last step of one of the two premises is obtained by a rule in which F is not the principal formula. We further distinguish two subcases: (i) one of the sequents, say Γ, F ⇒ Δ is obtained by the (EQ) rule, where F is not principal. The premises of (EQ) do not contain F , since this rule only involves two transition formulas belonging to Γ and Δ. Therefore, we have a proof of Γ ⇒ Δ by a direct application of (EQ) to it; (ii) the sequent where F is not principal is derived by any rule R, except the (EQ) rule. This case is standard, we can permute R over the cut, i.e. we cut the premise(s) of R and then we apply R to the result of cut. - F is the principal formula in the last step of both derivations of the premises of the cut inference. There are seven subcases: F is introduced a) by (∧R) - (∧L), b) by (∨R) (∨L), c) by (→ R) - (→ L), d) by ( says R) - ( says L), e) by (EQ) on the left and on the right, f) by (EQ) on the left and by (C4) on the right, and g) by (EQ) on the left and by (U nit) on the right. The list is exhaustive. Due to space limitations, here we only present the most interesting case f). We have the following derivation: ⇒ u : A′ → A ⇒ u : A → A′ (1) Γ ′, x −A→′ y ⇒ Δ, x −A→ y
(EQ) Γ ′, x −A→′ y ⇒ Δ (2) Γ ′, x −A→′ y, x −A→ y, x −A→ z, z −A→ y ⇒ Δ Γ ′, x −A→′ y, x −A→ y ⇒ Δ
(C4) (cut) By (2) and Proposition (B), we have a derivation of at most the same height also for
A′ A A′ A′ (2′) Γ ′, x −→ y, x −→ y, x −→ z, z −→ y ⇒ Δ. By Lemma 5, from (1) we have
A′ A′ A′ A a derivation of (1′) Γ ′, x −→ y, x −→ z, z −→ y ⇒ Δ, x −→ y. By cutting (1′) A′ A′ A′ and (2′), we obtain a derivation of Γ ′, x −→ y, x −→ z, z −→ y ⇒ Δ (this cut is eliminable by inductive hypothesis on the height of the derivations), then we can conclude by an application of (C4).
A • Inductive step for (B): we have to consider all possible derivations of Γ [xi −→ yi] ⇒
A Δ[uj −→ vj ]. We only present the most interesting case, namely the one the derivation ends as follows: ⇒ (3) u : A → A′′
⇒ (4) u : A′′ → A Γ [xi −A→ yi], x −A→ y ⇒ Δ[uj −A→ vj ], x −A→′′ y (EQ) We have to show that there is a derivation also for Γ ⋆, x −→ y ⇒ Δ⋆, x −A→′′ y. Since A′ the rule (→ R) is invertible (Lemma 7), since (5) ⇒ u : A → A′ and (6) ⇒ u : A′ → A are derivable, we have derivations also for (5′) x ≥ u, x : A ⇒ x : A′, (6′) x ≥ u, x : A′ ⇒ x : A, and since we have derivations for (3) and (4), also (3′) x ≥ u, x : A ⇒ x : A′′ and (4′) x ≥ u, x : A′′ ⇒ x : A are derivable. By applying the inductive hypothesis of Proposition A on the complexity of the cut formula, we can cut (5′) and (4′) to obtain a derivation of (7) x ≥ u, x : A′′ ⇒ x : A , ′ as well as (6′) and (3′) to obtain a derivation of (8) x ≥ u, x : A′ ⇒ x : A′′. We can conclude as follows: (7) x ≥ u, x : A′′ ⇒ x : A′ ⇒ u : A′′ → A′ (→ R) (8) x ≥ u, x : A′ ⇒ x : A′′ ⇒ u : A′ → A′′ (→ R) Γ [xi −A→ yi], x −A→′ y ⇒ Δ[uj −A→ vj ], x −A→′′ y (EQ) Theorem 4 (Soundness of SeqCICL ). If Γ ⇒ Δ is derivable, then Γ ⇒ Δ is valid in the sense of Definition 5. Theorem 5 (Completeness of SeqCICL ). If Γ ⇒ Δ is valid in the sense of Definition 5, then Γ ⇒ Δ is derivable.
Proof. We prove that the axioms are derivable and that the set of derivable formulas is closed under (MP), (RCEA), and (RCK). In Figure 2 we have shown a derivation of the axiom (UNIT). In Figure 3 we have shown a derivation of the axiom (C4). Derivations for (K) and (TAUT) are omitted for the lack of space. For (MP), suppose we have a derivation for (i) ⇒ x : A and (ii) ⇒ x : A → B. Since weakening is admissible (Lemma 5), we have that also (i′) ⇒ x : A, x : B and (ii′) x : A ⇒ x : A → B, x : B have a derivation in SeqCICL . Since (cut) is admissible (Theorem 3), we can conclude that ⇒ x : B is derivable as follows: . . . , ⇒ x ≥ x, x : B . . . , x : A ⇒ x : A, x : B
. . . , x : B ⇒ x : B x : A → B, x : A ⇒ x : B (→ L) (cut) (i′) ⇒ x : A, x : B (ii′)x : A ⇒ x : A → B, x : B ⇒ x : B x : A ⇒ x : B (cut) For (RCEA), we proceed as follows. As usual, ⊢ A ↔ B is a shorthand for ⊢ A → B and ⊢ B → A. Suppose we have a derivation for ⇒ u : A → B and for ⇒ u : B → A. We have that also ⇒ u : (A says C) → (B says C) has a derivation in SeqCICL (the other half is symmetric): y −C→ z ⇒ y −C→ z y ≥ x, y −C→ z, . . . , z : A ⇒ z : B y ≥ x, y −C→ z, x ≥ u, x : C says A ⇒ z : B (U nit) Completeness of SeqCICL with respect to CICL models of Definition 1 immediately follows from the completeness of the axiomatization of CICL with respect to the semantics, shown in Theorem 2. We have that a formula ϕ ∈ L is valid if and only if the sequent ⇒ u : ϕ has a derivation in SeqCICL . 5
Conclusions We have defined an intuitionistic conditional logic for Access Control ( CICL ) by providing an axiomatization, a Kripke model semantics and a cut-free sequent calculus.
From an axiomatic point of view, the employment of constructive logics for access
control has been put forward by Abadi in [
From a logical point of view, several formal systems have been developed in the
recent years [
In this work, we have proven that the axiomatization of the intuitionistic conditional
logic CICL is sound and complete with respect to the semantics. Moreovoer, we have
provided a cut-free, labelled, sequent calculus for this logic. In CICL , principals are
defined as arbitrary formulas. The generality of the language makes it possible to
formalize, for instance, the so called boolean principals [
The work has been partially supported by Regione Piemonte, Project “ICT4Law - ICT
Converging on Law: Next Generation Services for Citizens, Enterprises, Public
Administration and Policymakers”. Valerio Genovese is supported by the National Research
Fund, Luxembourg. This paper extends [