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;

 

Central relationship:

 "entity corresponds to resource"

 entity corresponds_to resource   [at current time]

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


 

Content negotiation

 Two entities can correspond to one resource

   E1 corresponds_to R
   E2 corresponds_to R

 (e.g. French and Spanish)

 

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


 

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


 

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'}

 

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> }


 

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>


 

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)


 

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*)

 

Redirection (307)

 R coincides_with S

     means

 S speaks_for R


 

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


 

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}


 

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}} !


 

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?