In this section we present how to specify protocol properties as trace and observational equivalence properties, based on the action facts given in the model. Trace properties are given as guarded first-order logic formulas and observational equivalence properties are specified using the `diff`

operator, both of which we will see in detail below.

The Tamarin multiset rewriting rules define a labeled transition system. The system's state is a multiset (bag) of facts and the initial system state is the empty multiset. The rules define how the system can make a transition to a new state. The types of facts and their use are described in Section Rules. Here we focus on the *action facts*, which are used to reason about a protocol's behaviour.

A rule can be applied to a state if it can be instantiated such that its left hand side is contained in the current state. In this case, the left-hand side facts are removed from the state, and replaced by the instantiated right hand side. The application of the rule is recorded in the *trace* by appending the instantiated action facts to the trace.

For instance, consider the following fictitious rule

```
rule fictitious:
[ Pre(x), Fr(~n) ]
--[ Act1(~n), Act2(x) ]-->
[ Out(<x,~n>) ]
```

The rule rewrites the system state by consuming the facts `Pre(x)`

and `Fr(~n)`

and producing the fact `Out(<x,~n>)`

. The rule is labeled with the actions `Act1(~n)`

and `Act2(x)`

. The rule can be applied if there are two facts `Pre`

and `Fr`

in the system state whose arguments are matched by the variables `x`

and `~n`

. In the application of this rule, `~n`

and `x`

are instantiated with the matched values and the state transition is labeled with the instantiations of `Act1(~n)`

and `Act2(x)`

. The two instantiations are considered to have occurred at the same timepoint.

A *trace property* is a set of traces. We define a set of traces in Tamarin using first-order logic formulas over action facts and timepoints. More precisely, Tamarin's property specification language is a guarded fragment of a many-sorted first-order logic with a sort for timepoints. This logic supports quantification over both messages and timepoints.

The syntax for specifying security properties is defined as follows:

`All`

for universal quantification, temporal variables are prefixed with #`Ex`

for existential quantification, temporal variables are prefixed with #`==>`

for implication`&`

for conjunction`|`

for disjunction`not`

for negation`f @ i`

for action constraints, the sort prefix for the temporal variable 'i' is optional`i < j`

for temporal ordering, the sort prefix for the temporal variables 'i' and 'j' is optional`#i = #j`

for an equality between temporal variables 'i' and 'j'`x = y`

for an equality between message variables 'x' and 'y'

All action fact symbols may be used in formulas. The terms (as arguments of those action facts) are more limited. Terms are only allowed to be built from quantified variables, public constants (names delimited using single-quotes), and free function symbols including pairing. This excludes function symbols that appear in any of the equations. Moreover, all variables must be guarded. If they are not guarded, Tamarin will produce an error.

**Guardedness. ** To ensure guardedness, for universally quantified variables, one has to check that they all occur in an action constraint right after the quantifier and that the outermost logical operator inside the quantifier is an implication. For existentially quantified variables, one has to check that they all occur in an action constraint right after the quantifier and that the outermost logical operator inside the quantifier is a conjunction. We do recommend to use parentheses, when in doubt about the precedence of logical connectives, but we follow the standard precedence. Negation binds tightest, then conjunction, then disjunction and then implication.

To specify a property about a protocol to be verified, we use the keyword `lemma`

followed by a name for the property and a guarded first-order formula. This expresses that the property must hold for all traces of the protocol. For instance, to express the property that the fresh value `~n`

is distinct in all applications of the fictitious rule (or rather, if an action with the same fresh value appears twice, it actually is the same instance, identified by the timepoint), we write

```
lemma distinct_nonces:
"All n #i #j. Act1(n)@i & Act1(n)@j ==> #i=#j"
```

or equivalently

```
lemma distinct_nonces:
all-traces
"All n #i #j. Act1(n)@i & Act1(n)@j ==> #i=#j"
```

We can also express that there exists a trace for which the property holds. We do this by adding the keyword `exists-trace`

after the name and before the property. For instance, the following lemma is true if and only if the preceding lemma is false:

```
lemma distinct_nonces:
exists-trace
"not All n #i #j. Act1(n)@i & Act1(n)@j ==> #i=#j"
```

