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 speaks_for R
   E2 speaks_for 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 {s implies s'}} then {A says s'}

 

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

In ABLP we say:

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

      i.e.

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


 

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 {http://example.com/foo corresponds_to E}}
  then  example.com says {http://example.com/foo corresponds_to E}

  whence  http://example.com/foo corresponds_to E
  because  example.com controls {http://example.com/foo corresponds_to E}


 

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=describes
 if  P(S)
   then  P(R)

[ STOP HERE ]


 

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

Controversial axiom:

 if  E corresponds_to R
   then  E speaks_for R

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

(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.

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 x corresponds_to to y 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?