Official LSV Web Site
Some verifications on the Trusted Platform Module
This page describes some verifications that have been done with the tool
ProVerif,
an automatic cryptographic protocol verifier in the formal model (so called Dolev-Yao model).
See the
following paper for more details.
Our methodology was to first study some core key management commands
in isolation in order to analyse the weakness of each command.
Then we carried
out a verification where we consider the commands CertifyKey, CreateWrapKey, LoadKey2, and
UnBind together. We consider the fixed version of each of these commands
and we show in Verification 10 that the security properties are
satisfied for a scenario that allows:
- an attacker to load his own keys inside the TPM, and
- an honest user to use the same authdata for different keys.
In our first six verifications, we model the command CertifyKey in
isolation. Then, in Verifications 7-9, we model the command CreateWrapKey
only. Lastly, in Verification 10, we consider a model where the
commands CertifyKey, CreateWrapKey, LoadKey2, and Unbind are taken into account. In all
verifications, the security properties under test are the correspondence
properties explained above.
Verification 1.
We consider a configuration with
two keys loaded inside the TPM.
We assume that the attacker does not have his own key
loaded onto the device.
ProVerif immediately discovers an attack that comes from the fact that the command
involved two keys and the attacker can easily swap the role of these two keys.
The two correspondence properties under study are not satisfied.
File available
here .
Verification 2.
We patch the command CertifyKey by considering two different tags for the
two different hmacs. ProVerif is now able to prove the
two correspondence properties.
File available
here .
Verification 3.
We add in the initial configuration another key for Alice and we assume that
this new key sk2 has the same authdata as a previous key of Alice
already loaded onto the TPM.
ProVerif immediately discovers another attack.
The attacker can exchange a key handle by another one for which the associated key has the same authdata.
Hence, the two correspondence
properties holds.
File available
here .
Verification 4.
The attack described in the previous verification comes from the fact
that the hmac is only linked to the key via the authdata.
A patch that has been proposed for future versions of the TPM is to add (the digest of) the
public key inside the hmac.
The same transformation is done on all the hmacs.
ProVerif is now able to prove that the two correspondence properties hold.
File available
here .
Verification 5.
We now assume that the attacker has his own key loaded onto the
device.
ProVerif immediately rediscovers the attack by Gurgens
et al.
File available
here .
Verification 6.
The attack comes from the fact that the attacker can replace the
user's hmac with one of his own (pertaining to his own key).
To fix this,
we add a digest of each public
key inside each hmac.
The attack described in Verification 5 is not possible anymore.
ProVerif is now able to prove that the two correspondence properties
hold. However, it does not succeed in proving injectivity for one of
the two properties. This is due to a limitation of the tool and does not
correspond to a real attack.
File available
here .
Verification 7.
We now study the command CreateWrapKey in isolation. For this command, we
need an OSAP session.
We consider a configuration with
2 keys pairs
loaded inside the TPM.
For the moment, the intruder does not have his own key loaded onto the device.
For this simple configuration, ProVerif is able to prove the two
correspondence properties hold.
File available
here .
Verification 8.
We add in the initial configuration another key for Alice and we assume that
this new key have the same authdata than a previous key of Alice
already loaded in the TPM.
ProVerif discovers an attack of the same type as the one
presented in Verification 3.
File available
here .
Verification 9.
As in the case of the CertifyKey command, a way to fix this, is to add
pk(sk) inside the hmac. Then ProVerif is able to prove the two
correspondence properties even if we load a `dishonest' key inside the
TPM, i.e. a key for which that attacker knows the authdata.
File available
here .
Verification 10.
We now consider a much richer scenario. We consider the commands:
- CertifyKey (the version described in Verification 6 in order to avoid the previous
attacks),
- CreateWrapKey, LoadKey2, and UnBind for which we add the public key
inside the hmac (again to avoid the kind of attacks that we described in
Verification 3 and Verification 8).
We consider a scenario where an honest key and a dishonest key are already loaded
inside the TPM.
ProVerif is able to establish the 8 correspondence security properties.
However, in one case, as in Verification 6, it is not able to prove the
injective version of the property,
File available
here .