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

prev - next
Central relationship:

 "entity corresponds to resource"

 entity corresponds_to resource   [at current time]

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

prev - next
Content negotiation

 Two entities can correspond to one resource

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

prev - next
HTTP is authoritative for "corresponds to" for http: URIs

In ABLP we say: controls { corresponds_to E}


  if says { corresponds_to E}
    then corresponds_to E

prev - next
Proxying is valid if the proxy proxies correctly

In ABLP we would say: speaks_for

That is,

  if speaks_for
  and says
	 { says { corresponds_to E}}
  then says { corresponds_to E}

  whence corresponds_to E
  because controls { corresponds_to E}

prev - next
Redirection (307) - define a new predicate.

 R coincides_with S


 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)


prev - next
LEAP: What might we do if we treat entities and resources are ABLP

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

prev - next
Redirection (307)

 R coincides_with S


 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

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}

prev - next

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