In this section we briefly explain how you can express standard secrecy properties in Tamarin and give a short example. See Protocol and Standard Security Property Specification Templates for an in-depth discussion.

Tamarin's built-in message deduction rule

```
rule isend:
[ !KU(x) ]
--[ K(x) ]-->
[ In(x) ]
```

allows us to reason about the Dolev-Yao adversary's knowledge. To specify the property that a message `x`

is secret, we propose to label a suitable protocol rule with a `Secret`

action. We then specify a secrecy lemma that states whenever the `Secret(x)`

action occurs at timepoint `i`

, the adversary does not know `x`

.

```
lemma secrecy:
"All x #i.
Secret(x) @i ==> not (Ex #j. K(x)@j)"
```

**Example.** The following Tamarin theory specifies a simple one-message protocol. Agent `A`

sends a message encrypted with agent `B`

's public key to `B`

. Both agents claim secrecy of a message, but only agent `A`

's claim is true. To distinguish between the two claims we add the action facts `Role('A')`

(respectively `Role('B')`

) to the rule modeling role `A`

(respectively to the rule for role `B`

). We then specify two secrecy lemmas, one for each role.

```
theory secrecy_asym_enc
begin
builtins: asymmetric-encryption
/* We formalize the following protocol:
1. A -> B: {A,na}pk(B)
*/
// Public key infrastructure
rule Register_pk:
[ Fr(~ltkX) ]
-->
[ !Ltk($X, ~ltkX)
, !Pk($X, pk(~ltkX))
, Out(pk(~ltkX))
]
// Compromising an agent's long-term key
rule Reveal_ltk:
[ !Ltk($X, ltkX) ] --[ Reveal($X) ]-> [ Out(ltkX) ]
// Role A sends first message
rule A_1_send:
[ Fr(~na)
, !Ltk($A, ltkA)
, !Pk($B, pkB)
]
--[ Send($A, aenc(<$A, ~na>, pkB))
, Secret(~na), Honest($A), Honest($B), Role('A')
]->
[ St_A_1($A, ltkA, pkB, $B, ~na)
, Out(aenc(<$A, ~na>, pkB))
]
// Role B receives first message
rule B_1_receive:
[ !Ltk($B, ltkB)
, In(aenc(<$A, na>,pk(ltkB)))
]
--[ Recv($B, aenc(<$A, na>, pk(ltkB)))
, Secret(na), Honest($B), Honest($A), Role('B')
]->
[ St_B_1($B, ltkB, $A, na)
]
lemma executable:
exists-trace
"Ex A B m #i #j. Send(A,m)@i & Recv(B,m) @j"
lemma secret_A:
all-traces
"All n #i. Secret(n) @i & Role('A') @i ==> (not (Ex #j. K(n)@j)) | (Ex B #j. Reveal(B)@j & Honest(B)@i)"
lemma secret_B:
all-traces
"All n #i. Secret(n) @i & Role('B') @i ==> (not (Ex #j. K(n)@j)) | (Ex B #j. Reveal(B)@j & Honest(B)@i)"
end
```

In the above example the lemma `secret_A`

holds as the initiator generated the fresh value, while the responder has no guarantees, i.e., lemma `secret_B`

yields an attack.

In this section we show how to specify a simple message authentication property. For specifications of the properties in Lowe's hierarchy of authentication specifications (Lowe 1997) see the Section Protocol and Standard Security Property Specification Templates.

We specify the following *message authentication* property: If an agent `a`

believes that a message `m`

was sent by an agent `b`

, then `m`

was indeed sent by `b`

. To specify `a`

's belief we label an appropriate rule in `a`

's role specification with the action `Authentic(b,m)`

. The following lemma defines the set of traces that satisfy the message authentication property.

```
lemma message_authentication:
"All b m #j. Authentic(b,m) @j ==> Ex #i. Send(b,m) @i &i<j"
```

A simple message authentication example is the following one-message protocol. Agent `A`

sends a signed message to agent `B`

. We model the signature using asymmetric encryption. A better model is shown in the section on Restrictions.

