logging in or signing up sistla language policy smith Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINTLite Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 52 Category: Entertainment License: All Rights Reserved Like it (0) Dislike it (0) Added: December 23, 2007 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript Language Based Policy Analysis in a SPKI Trust Management System: Language Based Policy Analysis in a SPKI Trust Management System Arun K. Eamani A. Prasad Sistla Univ. of Illinois at ChicagoSPKI/SDSI(Simple Public Key Infrastructure/Simple distributed Security Infrastructure): SPKI/SDSI(Simple Public Key Infrastructure/Simple distributed Security Infrastructure) a mechanism for specification of policy in a distributed access control system Proposed in [EFL+99][EU99] Can be viewed as a trust management systemOur Work: Our Work a language for specification of properties/queries of a policy an algorithm for checking satisfaction of a policy given in the languageOutline of the talk: Outline of the talk SPKI system and policy analysis Related work Language description Algorithms Conclusion SPKI/SDSI System: SPKI/SDSI System Policy specified through certificates or credentials(in short, certs) Two types of certs: authorization certs: Used by administrators to authorize principals to access resources. name certs: used to define groups of users Naming scheme: Naming scheme Principals, resources are identified by their public keys Ex: Kuic : public key for UIC Kuiuc : public key for UIUC I: a set of identifiers e.g. {friends, brothers} Local name(space): a key followed by an identifier Defines a set of principals E.g.: Kjohn friends, Kjohn brothers Name scheme cont’d: Name scheme cont’d Extended names: a key followed by two or more identifiers Kbob friends brothers name: local name or extended name Term: name or key Also called fully qualified name Certificates: Certificates name certs: define a local name Structure: (K, A, S, V) K: key A: identifier S: fully quantified name V: validity time interval Written as rule: K A S Defines that every member of S is a member of K A.Example: Example KBob friend K John KJohnbrother K David KBob friend K Joe friend brother Authorization certs (K, S, D, E, V): Authorization certs (K, S, D, E, V) K: public key S: subject — a fully qualified name D: delegation bit 1: has delegation right 0: no delegation right E: set of authorization rights V: validity time interval Written as: K S when D=1 K S when D=0 Example: Example R KBob KBob K John friend K John friend K Joe K John friend K David K Joe ,K David can access the resource without delegation rights. Rewriting Rules/Tuple Reduction: Rewriting Rules/Tuple Reduction Each name cert/auth cert is considered as a rewriting rule term T1 can be transferred to T2 using the rewriting rules. Example: Example KBob friend K John KJohn brother K David “KBob friend brother” resolves to “K David ” means K David is a member of the group “KBob friend brother” K John can access the resource R if R resolves to K John or K John Policy Analysis : Policy Analysis answering queries and questions about a given policy Can principal K Joe access the resource R? Is principal K Joe a member of “KBob friend brother” ?Related Work: Related Work [JR02]: Jha and Reps use model checking for policy analysis [Aba97]: use logic to model local name space [HvdM01]: use logic for semantics Clarke et al: use certificates chains for proof of compliance Related Work(Cont’d): Related Work(Cont’d) Most policy analysis done for fixed set of properties We propose a general purpose language for specifying properties We give algorithm for checking any propertie specified in the language.Language Description: Language Description FTPL(First order Temporal Policy Language) A policy state: a set of certificates valid at a given time Due to valid intervals, policy state changes over time Suppose the policy has two certs : C1 valid [0 10] C2 valid [5 15]. Defines a sequence of policy states: {C1}, {C1,C2}, {C2}. The first state lasts from 0 to 5 time units, the second from 6 to 10, and the last from 11 to 15 .FTLP feature: FTLP feature FTPL has constraints to reason about a single policy state as well as a sequence of policy states Uses variables and first order quantifiers ranging over principals. i, i Uses temporal operators to specify temporal properties FTPL con’t: FTPL con’t Employs two predicates: Resolve( p, q ): denotes p resolves to q p can be a term q can be a term or a variable Authorize( p, q, d, e): denotes “p authorize q to have the right specified by e” p is a variable or a key q is a variable or a nameFTPL cont’d: FTPL cont’d Quantifiers: i: for all principals i i: for some principal i Temporal Operators: [10,20] : eventually with in time 10 to 20 units from now [10,20] : at all times between 10 to 20 time unites from now : next time Logic connectives: (and), (or), (not), (implication) Examples: Examples authorize(R, KB, 0, {read}) KB has a “read” access right without delegation at the beginning [0, t] authorize(R, KB, 0, {read}) KB has a “read” access right some time before t [0, t] authorize(R, KB, 0, {read}) KB has a “read” access right at all times before t [0, ] ( authorize(R, K1, 0, {write}) authorize(R, K2, 0, {write}) ) K1’ K2 both have write access right at the same time some time in futureUsing quantifiers: Using quantifiers i ( resolve(KBob friend, i ) authorize( R, i, 0, {write}) ) Some friend of Bob has a write access i ( (resolve(KBob friend, i ) authorize( R, i, 0, {write}) ) Every friend of Bob has a write access authorize( R, K2 , 0, {r}) Until[0, ] authorize(R, K1 , 0, {r}) K1 has access right r before K2Example con’t: Example con’t Violation of separation of duty: [0, ] i ( resolve(R1 , i) resolve (R2 , i)) Roles R1, R2 have a common member at some point in time Violation of Containment: [0, ] i ( authorize( P, i, 0, {r}) resolve(R,i) ) There is a principal not a member of R and has “r” access right at some time Queries: Queries authorize( R, i, 0, {r}) Retrieves all principals having “r” access at the beginning [0, t] authorize( R, i, 0, {r}) Retrieves all principals having “r” access at all times up to tEvaluation of the formulas: Evaluation of the formulas Given a certificate system C, and a formula f with k free variables, we compute a relation Rf that has k+1 attributes: In each tuple of Rf , the first k attributes give the values of the free variables and the last attribute gives a set of time intervals when f is satisfied If f has no free variables, then Rf retrieves a set of time intervals during which f is satisfied E.g.: f = authorize(R, i, 0, {r}) Rf : KBob , {[10,20], [30,40]} Kjohn , {[5,10]} Outline of the algorithm: Outline of the algorithm Compute the subformulas of f as set F For each member g in F, in increasing length of g If g is an atomic subformula, compute Rg using an “and-or’’ graph; // the “and-or” graph captures the proofs of compliance in a finite structure; a single fix point computation computes all such Rg else compute Rg using the relations {Rh where h is an immediate subformula of g} Complexity: Complexity O( m2 (n+m)(n+L) + m|f|2 nu(f) ) m: of certs n: of keys L: sum of the length of right hand sides of the certs |f|: length of the formula u(f): of variables in fConclusion and future work: Conclusion and future work Our method can be used for policy analysis and policy audit Implementation ? You do not have the permission to view this presentation. In order to view it, please contact the author of the presentation.
sistla language policy smith Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINTLite Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 52 Category: Entertainment License: All Rights Reserved Like it (0) Dislike it (0) Added: December 23, 2007 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript Language Based Policy Analysis in a SPKI Trust Management System: Language Based Policy Analysis in a SPKI Trust Management System Arun K. Eamani A. Prasad Sistla Univ. of Illinois at ChicagoSPKI/SDSI(Simple Public Key Infrastructure/Simple distributed Security Infrastructure): SPKI/SDSI(Simple Public Key Infrastructure/Simple distributed Security Infrastructure) a mechanism for specification of policy in a distributed access control system Proposed in [EFL+99][EU99] Can be viewed as a trust management systemOur Work: Our Work a language for specification of properties/queries of a policy an algorithm for checking satisfaction of a policy given in the languageOutline of the talk: Outline of the talk SPKI system and policy analysis Related work Language description Algorithms Conclusion SPKI/SDSI System: SPKI/SDSI System Policy specified through certificates or credentials(in short, certs) Two types of certs: authorization certs: Used by administrators to authorize principals to access resources. name certs: used to define groups of users Naming scheme: Naming scheme Principals, resources are identified by their public keys Ex: Kuic : public key for UIC Kuiuc : public key for UIUC I: a set of identifiers e.g. {friends, brothers} Local name(space): a key followed by an identifier Defines a set of principals E.g.: Kjohn friends, Kjohn brothers Name scheme cont’d: Name scheme cont’d Extended names: a key followed by two or more identifiers Kbob friends brothers name: local name or extended name Term: name or key Also called fully qualified name Certificates: Certificates name certs: define a local name Structure: (K, A, S, V) K: key A: identifier S: fully quantified name V: validity time interval Written as rule: K A S Defines that every member of S is a member of K A.Example: Example KBob friend K John KJohnbrother K David KBob friend K Joe friend brother Authorization certs (K, S, D, E, V): Authorization certs (K, S, D, E, V) K: public key S: subject — a fully qualified name D: delegation bit 1: has delegation right 0: no delegation right E: set of authorization rights V: validity time interval Written as: K S when D=1 K S when D=0 Example: Example R KBob KBob K John friend K John friend K Joe K John friend K David K Joe ,K David can access the resource without delegation rights. Rewriting Rules/Tuple Reduction: Rewriting Rules/Tuple Reduction Each name cert/auth cert is considered as a rewriting rule term T1 can be transferred to T2 using the rewriting rules. Example: Example KBob friend K John KJohn brother K David “KBob friend brother” resolves to “K David ” means K David is a member of the group “KBob friend brother” K John can access the resource R if R resolves to K John or K John Policy Analysis : Policy Analysis answering queries and questions about a given policy Can principal K Joe access the resource R? Is principal K Joe a member of “KBob friend brother” ?Related Work: Related Work [JR02]: Jha and Reps use model checking for policy analysis [Aba97]: use logic to model local name space [HvdM01]: use logic for semantics Clarke et al: use certificates chains for proof of compliance Related Work(Cont’d): Related Work(Cont’d) Most policy analysis done for fixed set of properties We propose a general purpose language for specifying properties We give algorithm for checking any propertie specified in the language.Language Description: Language Description FTPL(First order Temporal Policy Language) A policy state: a set of certificates valid at a given time Due to valid intervals, policy state changes over time Suppose the policy has two certs : C1 valid [0 10] C2 valid [5 15]. Defines a sequence of policy states: {C1}, {C1,C2}, {C2}. The first state lasts from 0 to 5 time units, the second from 6 to 10, and the last from 11 to 15 .FTLP feature: FTLP feature FTPL has constraints to reason about a single policy state as well as a sequence of policy states Uses variables and first order quantifiers ranging over principals. i, i Uses temporal operators to specify temporal properties FTPL con’t: FTPL con’t Employs two predicates: Resolve( p, q ): denotes p resolves to q p can be a term q can be a term or a variable Authorize( p, q, d, e): denotes “p authorize q to have the right specified by e” p is a variable or a key q is a variable or a nameFTPL cont’d: FTPL cont’d Quantifiers: i: for all principals i i: for some principal i Temporal Operators: [10,20] : eventually with in time 10 to 20 units from now [10,20] : at all times between 10 to 20 time unites from now : next time Logic connectives: (and), (or), (not), (implication) Examples: Examples authorize(R, KB, 0, {read}) KB has a “read” access right without delegation at the beginning [0, t] authorize(R, KB, 0, {read}) KB has a “read” access right some time before t [0, t] authorize(R, KB, 0, {read}) KB has a “read” access right at all times before t [0, ] ( authorize(R, K1, 0, {write}) authorize(R, K2, 0, {write}) ) K1’ K2 both have write access right at the same time some time in futureUsing quantifiers: Using quantifiers i ( resolve(KBob friend, i ) authorize( R, i, 0, {write}) ) Some friend of Bob has a write access i ( (resolve(KBob friend, i ) authorize( R, i, 0, {write}) ) Every friend of Bob has a write access authorize( R, K2 , 0, {r}) Until[0, ] authorize(R, K1 , 0, {r}) K1 has access right r before K2Example con’t: Example con’t Violation of separation of duty: [0, ] i ( resolve(R1 , i) resolve (R2 , i)) Roles R1, R2 have a common member at some point in time Violation of Containment: [0, ] i ( authorize( P, i, 0, {r}) resolve(R,i) ) There is a principal not a member of R and has “r” access right at some time Queries: Queries authorize( R, i, 0, {r}) Retrieves all principals having “r” access at the beginning [0, t] authorize( R, i, 0, {r}) Retrieves all principals having “r” access at all times up to tEvaluation of the formulas: Evaluation of the formulas Given a certificate system C, and a formula f with k free variables, we compute a relation Rf that has k+1 attributes: In each tuple of Rf , the first k attributes give the values of the free variables and the last attribute gives a set of time intervals when f is satisfied If f has no free variables, then Rf retrieves a set of time intervals during which f is satisfied E.g.: f = authorize(R, i, 0, {r}) Rf : KBob , {[10,20], [30,40]} Kjohn , {[5,10]} Outline of the algorithm: Outline of the algorithm Compute the subformulas of f as set F For each member g in F, in increasing length of g If g is an atomic subformula, compute Rg using an “and-or’’ graph; // the “and-or” graph captures the proofs of compliance in a finite structure; a single fix point computation computes all such Rg else compute Rg using the relations {Rh where h is an immediate subformula of g} Complexity: Complexity O( m2 (n+m)(n+L) + m|f|2 nu(f) ) m: of certs n: of keys L: sum of the length of right hand sides of the certs |f|: length of the formula u(f): of variables in fConclusion and future work: Conclusion and future work Our method can be used for policy analysis and policy audit Implementation ?