theory TPM_Envelope begin

text{* Envelope protocol example from:

[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.

Modeler: Simon Meier
Date:    June 2012
Status:  No automatic proof (interactive proof possible)

Note that this model incorporates an arbitrary number of reboots, which is an
open problem in [1]. The verification relies on the construction that we track
all writes to the PCR-fact using the additional PCR_Write-fact. This allows us
then to descend in the hash chain by solving PCR_Write-premises.

*}

builtins: signing, asymmetric-encryption, hashing

// TPM platform configuration register (PCR) model
// Here, we model only one PCR. Modelling multiple PCR's can be done by
// parametrizing their facts on an additional term used to identify them.
rule PCR_Init:
    [ Fr(~aik)             // Authentication identity key
    ]
  --[
      PCR_Init()           // Used in property to ensure at most one initialization
    , PCR_Write('pcr0')
    ]->
    [ PCR('pcr0')          // the initial PCR value is 'pcr0'
    , PCR_Write('pcr0')    // We also track the writes.
    , !AIK(~aik)           // the auth. id. key is persistent
    , Out(pk(~aik))        // publish the public key of the auth. id. key
    ]

// reset the PCR to 'pcr0'
rule PCR_Reboot:
    [ PCR(x)
    , PCR_Write(x)
    ]
  --[ PCR_Write('pcr0')
    ]->
    [ PCR_Write('pcr0')
    , PCR('pcr0')
    ]

// Extend the hash-chain in the PCR
rule PCR_Extend:
    [ PCR_Write(x)       // Get write access
    , PCR(x)             //
    , In(y)              // The adversary can present any value.
    ]
  --[ PCR_Write(h(x,y))
    ]->
    [ PCR(h(x,y))
    , PCR_Write(h(x,y))
    ]

// Certify a key together with the value it is locked to.
rule PCR_CertKey:
    [ !AIK(aik)
    , !KeyTable(lock, sk)
    ]
  --[ ]->
    [ Out(sign{'certkey', lock, pk(sk)}aik)
    ]

// Quote the current value of the PCR
rule PCR_Quote:
    [ PCR(x)
    , !AIK(aik)
    ]
  --[ PCR_Read(x)
    ]->
    [ Out(sign{'certpcr', x}aik)
    , PCR(x)
    ]

// Decrypt a message encrypted with a key locked to the CURRENT value of the
// PCR.
rule PCR_Unbind:
    [ PCR(x)
    , !KeyTable(x, sk)
    , In( aenc{m}pk(sk) )
    ]
  --[ PCR_Unbind(x,sk,m)
    , PCR_Read(x)
    ]->
    [ PCR(x)
    , Out(m) ]

// Alice

// Alice starts by communicating with Bob's PCR to setup a unique root ~n in
// the hash-chain for the following envelope protocol.
rule Alice1:
    [ Fr(~n)
    , PCR(x)
    , PCR_Write(x)
    ]
  --[ PCR_Write(h(x,~n))
    ]->
    [ PCR(h(x,~n))
    , PCR_Write(h(x,~n))
    , Alice1(~n)
    ]

// Bob sends Alice a certified key locked to the value
//   h(h('pcr0',n),'obtain')
// to obtain a secret in an envelope. Note that we only allow for one session
// per reboot as [1].
rule Alice2:
    [ Alice1(n)
    , Fr(~s)
    , !AIK(aik)
    , In(sign{'certkey', h(h('pcr0',n),'obtain'), pk}aik)
    ]
  --[ Secret(~s)
    ]->
    [ Out(aenc{~s}pk)
    , Alice2(n,~s)
    ]

// Bob can use the PCR to prove to Alice that he didn't access the secret.
rule Alice3:
    [ Alice2(n,s)
    , !AIK(aik)
    , In(sign{'certpcr', h(h('pcr0',n),'deny')}aik)
    ]
  --[ Denied(s) ]->
    []

// We use the adversary to simulate Bob. He uses ordinary message deduction
// and it can create keys locked to specific values of the PCR.
rule CreateLockedKey:
    [ PCR(x)
    , Fr(~sk)
    , In(lock) // multiple keys can be locked to the same PCR value.
    ]
  --[ PCR_Read(x)
    ]->
    [ PCR(x)
    , !KeyTable(h(x,lock), ~sk)
    , Out(pk(~sk))
    ]

// Automatically proven
lemma types [typing]:
    // Values created by the PCR_Unbind rule
  " (All m d1 d2 #i. PCR_Unbind(d1, d2, m) @ i ==>
        (Ex f #j. KU(f,m) @ j & j < i)
      | (Ex #j. Secret(m) @ j)
    )
  "

// Automatically proven
lemma PCR_Write_charn [reuse, use_induction]:
    // Values read from the PCR have been written to it beforehand.
  " (All x #i. PCR_Read(x) @ i ==>
      (Ex #j. PCR_Write(x) @ j)
    )
  "

// Assuming that there is at most one instance of the PCR,
// the adversary (playing Bob) must not know a secret that Alice created and
// thinks that access to it was denied.
//
// Currently, we have to construct its proof manually. The key argument relies
// on following the PCR_Write-premises once their presence has been
// established via the PCR_Write_charn lemma.
lemma reachable_Denied:
  "(All #i #j. PCR_Init() @ i & PCR_Init() @ j ==> #i = #j)
   ==>
   not(Ex s #i #j #k. Secret(s) @ i & Denied(s) @ j & K(s) @ k)"


end