In this section we discuss some problems that a first-time user might face. This includes error messages and how one might fix them. We also discuss how certain ‘sanity’ lemmas can be proven to provide some confidence in the protocol specification.
To illustrate these concepts, consider the following protocol, where an initiator
$I and a receiver
$R share a symmetric key
$I then sends the message
~m, encrypted with their shared key
builtins: symmetric-encryption /* protocol */ rule setup: [ Fr(~k), Fr(~m) ] ---> [ AgSt($I,<~k,~m>), AgSt($R,~k) ] rule I_1: [ AgSt($I,<~k,~m>) ] --[ Send($I,~m) ]-> [ Out(senc(~m,~k)) ] rule R_1: [ AgSt($R,~k), In(senc(m,~k)) ] --[ Receive($R,m), Secret(m) ]-> [ ] lemma nonce_secret: "All m #i #j. Secret(m) @i & K(m) @j ==> F"
With the lemma
nonce_secret, we examine if the message is secret from the receiver’s perspective.
Imagine that in the setup rule you forgot the agent state fact for the receiver
AgSt($R,~k) as follows:
// WARNING: this rule illustrates a non-functional protocol rule setup: [ Fr(~k), Fr(~m) ] ---> [ AgSt($I,<~k,~m>) ]
With this omission, Tamarin verifies the lemma
nonce_secret. The lemma says that whenever the action
Secret(m) is reached in a trace, then the adversary does not learn
m. However, in the modified specification, the rule
R_1 will never be executed. Consequently there will never be an action
Secret(m) in the trace. For this reason, the lemma is vacuously true and verifying the lemma does not mean that the intended protocol has this property. To avoid proving lemmas in such degenerate ways, we first prove
With an exist-trace lemma, we prove, in essence, that our protocol can be executed. In the above example, the goal is that first an initiator sends a message and that then the receiver receives the same message. We express this as follows:
lemma functional: exists-trace "Ex I R m #i #j. Send(I,m) @i & Receive(R,m) @j "
If we try to prove this with Tamarin in the model with the error, the lemma statement will be falsified. This indicates that there exists no trace where the initiator sends a message to the receiver. Such errors arise, for example, when we forget to add a fact that connects several rules and some rules can never be reached. Generally it is recommended first to prove an
exists-trace lemma before other properties are examined.
In this section, we review common error messages produced by Tamarin. To this end, we will intentionally add mistakes to the above protocol, presenting a modified rule and explaining the corresponding error message.
First we change the setup rule as follows:
// WARNING: this rule illustrates an error message rule setup: [ Fr(~k), Fr(~m) ] ---> [ AgSt($I,~k,~m), AgSt($R,~k) ]
Note that the first
AgSt(...) in the conclusion has arity three, with variables
$I,~k,~m, rather than the original arity two, with variables
$I,<~k,~m> where the second argument is paired.
The following statement that some wellformedness check failed will appear at the very end of the text when loading this theory.
WARNING: 1 wellformedness check failed! The analysis results might be wrong!
Such a wellformedness warning appears in many different error messages at the bottom and indicates that there might be a problem. However, to get further information, one must scroll up in the command line to look at the more detailed error messages.
/* WARNING: the following wellformedness checks failed! fact usage: 1. rule `setup', fact "agst": ("AgSt",3,Linear) AgSt( $I, ~k, ~m ) 2. rule `setup', fact "agst": ("AgSt",2,Linear) AgSt( $R, ~k ) 3. rule `I_1', fact "agst": ("AgSt",2,Linear) AgSt( $I, <~k, ~m> ) 4. rule `R_1', fact "agst": ("AgSt",2,Linear) AgSt( $R, ~k ) */
The problem lists all the fact usages of fact
AgSt. The statement
1. rule 'setup', fact "agst":("AgSt",3,Linear) means that in the rule
setup the fact
AgSt is used as a linear fact with 3 arguments. This is not consistent with its use in other rules. For example
2. rule 'setup', fact "agst": ("AgSt",2,Linear) indicates that it is also used with 2 arguments in the
setup rule. To solve this problem we must ensure that we only use the same fact with the same number of arguments.
If we change the rule
// WARNING: this rule illustrates an error message rule R_1: [ AgSt($R,~k), In(senc(~m,~k)) ] --[ Receive($R,$I,~m), Secret($R,~n) ]-> [ ]
we get the error message
/* WARNING: the following wellformedness checks failed! unbound: rule `R_1' has unbound variables: ~n */
unbound variables indicates that there is a term, here the fresh
~n, in the action or conclusion that never appeared in the premise. Here this is the case because we mistyped
~n instead of
~m. Generally, when such a warning appears, you should check that all the fresh variables already occur in the premise. If it is a fresh variable that appears for the first time in this rule, a
Fr(~n) fact should be added to the premise.
Next, we change the functional lemma as follows
// WARNING: this lemma illustrates an error message lemma functional: exists-trace "Ex I R #i #j. Send(I,R,m) @i & Receive(R,I,m) @j "
This causes the following warning:
/* WARNING: the following wellformedness checks failed! formula terms: lemma `functional' uses terms of the wrong form: `Free m', `Free m' The only allowed terms are public names and bound node and message variables. If you encounter free message variables, then you might have forgotten a #-prefix. Sort prefixes can only be dropped where this is unambiguous. */
The warning indicates that in this lemma the term
m occurs free. This means that it is not bound to any quantifier. Often such an error occurs when one forgets to list all the variables that are used in the formula after the
All quantifier. In our example, the problem occurred because we deleted the
Ex I R m #i #j.
Next, we change the lemma
// WARNING: this lemma illustrates an error message lemma nonce_secret: "All R m #i #j. Secr(R,m) @i & K(m) @j ==> F"
We get the following warning:
/* WARNING: the following wellformedness checks failed! lemma actions: lemma `nonce_secret' references action (ProtoFact Linear "Secr" 2,2,Linear) but no rule has such an action. */
Such a warning always occurs when a lemma uses a fact that never appears as an action fact in any rule. The cause of this is either that the fact is spelled differently (here
Secr instead of
Secret) or that one forgot to add the action fact to the protocol rules. Generally, it is good practice to double check that the facts that are used in the lemmas appear in the relevant protocol rules as actions.
If we omit the line
the following warning will be output
unexpected "(" expecting letter or digit, ".", "," or ")"
The warning indicates that Tamarin did not expect opening brackets. This means that a function is used that Tamarin does not recognize. This can be the case if a function
f is used that has not been declared with
functions: f/1. Also, this warning occurs when a built-in function is used but not declared. In this example, the problem arises because we used the symmetric encryption
senc, but omitted the line where we declare that we use this built-in function.
If we change the
setup rule to
// WARNING: this rule illustrates an error message rule setup: [ Fr(~k), Fr(~m) ] ---> [ AgSt($I,<~k,m>), AgSt($R,~k) ]
we get the error message
/* WARNING: the following wellformedness checks failed! unbound: rule `setup' has unbound variables: m sorts: rule `setup' clashing sorts, casings, or multiplicities: 1. ~m, m */
This indicates that the sorts of a message were inconsistently used. In the rule
setup, this is the case because we used m once as a fresh value
~m and another time without the
Tamarin may fail to terminate when it automatically constructs proofs. One reason for this is that there are open chains. For advice on how to find and remove open chains, see open chains.