We will model and verify a simple API for key management and cryptography, similar to PKCS#11 (slides). The API can be used to generate keys in a secure device (e.g. a smartcard) and to perform cryptographic operations inside the device, without exposing the confidential keys. For simplicity we will assume that:
- We have a unique device where all keys are created and then used
- Keys persist in the device, i.e., cannot be deleted
Modelling keys and key creation
We start modelling keys and a simple key creation functionality. Given the above assumptions we can model a key
k stored in the device as the persistent fact
!Key(k). Recall, in particular, that
! in front of a fact makes it persistent in the tamarin state (see the slides and the examples).
In order to generate a new key we can now specify the following rule
rule CreateKey: [ Fr(k) ] --[ CreateKey(k) ]-> [ !Key(k) ]
This rule is composed of three parts:
kis a fresh name.
Frin tamarin is a special fact used for this purpose.
CreateKey(k)is the action executed when the rule is fired. You can think of this as the invoked action: we are creating a key by invoking the
!Key(k)specifies that this persistent fact will be added to the state once the rule is fired.
Notice that this rule can create an unbounded number of keys which are all different thanks to the
In order to specify a complete tamarin input file we use the following format:
theory Example1 begin rule CreateKey: [ Fr(k) ] --[ CreateKey(k) ]-> [ !Key(k) ] end
If we save the file as
Example1.spthy we can run the tamarin prover as follows.
Hint: you can use
nanoto create and edit the file
$ nano Example1.spthy (.... copy and paste the specification .... save with ctrl-X ...) $ tamarin-prover --prove Example1.spthy ... ============================================================================== summary of summaries: analyzed: Example1.spthy ==============================================================================
The analysis is doing nothing at the moment, apart from checking that the specification is (syntactically) correct. We can write a few sanity lemmas to check that the model is behaving as expected. We aim at proving the following properties:
- At least one key is created;
- At least two keys are created;
- All created keys are different.
The first two lemmas are called existential lemmas, as they can be proved by exhibiting a trace satisfying a condition.
Lemma 1: at least one key is created
The fact that at least one key is created can be proved by checking that
CreateKey is executed at least once. This can be specified as follows:
lemma ExecuteOnce: exists-trace " Ex k #i . CreateKey(k) @ #i "
We require that there exists a
k and a time point
#i such that
Createkey(k) is executed at time
CreateKey(k) @ #i. Notice the use of keyword
exists-trace that specifies the existential nature of the lemma. Removing this keyword would require that every trace has at least a
CreateKey(k) action which is not true if we consider the empty trace, i.e., a system that does nothing.
We can check this lemma by adding it in the specification of the
Example1.spthy file right before the
end statement, and running tamarin again:
$ tamarin-prover --prove Example1.spthy ... ============================================================================== summary of summaries: analyzed: Example1.spthy ExecuteOnce (exists-trace): verified (2 steps) ==============================================================================
Lemma 2: at least two keys are created
We can extend previous lemma to show that at least two keys are created, i.e., that
CreateKey is invoked at least twice:
lemma ExecuteTwice: exists-trace " Ex k1 k2 #i1 #i2 . CreateKey(k1) @ #i1 & CreateKey(k2) @ #i2 & not(#i1 = #i2) "
Notice that we require the existence of two keys
k2 and two time points
#i2 such that
k1 is created at time
k2 is created at time
#i2. Moreover, we ask that
#i2 are different. This is important to prevent that the lemma is trivially proved by instantiating
& is the logical and and
not(...) negates the logical statement inside the brackets.
Exercise: Add this lemma to
Example1.spthy and check it with tamarin.
Lemma 3: all created keys are different
The final lemma is that all created keys are different. This can be specified starting from the previous lemma, removing
exists-trace keyword (as we want this to hold for every trace), changing
All and adding a logical implication:
lemma AllDifferent: " All k1 k2 #i1 #i2 . CreateKey(k1) @ #i1 & CreateKey(k2) @ #i2 & not(#i1 = #i2) ==> ... "
The idea is that for all keys
k2 created in two different time points, i.e., with two different invocation of
CreateKey, we require a property of
k2. Try to complete the lemma by adding such a property in place of
... and check it in tamarin. The missing statement (using the same formatting as above) is the password for task 2!