DOC PREVIEW
From Indexed Lax Logic to Intuitionistic Logic

This preview shows page 1-2-17-18-19-35-36 out of 36 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 36 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

From Indexed Lax Logic to Intuitionistic LogicDeepak Garg1Michael Carl Tschantz2January, 2008CMU-CS-07-167School of Computer ScienceCarnegie Mellon UniversityPittsburgh, PA 15213AbstractWe present translations from a logic with indexed lax modalities to first-order intuitionistic logicand intuitionistic linear logic. These translations rely on a continuation passing style encoding forthe lax modalities. We show that our translations preserve provability of formulas.1This author was partially sponsored by the Air Force Research Laboratory under grant no. FA87500720028.The views and conclusions contained in this document are those of the author and should not be interpreted asrepresenting official policies, either expressed or implied, of any sponsoring institution, the U.S. government or anyother entity.2This author was partially sponsored by the Army Research Office through grant number DAAD19-02-1-0389(“Perpetually Available and Secure Information Systems”) to Carnegie Mellon University’s CyLab and by a generousgift from the Hewlett-Packard Corporation. The views and conclusions contained in this document are those ofthe authors and should not be interpreted as representing the official policies, either expressed or implied, of anysponsoring institution, the U.S. government, or any other entity.Keywords: Lax Logic, Affirmations, Logical Transformations1 IntroductionLax logic is a modal logic extending intuitionistic propositional logic with a single modality lax(A) satisfying the following axioms.` A ⊃ A`   A ⊃ A` (A ⊃ B) ⊃ (A ⊃ B)In this report we describe two simple translations of lax logic with multiple modalities: a first-ordertranslation into first-order intuitionistic logic and a linear translation into intuitionistic linear logic.We show that our translations preserve provability. The essence of these translations is a continu-ation passing style (CPS) encoding of the lax modality.Background. In its propositional form, lax logic was introduced by Mendler et al [FM97] as ameans of modeling digital circuits. Subsequently, a first-order version was developed for use inconstraint logic programming [FW97, FMW97]. The semantics and proof theory of lax logic arewell studied [PD01, FM97, How01, BBdP98, GP06, AMdPR01] and the propositional fragmentis decidable [FM97, How01]. Lax logic corresponds (under the Curry-Howard isomorphism) tomonads from functional programming [BBdP98].Our primary interest in lax logic is its application to representing decentralized access-controlsystems where different users, machines, programs, etc (abstractly called principals) request accessto secure resources like files or devices under the control of other principals such as administrators orthe operating system. The policies governing access to resources are formalized as logical formulasin a suitably chosen logic. Access is granted to a resource if a particular proposition such ascan read(Bob, foo.pdf) is provable in the logic from the given policy.A quintessential requirement on a logic of access control is a notion of statements made by aprincipal [ABLP93, LABW92]. For instance, we may want to formalize the following statements inthe access control policy of a file system:- Administrator says Bob can read foo.pdf- Administrator says that any user X can read foo.pdf if X is a member of the group of privilegedusersOne convenient way of formalizing such statements is to introduce for each principal K, a modalityhKiA (read “K says A”) with the intended meaning that K says that A is true. Then the abovestatements can be encoded as follows.- hadministratorican read(Bob, foo.pdf)- hadministratori(∀X. privileged(X) ⊃ can read(X, food.pdf)).Here privileged(X) is a predicate indicating that X is a privileged user and can read(Bob, foo.pdf)means that Bob is allowed to read foo.pdf.There is reasonable flexibility in choosing the logical rules governing the modality hKiA and anumber of proposals have been made [LABW92, ABLP93, Aba03, GP06, Aba06]. For instance the2 operator from modal logic K can be used. However, more recently, an increasingly large number1of proposals [GP06, Aba06, CCD+07, GBB+06, LLFS+07, GA08] have chosen hKiA to be a laxmodality, with the rules described earlier:` A ⊃ hKiA` hKihKiA ⊃ hKiA` hKi(A ⊃ B) ⊃ (hKiA ⊃ hKiB)With these rules, the access control logic becomes an indexed lax logic, with one lax modalityfor every principal. We briefly mention the merits of making hKiA a lax modality, referringthe interested reader to existing work for more details on modeling access control systems in thelogic [LABW92, ABLP93, GP06].- Owing to a well studied proof theory, the notion of proof is well understood for lax logic. Thisis crucial in access control systems that often rely on the existence of proof of a certain propo-sition (like can read(Bob, foo.pdf)) in order to grant access to resources. This is particularlythe case with proof-carrying authorization architectures [AF99, Bau03].- The axiom A ⊃ hKiA forces every principal to state every true statement A. This indicatesthat proof is irrefutable evidence, i.e., if A has a proof, then every principal will believe it.This is not the case in a number of modal logics, such as K.- It is not the case that (hKi⊥) ⊃ ⊥. Thus, individual principals may make inconsistentstatements without making the logic inconsistent. This is important since principals may bemalicious.In this report, we present a translation from an access control logic with lax modalities (calledINLL for INdexed Lax Logic here) to two different logics: first-order intuitionistic logic and intu-itionistic propositional linear logic. We show in each case that the translations preserve provabilityof formulas. In particular, we prove two complementary theorems in each case: soundness, whichstates that a translated formula is provable only if the original formula is, and completeness whichstates the converse.The main motivation for studying these translations is automation of the proof search procedurefor INLL, which is central to implementations of access control systems using the logic. Rather thanprove a formula in INLL (for which theorem provers are not known), one could simply translate itto (say) first-order logic and use a standard theorem prover. Besides automation, our results areinteresting from a theoretical perspective. To the best of our knowledge, these are the first soundand complete translations from lax


From Indexed Lax Logic to Intuitionistic Logic

Download From Indexed Lax Logic to Intuitionistic Logic
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view From Indexed Lax Logic to Intuitionistic Logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view From Indexed Lax Logic to Intuitionistic Logic 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?