```
theory auth_signing_simple
begin
builtins: asymmetric-encryption
/* We formalize the following protocol:
1. A -> B: {A,na}sk(A)
*/
// Public key infrastructure
rule Register_pk:
[ Fr(~ltkX) ]
-->
[ !Ltk($X, ~ltkX)
, !Pk($X, pk(~ltkX))
, Out(pk(~ltkX))
]
// Role A sends first message
rule A_1_send:
[ Fr(~na)
, !Ltk($A, ltkA)
]
--[ Send($A, <$A, ~na>)
]->
[ St_A_1($A, ltkA, ~na)
, Out(aenc(<$A, ~na>,ltkA))
]
// Role B receives first message
rule B_1_receive:
[ !Pk($A, pk(skA))
, In(aenc(<$A, na>,skA))
]
--[ Recv($B, <$A, na>)
, Authentic($A,<$A, na>), Honest($B), Honest($A)
]->
[ St_B_1($B, pk(skA), $A, <$A, na>)
]
lemma executable:
exists-trace
"Ex A B m #i #j. Send(A,m)@i & Recv(B,m) @j"
lemma message_authentication:
"All b m #i. Authentic(b,m) @i
==> (Ex #j. Send(b,m) @j & j<i)"
end
```

All the previous properties are trace properties, i.e., properties that are defined on each trace independently. For example, the definition of secrecy required that there is no trace where the adversary could compute the secret without having previously corrupted the agent.

In contrast, Observational Equivalence properties reason about two systems (for example two instances of a protocol), by showing that an intruder cannot distinguish these two systems. This can be used to express privacy-type properties, or cryptographic indistinguishability properties.

For example, a simple definition of privacy for voting requires that an adversary cannot distinguish two instances of a voting protocol where two voters swap votes. That is, in the first instance, voter `A`

votes for candidate `a`

and voter `B`

votes for `b`

, and in the second instance voter `A`

votes for candidate `b`

and voter `B`

votes for `a`

. If the intruder cannot tell both instances apart, he does not know which voter votes for which candidate, even though he might learn the result, i.e., that there is one vote for a and one for b.

Tamarin can prove such properties for two systems that only differ in terms using the `diff( , )`

operator. Consider the following toy example, where one creates a public key, two fresh values `~a`

and `~b`

, and publishes `~a`

. Then one encrypts either `~a`

or `~b`

(modeled using the `diff`

operator) and sends out the ciphertext:

```
// Generate a public key and output it
// Choose two fresh values and reveal one of it
// Encrypt either the first or the second fresh value
rule Example:
[ Fr(~ltk)
, Fr(~a)
, Fr(~b) ]
--[ Secret( ~b ) ]->
[ Out( pk(~ltk) )
, Out( ~a )
, Out( aenc( diff(~a,~b), pk(~ltk) ) )
]
```

In this example, the intruder cannot compute `~b`

as formalized by the following lemma:

```
lemma B_is_secret:
" /* The intruder cannot know ~b: */
All B #i. (
/* ~b is claimed secret implies */
Secret(B) @ #i ==>
/* the adversary does not know '~b' */
not( Ex #j. K(B) @ #j )
)
```

However, he can know whether in the last message `~a`

or `~b`

was encrypted by simply taking the output `~a`

, encrypting it with the public key and comparing it to the published ciphertext. This is captured using observational equivalence.

To see how this works, we need to start Tamarin in observational equivalence mode by adding a `--diff`

to the command:

`tamarin-prover interactive --diff ObservationalEquivalenceExample.spthy`

Now point your browser to http://localhost:3001. After clicking on the theory `ObservationalEquivalenceExample`

, you should see the following.

There are multiple differences to the 'normal' trace mode.

First, there is a new option `Diff Rules`

, which will simply present the rewrite rules from the `.spthy`

file. (See image below.)

Second, all the other points (Message Theory, Multiset Rewrite Rules, Raw/Refined Sources) have been quadruplicated. The reason for this is that any input file with the `diff`

operator actually specifies two models: one model where each instance of `diff(x,y)`

is replaced with `x`

(the *left hand side*, or LHS for short), and one model where each instance of `diff(x,y)`

is replaced with `y`

