# Rules for access in imaginary access control situations
#
#  This is an example of all the processing done by a
#  digital-signatue-aware inference engine in validating a
#  request for access to a member access page.
# 
#  This is simplified, of course, but the whole thing is very straightforward.
#  Enhancements would be to:
#   - put expiry dates in certificates
#   - do a revokation check back to a signed revokation list
#   -  
# 
@prefix root: <#> .
@prefix : <#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix os: <http://www.w3.org/2000/10/swap/os#> .
@prefix acc: <http://www.w3.org/2000/10/swap/test/crypto/acc.n3#>.
@prefix crypto: <http://www.w3.org/2000/10/swap/crypto#> .
@prefix string: <http://www.w3.org/2000/10/swap/string#> .


<> :description <http://www.w3.org/2002/Talks/04-sweb/slide22-1.html>.

# Notes.  This uses two levels, request and credentials (certificate)
#        It would have been even simpler in fact to declare recursively but
#        would have been open to denial of service by very long chains

@forAll :d, :F, :G, :k, :k2, :k3, :kp, :x, :request, :sig, :str, :y , :z , :q .

# The rule of access.
#
#  acc:requestSupportedBy means that it correctly claimed to be
#        signed by the given key.

{
    :request acc:forDocument :d;
             acc:requestSupportedBy :k.

    []       acc:certSupportedBy :k2;    # Certificate
             log:includes { :k a acc:RequestKey }.

    []       acc:certSupportedBy [a acc:MasterKey];    # Certificate
             log:includes { :k2 a acc:MemberKey }.

} => { :request a acc:GoodRequest }.

#  What is a Master key?
#
#  (we could just put in the text here)

{ <access-master.public> log:semantics [
        log:includes {:x a acc:MasterKey}]
} log:implies {:x a acc:MasterKey}.


#  What do we belive is a request?
#  We trust the command line in defining what is a request.

{  "1"!os:argv!os:baseAbsolute^log:uri log:semantics :F.
   :F log:includes { :str acc:endorsement[acc:signature :sig; acc:key :k]}.
   :k crypto:verify ([is crypto:md5 of :str] :sig).
   :str log:parsedAsN3:G } log:implies { :G acc:requestSupportedBy :k }.

#  What do we believe from a signed request?
#   - what it says it is asking for.
#   - what it quotes as credentials
#  It could actually enclose a copy of the credentials inline,
#  but here we use the web.  A credential is a document which
#  provides evidence in support of the request.

{:G acc:requestSupportedBy :k; log:includes {[] acc:forDocument :d}} log:implies {:G acc:forDocument :d}.

{:G acc:requestSupportedBy :k; log:includes {[] acc:credential :d}} log:implies {:G acc:credential :d}.

# What do we belive from a signed credential?
#
# In this case, just note that a key supports the signed formula.
# The fact of this support is used in the access rule above.
# We don't actually beleive everything the certificate says.

{  [] acc:credential [ log:semantics :F ].
   :F log:includes { :str acc:endorsement[acc:signature :sig; acc:key :k]}.
   :k crypto:verify ([is crypto:md5 of :str] :sig).
   :str log:parsedAsN3 :G } log:implies { :G acc:certSupportedBy :k }.