next

How to prove correctness of an HTTP proxy, cache, API, or theory?

 8.2.1. 200 OK

    The request has succeeded.  The information returned with the
    response is dependent on the method used in the request, for example:

    GET  an entity corresponding to the requested resource is sent in the
       response;

 
prev - next

Central relationship:

 "entity corresponds to resource"

 entity corresponds_to resource   [at current time]

 HTTP exchange: GET URI / 200 entity
   means
entity corresponds_to <URI>


 
prev - next

Content negotiation

 Two entities can correspond to one resource

   E1 corresponds_to R
   E2 corresponds_to R

 (e.g. French and Spanish)

 
prev - next

Caching is enabled by knowledge of lifetime

 corresponds_during(entity, resource, t1, t2)

   Last-modified: t1
   Expires: t2

   if t1 <= current time < t2 then
      entity corresponds_to resource


 
prev - next

Tool: ABLP logic
 - proving crypto protocols
 - authorization / access control

 Calculus of principals + modal 'says' logic

 A principal P says a statement s.

 "P says s"

   similar to: P authorizes s
               P is responsible for s
               P can be held to s


 
prev - next

ABLP logic summary

Principal: person, server, channel, document, ...

 A speaks_for B
   {A says s} => {B says s}

 A controls s
   {A says s} => s

 A|B  'A quoting B', 'A pretending to be B'
   A|B says s  iff  A says {B says s}

Logic works under 'says'
 if {A says s} and {A says t} then {A says s and t}     (and vice versa)
 if {A says s} and {A says {s implies s'}} then {A says s'}

 
prev - next

HTTP is authoritative for "corresponds to" for http: URIs

In ABLP we say:

  example.com controls {E corresponds_to <http://example.com/foo> }

      i.e.

  if  example.com says {E corresponds_to <http://example.com/foo> }
    then   {E corresponds_to <http://example.com/foo> }


 
prev - next

Proxying is valid if the proxy proxies correctly

In ABLP we would say:

  proxy.example.com speaks_for example.com

That is,

  if  proxy.example.com speaks_for example.com
  and  proxy.example.com says
	 {example.com says {E corresponds_to <http://example.com/foo>}}
  then  example.com says {E corresponds_to <http://example.com/foo>}

  whence  E corresponds_to <http://example.com/foo>


 
prev - next

Redirection (307) - define a new predicate.

 R coincides_with S

     means

 if  E corresponds_to S
   then  E corresponds_to R

 and perhaps similarly for other properties P such as P=described_by Q
 if  P(S)
   then  P(R)


 
prev - next

LEAP: What might we do if we treat entities and resources as ABLP
principals?

That is, suppose we add this controversial axiom:

 if  E corresponds_to R
   then  E speaks_for R

 i.e. if  E says s  then  R says s

What follows?

(but speaks_for is not *sufficient*)

 
prev - next

Redirection (307)

 R coincides_with S

     means

 S speaks_for R


 
prev - next

Content negotiation

 Two entities can correspond to one resource

   E1 speaks_for R
   E2 speaks_for R

 (e.g. French and Spanish)

 If entities disagree on what they say, the resource is incoherent:

   if E1 says s, and E2 says t, and (s and t) = false
     then R says false


 
prev - next

httpRange-14

The domain of "says" is principals.
Non-principals don't say anything.

Therefore non-principals don't 200.

 E corresponds_to R   (200)
 E speaks_for R

 if  E says s  then   R says s
 if  R doesn't say any s  then E doesn't (mustn't) say any s

 {E says s} is inconsistent with not {R says s}


 
prev - next

httpRange-14

Aboutness isn't sufficient:

   {E is_about R} does not imply {E speaks_for R}

   e.g. one might have
     {s is_about R} and {E speaks_for R}
     but not  {E says s}
     or even  {E says {not s}} !


 
prev - next

What else does E corresponds_to R imply?

  Limitations on what can be corresponded to?
    E.g. does Pat Hayes's page correspond to Pat?

  Limitations on what subsetting is allowed?
    E.g. does the empty entity correspond to every resource?