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:

`Fr(k)`

specifies that`k`

is a fresh name.`Fr`

in 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`CreateKey(k)`

functionality.`!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:

- 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 `#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!