(the *right hand side*, or RHS for short). Moreover, as the observational equivalence mode requires different precomputations, each of the two models is treated twice. For example, the point `RHS: Raw sources [Diff]`

gives the raw sources for the RHS interpretation of the model in observational equivalence mode, whereas `LHS: Raw sources`

gives the raw sources for the LHS interpretation of the model in the 'trace' mode.

Third, all lemmas have been duplicated: the lemma `B_is_secret`

exists once on the left hand side (marked using `[left]`

) and once on the right hand side (marked using `[right]`

), as both models can differ and thus the lemma needs to be proven on both sides.

Finally, there is a new lemma `Observational_equivalence`

, added automatically by Tamarin (so no need to define it in the `.spthy`

input file). By proving this lemma we can prove observational equivalence between the LHS and RHS models.

In the `Diff Rules`

, we have the rules as written in the input file:

If we click on `LHS: Multiset rewriting rules`

, we get the LHS interpretation of the rules (here `diff(~a, ~b)`

was replaced by `~a`

):

If we click on `RHS: Multiset rewriting rules`

, we get the RHS interpretation of the rules (here `diff(~a, ~b)`

was replaced by `~b`

):

We can easily prove the `B_is_secret`

lemma on both sides:

To start proving observational equivalence, we only have the proof step `1. rule-equivalence`

. This generates multiple subcases:

Essentially, there is a subcase per protocol rule, and there are also cases for several adversary rules. The idea of the proof is to show that whenever a rule can be executed on either the LHS or RHS, it can also be executed on the other side. Thus, no matter what the adversary does, he will always see 'equivalent' executions. To prove this, Tamarin computes for each rule all possible executions on both sides, and verifies whether an 'equivalent' execution exists on the other side. If we continue our proof by clicking on `backward-search`

, Tamarin generates two sub-cases, one for each side. For each side, Tamarin will continue by constructing all possible executions of this rule.

During this search, Tamarin can encounter executions that can be 'mirrored' on the other side, for example the following execution where the published key is successfully compared to itself:

Or, Tamarin can encounter executions that do not map to the other side. For example the following execution on the LHS that encrypts `~a`

using the public key and successfully compares the result to the published ciphertext, is not possible on the RHS (as there the ciphertext contains `~b`

). Such an execution corresponds to a potential attack, and thus invalidates the "Observational_equivalence" lemma.

Note that Tamarin needs to potentially consider numerous possible executions, which can result in long proof times or even non-termination. If possible it tries not to resolve parts of the execution that are irrelevant, but this is not always sufficient.

Restrictions restrict the set of traces to be considered in the protocol analysis. They can be used for purposes ranging from modeling branching behavior of protocols to the verification of signatures. We give a brief example of the latter. Consider the simple message authentication protocol, where an agent `A`

sends a signed message to an agent `B`

. We use Tamarin's built-in equational theory for signing.

```
// Role A sends first message
rule A_1_send:
let m = <A, ~na>
in
[ Fr(~na)
, !Ltk(A, ltkA)
, !Pk(B, pkB)
]
--[ Send(A, m)
]->
[ St_A_1(A, ltkA, pkB, B, ~na)
, Out(<m,sign(m,ltkA)>)
]
// Role B receives first message
rule B_1_receive:
[ !Ltk(B, ltkB)
, !Pk(A, pkA)
, In(<m,sig>)
]
--[ Recv(B, m)
, Eq(verify(sig,m,pkA),true)
, Authentic(A,m), Honest(B), Honest(A)
]->
[ St_B_1(B, ltkB, pkA, A, m)
]
```

In the above protocol, agent `B`

verifies the signature `sig`

on the received message `m`

. We model this by considering only those traces of the protocol in which the application of the `verify`

function to the received message equals the constant `true`

. To this end, we specify the equality restriction

```
restriction Equality:
"All x y #i. Eq(x,y) @i ==> x = y"
```

The full protocol theory is given below.

