theory CSF11_RunningExample begin

text{* Running example from:

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.

Modeler: Simon Meier
Date:    June 2012
Status:  Working

*}

builtins: hashing, asymmetric-encryption, signing

// TPM PCR model
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 auth. id. key
    ]


// Disabled, as the protocol is not secure under reboots.
// TODO: Check that we can find the attack.
//
// Note that we miss the attack, as we do not consider collapsing different
// PCR_Unbind nodes. In order to find this attack, we would require to
// introduce strongly different node variables.
//
// rule PCR_Reboot:
//     [ PCR(x) ] --> [ PCR('pcr0') ]  // reset the PCR to 'pcr0'

rule PCR_Extend:
    [ PCR(x)
    , In(y)
    ]
  --[ PCR_Extend(x,y,h(x,y))
    ]->
    [ PCR(h(x,y))
    ]

rule PCR_CertKey:
    [ !AIK(aik)
    , !KeyTable(x, sk)
    ]
  --[ PCR_CertKey_Inst(x)
    ]->
    [ Out(sign{'certkey', x, pk(sk)}aik) ]

rule PCR_Unbind:
    [ PCR(x)
    , !KeyTable(x, sk)
    , In( aenc{m}pk(sk) )
    ]
  --[ PCR_Unbind(x,sk,m)
    ]->
    [ PCR(x)
    , Out(m) ]

// Alice
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)
    ]

// Keytable
rule MkKey:
    // Fr(<'MkKey',$a>)  // register at most one key per public constant
    [ Fr(~ska) ]
    -->
    [ !KeyTable(h('pcr0',$a), ~ska) ]

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

lemma Unbind_PCR_Value [reuse, use_induction]:
    "All x sk m #i.
        PCR_Unbind(x, sk, m) @ i
        ==>
        ( (Ex aik #j.     PCR_Init(x, aik) @ j  )
        | (Ex y xPrev #j. PCR_Extend(xPrev,y,x) @ j)
        | (Ex #i #j. UniqueInit() @ j & UniqueInit() @ i & not (#i = #j))
        )
    "

lemma secrecy:
  " ( (All #i #j. UniqueInit() @ j & UniqueInit() @ i ==> #i = #j)
    & (All t #e. Ineq(t,t) @ e ==> F)
    ) ==>
    not( (Ex s0 s1 #i #d0 #d1.
             Secrets(s0, s1) @ i
           & K(s0) @ d0
           & K(s1) @ d1
       ) )"







end