Secure Sessions

Examples of sessions

These examples are mentioned in the paper Cryptographic Protocol Synthesis and Verification for Multiparty Sessions.

Each of these examples consists in the presentation of a source file (file '.session') describing the session and links to download any of the nine generated files by our compiler: the '.ml' and '.mli' giving the generated source code of the protocol implementation; the '.ml7' files are the annotated interfaces used for verification; the '.ps' files represent the session graph and its refined versions.

Rpc

The Rpc session is a two-party session between a client 'c' and a webservice 'w' with a typical Query/Reply message flow.

Consider the following session graph:

This session is specified as follows (file Rpc.session):

session Rpc =
  var q : string
  var x : int

  role c = 
    send Query {q,c,w};
    recv Reply {x}

  role w = 
    recv Query {q,c,w} -> 
    send Reply {x}

Ws

The Ws session is a two-party session similar to Rpc but for the possibility of the Webservice to signal an error with a Fault message.

Consider the following session graph:

This session is specified as follows (file Ws.session):

session Ws =
  var q : string
  var x : int

  role c : unit = 
    send Request {c,w,q};
    recv [ Reply {x} | Fault ]

  role w : string =
    recv Request {c,w,q} -> 
    send ( Reply {x} + Fault )

Commit

The Commit session is a two-party session where the client 'c' writes a value in variable 'q' that is only revealed later to 'w'. Once the session is completed, 'w' has the guarantee that the value written initially by 'c' is the same as the one it received later.

Consider the following session graph:

This session is specified as follows (file Commit.session):

session Commit =
  var q : int

  role c : string = 
    send Commit {q,c,w};
    recv Ack ->
    send Reveal {}

  role w : string  = 
    recv Commit {c,w} -> 
    send Ack;
    recv Reveal {q}

Wsn

The Wsn session allows the client 'c' to submit multiple queries to the webservice 'w' by rebinding the variable 'q'.

Consider the following session graph:

This session is specified as follows (file Wsn.session):

session Wsn =
  var q : string
  var x : int

  role c : unit = 
    send Request{c,w,q};
    loop:
    recv [ Reply{x} -> send Extra{q};loop | Fault ]

  role w : string = 
    recv Request{c,w,q} -> 
    loop:
    send ( Reply{x}; recv Extra{q} -> loop + Fault )

Fwd

The Fwd session involves three parties: 'c' tries to send a value 'q' to 'r' through 'w'. In this session 'w' is prevented to alter the value of 'q' written by 'c'.

Consider the following session graph:

This session is specified as follows (file Fwd.session):

session Fwd =
  var q : int

  role c = 
    send Commit {q,c,w,r}

  role w = 
    recv Commit {q,c,w,r} -> 
    send Fwd

  role r =
    recv Fwd {q,c,w,r}

Proxy

The Proxy session involves three parties: 'c' submits a Request to a proxy 'p' and expects a Reply from a webservice 'w'. 'p' can choose two different paths to achieve this goal. One just forwards the request to 'w' who replies; another can trigger a loop of interaction between 'p' and 'w' as they audit the credentials of 'p'.

Consider the following session graph:

This session is specified as follows (file Proxy.session):

session Proxy =
  var q: string (* query *)
  var x: string (* reply *)
  var d: string (* details *)
  var o: string (* objections *)

  role c = 
    send Request {c,p,w,q};
    recv Reply {x}

  role p =
    recv Request {c,p,w,q} ->
    send 
    ( Forward
    + Audit;
      loop:
      recv Details {d} ->
      send ( Retry {o}; loop + Resume ))

  role w =
    recv 
    [ Forward {c,p,w,q} ->
      end:
      send Reply {x}
    | Audit {c,p,w} ->
      loop: 
      send Details {d} ;
      recv [ Retry {o} -> loop | Resume {q} -> end] ]

Login

The Login session illustrates trust and dynamic principal selection: a client 'c' gets the name of a webservice 'w' from a proxy 'p'.

Consider the following session graph:

This session is specified as follows (file Login.session):

session Login =
   var q : string
   var r : int ;

  trusts d < p

  role c = 
    send Login {c,p,d,q};
    recv 
    [ Redirect {w} ->
        send Request{q};
        loop:
        recv [ Reply{r} -> send Extra{q};loop | Fault ]
    | Basicreply {r} ]

  role w = 
    recv Request{c,p,w,q} -> 
    loop:
    send ( Reply{r}; recv Extra{q} -> loop + Fault )

  role p =
    recv Login {p,d,c,q} ->
    send
    ( Redirect {w}
    + Reject )    

  role d =
    recv Reject {p,d,c} -> send Basicreply{r}