```
theory auth_signing
begin
builtins: signing
/* We formalize the following protocol:
1. A -> B: {A,na}sk(A)
using Tamarin's builtin signing and verification functions.
*/
// Public key infrastructure
rule Register_pk:
[ Fr(~ltkA) ]
-->
[ !Ltk($A, ~ltkA)
, !Pk($A, pk(~ltkA))
, Out(pk(~ltkA))
]
// Compromising an agent's long-term key
rule Reveal_ltk:
[ !Ltk(A, ltkA) ] --[ Reveal(A) ]-> [ Out(ltkA) ]
// Role A sends first message
rule A_1_send:
let m = <A, ~na>
in
[ Fr(~na)
, !Ltk(A, ltkA)
, !Pk(B, pkB)
]
--[ Send(A, m)
]->
[ St_A_1(A, ltkA, pkB, B, ~na)
, Out(<m,sign(m,ltkA)>)
]
// Role B receives first message
rule B_1_receive:
[ !Ltk(B, ltkB)
, !Pk(A, pkA)
, In(<m,sig>)
]
--[ Recv(B, m)
, Eq(verify(sig,m,pkA),true)
, Authentic(A,m), Honest(B), Honest(A)
]->
[ St_B_1(B, ltkB, pkA, A, m)
]
restriction Equality:
"All x y #i. Eq(x,y) @i ==> x = y"
lemma executable:
exists-trace
"Ex A B m #i #j. Send(A,m)@i & Recv(B,m) @j"
lemma message_authentication:
"All b m #i. Authentic(b,m) @i
==> (Ex #j. Send(b,m) @j & j<i)
| (Ex B #r. Reveal(B)@r & Honest(B) @i & r < i)"
end
```

Note that restrictions can also be used to verify observational equivalence properties. As there are no user-specifiable lemmas for observational equivalence, restrictions can be used to remove state space, which essentially removes degenerate cases.

Here is a list of common restrictions. Do note that you need to add the appropriate action facts to your rules for these restrictions to have impact.

First, let us show a restriction forcing an action (with a particular value) to be unique:

```
restriction unique:
"All x #i #j. UniqueFact(x) @#i & UniqueFact(x) @#j ==> #i = #j"
```

We call the action `UniqueFact`

and give it one argument. If it appears on the trace twice, it actually is only once, as the two time points are identified.

Next, let us consider an equality restriction. This is useful if you do not want to use pattern-matching explicitly, but maybe want to ensure that the decryption of an encrypted value is the original value, assuming correct keys. The restriction looks like this:

```
restriction Equality:
"All x y #i. Eq(x,y) @#i ==> x = y"
```

which means that all instances of the `Eq`

action on the trace have the same value as both its arguments.

Now, let us consider an inequality restriction, which ensures that the two arguments of `Neq`

are different:

```
restriction Inequality:
"All x #i. Neq(x,x) @ #i ==> F"
```

This is very useful to ensure that certain arguments are different.

If you have a rule that should only be executed once, put `OnlyOnce()`

as an action fact for that rule and add this restriction:

```
restriction OnlyOnce:
"All #i #j. OnlyOnce()@#i & OnlyOnce()@#j ==> #i = #j"
```

Then that rule can only be executed once. Note that if you have multiple rules that all have this action fact, at most one of them can be executed a single time.

A similar construction can be used to limit multiple occurrences of an action for specific instantiations of variables, by adding these as arguments to the action. For example, one could put `OnlyOnceV('Initiator')`

in a rule creating an initiator process, and `OnlyOnceV('Responder')`

in the rule for the responder. If used with the following restriction, this would then yield the expected result of at most one initiator and at most one responder:

```
restriction OnlyOnceV:
"All #i #j x. OnlyOnceV(x)@#i & OnlyOnceV(x)@#j ==> #i = #j"
```

If we use the `multiset`

built-in we can construct numbers as "1+1+...+1", and have a restriction enforcing that one number is less than another, say `LessThan`

:

```
restriction LessThan:
"All x y #i. LessThan(x,y)@#i ==> Ex z. x + z = y"
```

You would then add the `LessThan`

action fact to a rule where you want to enforce that a counter has strictly increased.

Similarly you can use a `GreaterThan`

where we want `x`

to be strictly larger than `y`

:

```
restriction GreaterThan:
"All x y #i. GreaterThan(x,y)@#i ==> Ex z. x = y + z"
```

