Official LSV Web Site
Some verifications of protocols based on TPM state registers
In a Horn-clause-based framework, we analyse security protocols that use platform configuration registers (PCRs),
which are registers for maintaining state inside the Trusted Platform Module (TPM). In our model, the PCR state space
is unbounded, and a naive analysis using ProVerif (see the files provided below) or SPASS does not terminate.
To address this, we extract a set of instances of the Horn clauses of our model, for which ProVerif does terminate on our examples.
We prove the soundness of this extraction process: no attacks are lost, that is, any query derivable in the more general set of
clauses is also derivable from the extracted instances (see
here for more details about the soundness of this extraction process).
To show the effectiveness of our framework, we apply it to automatic analysis of two case
studies: a simplified version of Microsoft Bitlocker, and the digital envelope protocol
that allows a user to choose whether to perform a decryption, or to verifiably renounce the ability to perform the decryption.
An introductory example
Description. Assume that Alice has two secrets s1 and s2. The protocol should ensure that
- Bob can learn one of the secrets, but not both.
- Alice commits to the secrets before knowing Bob's choice, i.e. Alice cannot change the secrets according
to Bob's decision.
- Once Alice has committed to the secrets, Bob can open
one of them without any interaction with or help from Alice.
Designing such a protocol using a TPM is rather easy. For sake of simplicity, we assume
that two key pairs (s1, pk(s1)) and (s2, pk(s2)) are already loaded in the TPM: one of them is locked to
h(u0,a1), i.e. the initial PCR value u0 which has been extended with the constant a1, whereas the other key is locked to h(u0,a2).
By using a TPM command called CertifyKey, Bob can obtain certificates for these keys and their lock values.
When Alice receives these certificates, she uses the first public key pk(k1) to encrypt s1 and the second public key pk(k2) to encrypt
s2 and sends both ciphertexts to Bob. If Bob decides to open the first secret, he extends the PCR with a1
and uses a TPM command called Unbind to decrypt the first ciphertext. Similarly, if Bob decides to open
the second ciphertext, he extends the PCR with a2. Because an extension of a PCR cannot be undone, Bob is indeed unable to retrieve both secrets.
A simplified version of the Bitlocker protocol
Description.
This is a "trusted boot" protocol for use with full disk encryption.
It is based on the protocol used in Microsoft Bitlocker, though we make several simplifications to the protocol. Roughly,
when the machine boots, a segment of ROM code called the pre-bios runs. It measures the bios, and extends the measurement into the
PCR. The correct bios will also measure the loader and extend that
into the PCR. An incorrect bios can do whatever it likes. The
correct loader will retrieve the volume master key (VMK), extend "deny" into the PCR, decrypt the OS, and load it. An incorrect
loader can do whatever it likes.
An attacker can replace components such as the BIOS and the bootloader, but in doing so he destroys
the ability to achieve the correct boot state, and the VMK should remain inaccessible.
Our security property is posed as the rechability of a state in which the attacker knows the volume master key VMK (the PCR may have any value).
The envelope protocol
Description.
We analyse the envelope protocol which allows Alice to provide digital data to Bob
in such a way that Bob has only one of two possible actions available to him:
- He can access the data without any further action from Alice.
- Alternatively, he can revoke his right to access the data, and in this case he is able to prove to Alice that he did not and can no longer obtain access to the data.
Our security property is posed as the reachability of a state in which the attacker
knows both Alice's secret and a certificate showing that he denied himself the secret by extending deny into the PCR.
ProVerif confirms that this situation is not reachable.