theory StatVerif_Security_Device 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 accessibility 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 #j. KU(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 */