Tamarin supports a number of annotations to its lemmas, which change their meaning. Any combination of them is allowed. We explain them in this section. The usage is that any annotation goes into square brackets after the lemma name, i.e., for a lemma called "Name" and the added annotations "Annotation1" and "Annotation2", this looks like so:

`lemma Name [Annotation1,Annotation2]:`

`sources`

To declare a lemma as a source lemma, we use the annotation `sources`

:

```
lemma example [sources]:
"..."
```

This means a number of things:

- The lemma's verification will use induction.
- The lemma will be verified using the
`Raw sources`

. - The lemma will be used to generate the
`Refined sources`

, which are used for verification of all non-`sources`

lemmas.

Source lemmas are necessary whenever the analysis reports `partial deconstructions left`

in the `Raw sources`

. See section on Open chains for details on this.

All `sources`

lemmas are used only for the case distinctions and do not benefit from other lemmas being marked as `reuse`

.

`use_induction`

As you have seen before, the first choice in any proof is whether to use simplification (the default) or induction. If you know that a lemma will require induction, you just annotate it with `use_induction`

, which will make it use induction instead of simplification.

`reuse`

A lemma marked `reuse`

will be used in the proofs of all lemmas syntactically following it (except `sources`

lemmas as above). This includes other `reuse`

lemmas that can transitively depend on each other.

`hide_lemma=L`

It can sometimes be helpful to have lemmas that are used only for the proofs of other lemmas. For example, assume 3 lemmas, called `A`

, `B`

, and `C`

. They appear in that order, and `A`

and `B`

are marked reuse. Then, during the proof of `C`

both `A`

and `B`

are reused, but sometimes you might only want to use `B`

, but the proof of `B`

needs `A`

. The solution then is to hide the lemma `A`

in `C`

:

```
lemma A [reuse]:
...
lemma B [reuse]:
...
lemma C [hide_lemma=A]:
...
```

This way, `C`

uses `B`

which in turn uses `A`

, but `C`

does not use `A`

directly.

`left`

and `right`

In the observational equivalence mode you have two protocols, the left instantiation of the *diff-terms* and their right instantiation. If you want to consider a lemma only on the left or right instantiation you annotate it with `left`

, respectively `right`

. If you annotate a lemma with `[left,right]`

then both lemmas get generated, just as if you did not annotate it with either of `left`

or `right`

.

In this section we provide templates for specifying protocols and standard security properties in a unified manner.

A protocol specifies two or more roles. For each role we specify an initialization rule that generates a fresh run identifier `id`

(to distinguish parallel protocol runs of an agent) and sets up an agent's initial knowledge including long term keys, private keys, shared keys, and other agent's public keys. We label such a rule with the action fact `Create(A,id)`

, where `A`

is the agent name (a public constant) and `id`

the run identifier and the action fact `Role('A')`

, where `'A'`

is a public constant string. An example of this is the following initialization rule:

```
// Initialize Role A
rule Init_A:
[ Fr(~id)
, !Ltk(A, ltkA)
, !Pk(B, pkB)
]
--[ Create(A, ~id), Role('A') ]->
[ St_A_1(A, ~id, ltkA, pkB, B)
]
```

The pre-distributed key infrastructure is modeled with a dedicated rule that may be accompanied by a key compromise rule. The latter is to model compromised agents and is labeled with a `Reveal(A)`

action fact, where `A`

is the public constant denoting the compromised agent. For instance, a public key infrastructure is modeled with the following two rules:

```
// Public key infrastructure
rule Register_pk:
[ Fr(~ltkA) ]
-->
[ !Ltk($A, ~ltkA)
, !Pk($A, pk(~ltkA))
, Out(pk(~ltkA))
]
rule Reveal_ltk:
[ !Ltk(A, ltkA) ] --[ Reveal(A) ]-> [ Out(ltkA) ]
```

We use the `Secret(x)`

action fact to indicate that the message `x`

is supposed to be secret. The simple secrecy property `"All x #i. Secret(x) @i ==> not (Ex #j. K(x)@j)"`

may not be satisfiable when agents' keys are compromised. We call an agent whose keys are not compromised an *honest* agent. We indicate assumptions on honest agents by labeling the same rule that the `Secret`

