sistla language policy

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 Chicago

SPKI/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 system

Our Work: 

Our Work a language for specification of properties/queries of a policy an algorithm for checking satisfaction of a policy given in the language

Outline 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 name

FTPL 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 future

Using 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 K2

Example 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 t

Evaluation 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 f

Conclusion and future work: 

Conclusion and future work Our method can be used for policy analysis and policy audit Implementation ?