Task 1: key creation

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:

  1. We have a unique device where all keys are created and then used
  2. 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:

  1. Fr(k) specifies that k is a fresh name. Fr in tamarin is a special fact used for this purpose.
  2. 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 CreateKey(k) functionality.
  3. !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 Fr(k) special fact.

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 nano to 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:

  1. At least one key is created;
  2. At least two keys are created;
  3. 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 #i, written 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 k1 and k2 and two time points #i1 and #i2 such that k1 is created at time #i1 and k2 is created at time #i2. Moreover, we ask that #i1 and #i2 are different. This is important to prevent that the lemma is trivially proved by instantiating k1=k2 and #i1=#2.

Symbol & 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 Ex into 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 k1 and k2 created in two different time points, i.e., with two different invocation of CreateKey, we require a property of k1 and 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!