action fact appears in with an `Honest(B)`

action fact, where `B`

is the agent name that is assumed to be honest. For instance, in the following rule the agent in role `'A'`

is sending a message, where the nonce `~na`

is supposed to be secret assuming that both agents `A`

and `B`

are honest.

```
// Role A sends first message
rule A_1_send:
[ St_A_1(A, ~id, ltkA, pkB, B)
, Fr(~na)
]
--[ Send(A, aenc{A, ~na}pkB)
, Secret(~na), Honest(A), Honest(B), Role('A')
]->
[ St_A_2(A, ~id, ltkA, pkB, B, ~na)
, Out(aenc{A, ~na}pkB)
]
```

We then specify the property that a message `x`

is secret as long as agents assumed to be honest have not been compromised as follows

```
lemma secrecy:
"All x #i.
Secret(x) @i ==>
not (Ex #j. K(x)@j)
| (Ex B #r. Reveal(B)@r & Honest(B) @i)"
```

The lemma states that whenever a secret action `Secret(x)`

occurs at timepoint `i`

, the adversary does not know `x`

or an agent claimed to be honest at time point `i`

has been compromised at a timepoint `r`

.

A stronger secrecy property is *perfect forward secrecy*. It requires that messages labeled with a `Secret`

action before a compromise remain secret.

```
lemma secrecy_PFS:
"All x #i.
Secret(x) @i ==>
not (Ex #j. K(x)@j)
| (Ex B #r. Reveal(B)@r & Honest(B) @i & r < i)"
```

**Example.** The following Tamarin theory specifies a simple one-message protocol. Agent `A`

sends a message encrypted with agent `B`

's public key to `B`

. Both agents claim secrecy of a message, but only agent `A`

's claim is true. To distinguish between the two claims we add the action facts `Role('A')`

and `Role('B')`

for role `A`

and `B`

, respectively and specify two secrecy lemmas, one for each role.

The perfect forward secrecy claim does not hold for agent `A`

. We show this by negating the perfect forward secrecy property and stating an exists-trace lemma.

```
theory secrecy_template
begin
builtins: asymmetric-encryption
/* We formalize the following protocol:
1. A -> B: {A,na}pk(B)
*/
// Public key infrastructure
rule Register_pk:
[ Fr(~ltkA) ]
-->
[ !Ltk($A, ~ltkA)
, !Pk($A, pk(~ltkA))
, Out(pk(~ltkA))
]
rule Reveal_ltk:
[ !Ltk(A, ltkA) ] --[ Reveal(A) ]-> [ Out(ltkA) ]
// Initialize Role A
rule Init_A:
[ Fr(~id)
, !Ltk(A, ltkA)
, !Pk(B, pkB)
]
--[ Create(A, ~id), Role('A') ]->
[ St_A_1(A, ~id, ltkA, pkB, B)
]
// Initialize Role B
rule Init_B:
[ Fr(~id)
, !Ltk(B, ltkB)
, !Pk(A, pkA)
]
--[ Create(B, ~id), Role('B') ]->
[ St_B_1(B, ~id, ltkB, pkA, A)
]
// Role A sends first message
rule A_1_send:
[ St_A_1(A, ~id, ltkA, pkB, B)
, Fr(~na)
]
--[ Send(A, aenc{A, ~na}pkB)
, Secret(~na), Honest(A), Honest(B), Role('A')
]->
[ St_A_2(A, ~id, ltkA, pkB, B, ~na)
, Out(aenc{A, ~na}pkB)
]
// Role B receives first message
rule B_1_receive:
[ St_B_1(B, ~id, ltkB, pkA, A)
, In(aenc{A, na}pkB)
]
--[ Recv(B, aenc{A, na}pkB)
, Secret(na), Honest(B), Honest(A), Role('B')
]->
[ St_B_2(B, ~id, ltkB, pkA, A, na)
]
lemma executable:
exists-trace
"Ex A B m #i #j. Send(A,m)@i & Recv(B,m) @j"
lemma secret_A:
"All n #i. Secret(n) @i & Role('A') @i ==>
(not (Ex #j. K(n)@j)) | (Ex X #j. Reveal(X)@j & Honest(X)@i)"
lemma secret_B:
"All n #i. Secret(n) @i & Role('B') @i ==>
(not (Ex #j. K(n)@j)) | (Ex X #j. Reveal(X)@j & Honest(X)@i)"
lemma secrecy_PFS_A:
exists-trace
"not All x #i.
Secret(x) @i & Role('A') @i ==>
not (Ex #j. K(x)@j)
| (Ex B #r. Reveal(B)@r & Honest(B) @i & r < i)"
end
```

