CSE394: Security Policy Frameworks
	       Scott Stoller, 11oct2005
     Cassandra API Operations: requestCredential

Pseudo-code for other API operations is in
my Trust Management Tutorial slides.

S: the current location, i.e., the policy owner.

Cassandra's definition of requestCredential:

e: requestCredential(iss.p(args) <- cReq)
if iss=S then
  // cAllow is the allowed part of the request
  cAllow = result of query 
    S.canReqCred(e, iss.p(args)) <- cReq
  // cResult is the true part of cAllow.
  cResult = result of query S.p(args) <- cAllow
  if cResult != false then
    return [S.p(args) <- cResult] signed by S
  else return null
else // request is for a foreign credential at S
  // cAllow is the allowed part of the request
  cAllow = result of query
    S.canReqCred(e, p.iss(args)) <- cReq
  creds = emptyset
  for each credential (iss.p(args) <- c) at S
    // if c is part of cAllow, then include this 
    // credential in the result.
    if (c implies cAllow)
      insert this credential in creds
  return creds

Example:
// Server S allows e to get credentials for his 
// own connections to all servers.
canReqCred(e, e'.canConnect(e,port)) <- true
// Server S is caching a credential for Joe from S1
S1.canConnect(Joe,port) <- 1024 <= port <= 2048.


Joe: requestCredential(S1.canConnect(Joe,port)) <- port < 1080

With Cassandra's definition for requestCredential, 
cAllow = port < 1080.  for the credential with 
c = 1024 <= port <= 2048, (c implies cAllow) is false, 
so return empty set to Joe

Revised definition of requestCredential:

e: requestCredential(iss.p(args) <- cReq)
if iss=S then
  // cAllow is the allowed part of the request
  cAllow = result of query 
    S.canReqCred(e, iss.p(args)) <- cReq
  // cResult is the true part of cAllow.
  cResult = result of query S.p(args) <- cAllow
  if cResult != false then
    return [S.p(args) <- cResult] signed by S
  else return null
else // request is for a foreign credential at S
  // cAllow is everything e is allowed to know 
  // about iss.p(args), possibly more than e requested.
  cAllow = result of the query 
    S.canReqCred(e, iss.p(args)) <- true
  creds = emptyset
  for each credential (iss.p(args) <- c) at S
    // if e is allowed to know c, 
    // and c overlaps with the request,
    // then include this credential in the result.
    if (c implies cAllow) and (c and cReq != false)
      insert this credential in creds
  return creds

Example (continued):
With this definition of requestCredential, cAllow = true.
for the above credential, we check (c implies cAllow) and 
(c and cReq != false).  Both ar true, so we return this 
credential.