StatVerif_Example1.spthy

theory StatVerif_Example1 begin

/*
   Protocol:    Simple security device (Example 1 from [1])
   Modeler:     Simon Meier
   Date:        May 2012

   Status:      working

   This is the simple security device example presented in Section V.A of the
   following paper.

   [1] M. Arapinis, E. Ritter and M. Ryan. StatVerif: Verification of Stateful
   Processes. In CSF'11. IEEE Computer Society Press, pages 33-47 , 2011.

   It models a hardware device that stores both a private key and a
   configuration register that can be set to 'left' for decrypting the first
   component of tuples encrypted using the device's public key and 'right' for
   decrypting the second component of tuples encrypted using the device's
   public key. Alice uses such a device to encrypt tuples such that Bob
   can access either all their first components or all their second
   components, but never both.

   Note that in contrast to [1], we allow the creation of an unbounded number
   of devices. We also verify both the accessability of left and right
   components, as well as their exclusivity. The source code of the model
   from [1] is attached at the end of this file.

*/

builtins: asymmetric-encryption


// Create a new device. It stores the private key and publishes the
// corresponding public key.
rule NewDevice:
    [ Fr(~sk)  // We let the key identify the device.
    ]
  -->
    [  UnconfiguredDevice(~sk)
    , !DevicePublicKey(pk(~sk))
    ,  Out(pk(~sk))
    ]

// Alice can use any public key associated to such a hardware security device
// for publishing messages with exclusive access.
rule Alice:
    [  Fr(~x)
    ,  Fr(~y)
    , !DevicePublicKey(key)
    ]
  --[ Exclusive(~x,~y) ]->
    [ Out( aenc{~x,~y}key )
    ]

// Unconfigured devices can be configured exactly once.
rule ConfigureDevice:
    [ UnconfiguredDevice(sk), In(config) ]
    -->
    [ !ConfiguredDevice(sk, config) ]

// Devices configured to 'left' can be used to decrypt the first component of
// messages encrypted using the device's public key.
rule UseLeftDevice:
    [ !ConfiguredDevice(sk, 'left'), In(aenc{x,y}pk(sk)) ]
  --[ Access(x) ]->
    [ Out(x) ]

// Devices configured to 'right' can be used to decrypt the second component of
// messages encrypted using the device's public key.
rule UseRightDevice:
    [ !ConfiguredDevice(sk, 'right'), In(aenc{x,y}pk(sk)) ]
  --[ Access(y) ]->
    [ Out(y) ]


// As we use a backwards search, we must specify the possible structure of
// messages sent in 'UseLeftDevice' and 'UseRightDevice' precise enough such
// that we can solve all chain constraints starting from the sent message. We
// therefore log the message being accessed and relate it to its possible
// origins: known to the intruder in an earlier step or part of an exclusive
// message generated by 'Alice'. Typing lemmas are proven by induction and
// incorporated in the case distinction precomputation.
lemma types [typing]:
  "All m #i. Access(m) @ i ==>
      (Ex f #j. KU(f,m) @ j & j < i)  // Make use of the KU-facts logged
                                      // by the construction rules.
    | (Ex x #j. Exclusive(x,m) @ j)
    | (Ex y #j. Exclusive(m,y) @ j)
  "

// Check that there is some trace where the intruder knows the left message of
// an exclusive message-tuple. In contrast to the typing lemma, we use the
// standard 'K'-fact, which is logged by the built-in 'ISend' rule.
lemma reachability_left:
  exists-trace
  "Ex x y #i #j. Exclusive(x,y) @i & K(x) @ j"

lemma reachability_right:
  exists-trace
  "Ex x y #i #k. Exclusive(x,y) @i & K(y) @ k"

// Check that exclusivity is maintained
lemma secrecy:
  "not(Ex x y #i #k1 #k2.
         Exclusive(x,y) @i & K(x) @ k1 & K(y) @ k2
      )
  "

end

/* StatVerif source code of the original model from [1].

fun pair/2.
fun aenc/3.
fun pk/1.
free left.
free right.
free init.
free c.

reduc
    projl(pair(xleft, xright)) = xleft;
    projr(pair(xleft, xright)) = xright;
    adec(u, aenc(pk(u), v, w)) = w.

query
    att:vs,pair(sl,sr).

let device =
    out(c, pk(k)) |
    ( ! lock(s); in(c, x); read s as y;
        if y = init then
            (if x = left then s := x; unlock(s)
            else if x = right then s := x; unlock(s))  ) |
    ( ! lock(s); in(c, x); read s as y; let z = adec(k, x) in
        let zl = projl(z) in
        let zr = projr(z) in
        ((if y = left then out(c, zl); unlock(s)) |
         (if y = right then out(c, zr); unlock(s)))).

let user =
    new sl; new sr; new r;
        out(c, aenc(pk(k), r, pair(sl,sr))).

process
    new k; new s; [s |-> init] | device | ! user

*/