In this section we show how to formalize the entity authentication properties of Lowe's hierarchy of authentication specifications (Lowe 1997) for two-party protocols.

All the properties defined below concern the authentication of an agent in role `'B'`

to an agent in role `'A'`

. To analyze a protocol with respect to these properties we label an appropriate rule in role `A`

with a `Commit(a,b,<'A','B',t>)`

action and in role `B`

with the `Running(b,a,<'A','B',t>)`

action. Here `a`

and `b`

are the agent names (public constants) of roles `A`

and `B`

, respectively and `t`

is a term.

- Aliveness

A protocol guarantees to an agent `a`

in role `A`

*aliveness* of another agent `b`

if, whenever `a`

completes a run of the protocol, apparently with `b`

in role `B`

, then `b`

has previously been running the protocol.

```
lemma aliveness:
"All a b t #i.
Commit(a,b,t)@i
==> (Ex id #j. Create(b,id) @ j)
| (Ex C #r. Reveal(C) @ r & Honest(C) @ i)"
```

- Weak agreement

A protocol guarantees to an agent `a`

in role `A`

*weak agreement* with another agent `b`

if, whenever agent `a`

completes a run of the protocol, apparently with `b`

in role `B`

, then `b`

has previously been running the protocol, apparently with `a`

.

```
lemma weak_agreement:
"All a b t1 #i.
Commit(a,b,t1) @i
==> (Ex t2 #j. Running(b,a,t2) @j)
| (Ex C #r. Reveal(C) @ r & Honest(C) @ i)"
```

- Non-injective agreement

A protocol guarantees to an agent `a`

in role `A`

*non-injective agreement* with an agent `b`

in role `B`

on a message `t`

if, whenever `a`

completes a run of the protocol, apparently with `b`

in role `B`

, then `b`

has previously been running the protocol, apparently with `a`

, and `b`

was acting in role `B`

in his run, and the two principals agreed on the message `t`

.

```
lemma noninjective_agreement:
"All a b t #i.
Commit(a,b,t) @i
==> (Ex #j. Running(b,a,t) @j)
| (Ex C #r. Reveal(C) @ r & Honest(C) @ i)"
```

- Injective agreement

We next show the lemma to analyze *injective agreement*. A protocol guarantees to an agent `a`

in role `A`

injective agreement with an agent `b`

in role `B`

on a message `t`

if, whenever `a`

completes a run of the protocol, apparently with `b`

in role `B`

, then `b`

has previously been running the protocol, apparently with `a`

, and `b`

was acting in role `B`

in his run, and the two principals agreed on the message `t`

. Additionally, there is a unique matching partner instance for each completed run of an agent, i.e., for each `Commit`

by an agent there is a unique `Running`

by the supposed partner.

```
lemma injectiveagreement:
"All A B t #i.
Commit(A,B,t) @i
==> (Ex #j. Running(B,A,t) @j
& j < i
& not (Ex A2 B2 #i2. Commit(A2,B2,t) @i2
& not (#i2 = #i)))
| (Ex C #r. Reveal(C)@r & Honest(C) @i)"
```

The idea behind injective agreement is to prevent replay attacks. Therefore, new freshness will have to be involved in each run, meaning the term `t`

must contain such a fresh value.

Lowe, Gavin. 1997. “A Hierarchy of Authentication Specifications.” In *10th Computer Security Foundations Workshop (Csfw 1997), June 10-12, 1997, Rockport, Massachusetts, Usa*, 31–44. IEEE Computer Society. http://www.cs.ox.ac.uk/people/gavin.lowe/Security/Papers/authentication.ps.