theory TPM_Exclusive_Secrets begin

/*
    Protocol: Running example from [1]
    Modeler: Simon Meier
    Date:    September 2012
    Status:  Working

    [1] Stephanie Delaune, Steve Kremer, Mark D. Ryan, Graham Steel, "Formal
    Analysis of Protocols Based on TPM State Registers," csf, pp.66-80, 2011
    IEEE 24th Computer Security Foundations Symposium, 2011.

    The goal of this example is to verify that the adversary cannot exploit
    his TPM to simultainously access the two secrets that were encryped
    exclusively by Alice.

    Note that we could easily model multiple PCR's, if required.

*/

builtins: hashing, asymmetric-encryption, signing

// TPM Model with support for a single PCRs
///////////////////////////////////////////

rule PCR_Init:
    [ Fr(~aik)          // Authentication identity key
    ]
  --[ PCR_Init('pcr0',~aik)
    , UniqueInit()      // For removing traces that have multiple initializations
    ]->
    [ PCR('pcr0')       // the initial PCR value is 'pcr0'
    , !AIK(~aik)        // the auth. id. key is persistent
    , Out(pk(~aik))     // publish the public key of the attest. ident. key
    ]


// Disabled, as the protocol is not secure under reboots.
//
// Note that we miss the attack, as we do not consider collapsing different
// PCR_Unbind nodes by default. The general construction would require
// distinctness constraints on temporal variables. We can however simulate it
// by proving a simple case distinction lemma with a 'reuse' attribute, as
// demonstrated below.
//
// rule PCR_Reboot:
//    [ PCR(x) ] --> [ PCR('pcr0') ]  // reset the PCR to 'pcr0'

// Extending the PCR register with the value 'y'
rule PCR_Extend:
    [ PCR(x) , In(y) ] --[ PCR_Extend(x,y,h(x,y)) ]-> [ PCR(h(x,y)) ]

// Create a fresh  key that is bound to 'pcr0' extended with a public
// constant.
rule PCR_CreateKey:
    [ Fr(~ska) ] --> [ !KeyTable(h('pcr0',$a), ~ska) ]

// Certifying a key using the TPM's Attestation Identity Key (AIK)
rule PCR_CertKey:
    [ !AIK(aik)
    , !KeyTable(x, sk)   // Any key in the keytable can be certified.
    ]
  --[ PCR_CertKey_Inst(x)
    ]->
    [ Out(sign{'certkey', x, pk(sk)}aik) ]

// Keys in the keytable are bound to a fixed PCR value. If this value, agrees
// with the actual PCR value, then the TPM can be used to decrypt messages
// encrypted with these keys.
rule PCR_Unbind:
    [ PCR(x)
    , !KeyTable(x, sk)
    , In( aenc{m}pk(sk) )
    ]
  --[ PCR_Unbind(x,sk,m)
    ]->
    [ PCR(x) , Out(m) ]

// Alice generates two secrets and accepts two *different* keys signed by the
// TPM to provide exlusive access to them. We are a bit lazy here and use
// pattern matching for the signature verification.
rule Alice_Init:
    [ Fr(~s0)
    , Fr(~s1)
    , !AIK(aik)
    , In(sign{'certkey', x0, pk0}aik)
    , In(sign{'certkey', x1, pk1}aik)
    ]
  --[ InEq(x0, x1)
    , Secrets(~s0,~s1)
    ]->
    [ Out(aenc{~s0}pk0)
    , Out(aenc{~s1}pk1)
    ]



// Axioms; i.e., restrictions on the set of traces of interest
//////////////////////////////////////////////////////////////

axiom UniqueInit_unique:
  " All #i #j. UniqueInit() @ j & UniqueInit() @ i ==> #i = #j "

axiom Ineq_checks_succeed:
  " All t #e. InEq(t,t) @ e ==> F "


// Security Properties
//////////////////////


// A type invariant characterizing the values that can be learned using the
// TPM to Unbind (i.e., decrypt) messages.
lemma types [typing]:
  " (All m d1 d2 #i. PCR_Unbind(d1, d2, m) @ i ==>
        (Ex #j.   KU(m) @ j & j < i)
      | (Ex s #j. Secrets(m, s) @ j)
      | (Ex s #j. Secrets(s, m) @ j)
    )
  "

// Characterizing the unbinding operation. This is the key lemma. It allows us
// to jump backwards to smaller values of the PCR register during reasoning.
lemma Unbind_PCR_charn [reuse, use_induction]:
    "All x sk m #i.
        // If the key 'sk' bound to PCR value 'x' is used to extract the body
        // 'm' of an encryption, then
        PCR_Unbind(x, sk, m) @ i
        ==>
        // 'x' is the initial PCR value
        ( (Ex aik #j.     PCR_Init(x, aik) @ j  )
        // or it was the result of an extension.
        | (Ex y xPrev #j. PCR_Extend(xPrev,y,x) @ j)
        )
    "

// Uncomment to perform case distinctions on the identity of different
// PCR_Unbind nodes. This is required to find the attack when using reboots.
/*
lemma PCR_Unbind_case_distinctions [reuse]:
  "All d11 d21 m1 #i1 d12 d22 m2 #i2.
      PCR_Unbind(d11, d21, m1) @ i1
    & PCR_Unbind(d12, d22, m2) @ i2
    ==>
      (#i1 = #i2) | not(#i1 = #i2)
  "
*/

// The desired security property
lemma exclusive_secrets:
  " not(Ex s0 s1 #i #d0 #d1.
           Secrets(s0, s1) @ i
         & K(s0) @ d0
         & K(s1) @ d1
       )"

// Sanity check: both secrets can be accessed individually.
lemma left_reachable:
  exists-trace
  " Ex s0 s1 #i #j.  Secrets(s0, s1) @ i & K(s0) @ j "

lemma right_reachable:
  exists-trace
  " Ex s0 s1 #i #j.  Secrets(s0, s1) @ i & K(s1) @ j "


end