theory Lemmas
begin
// Security properties are specified in lemmas, which are defined after the
// rules.
rule FreshValue:
[ Fr(~v) ]
--[ Action(~v) ]->
[]
/*
* Let us prove a trivial property: fresh values are all distinct. By
* default, properties are checked against all the traces (`all-traces` below
* can be omitted because it is the default). I.e., given a lemma φ, Tamarin
* tries to solve the constraint system {¬φ} (if the constraint system has no
* solution, then ¬φ is unsatisfiable, so φ is valid; if the constraint
* system has a solution then ¬φ is satisfiable, and Tamarin outputs an attack).
*/
lemma fresh_values_are_all_distinct:
all-traces
"
/*
* "If fresh value x was consumed at time i and at time j,
* then i and j must coincide."
*/
All x #i #j. Action(x)@i & Action(x)@j ==> #i = #j
"
/*
* You may check the syntax of the program with:
*
* tamarin-prover ex5-lemmas.spthy
*
* but the result will be "analysis incomplete".
* To carry out the automatic proof, you need to pass --prove:
*
* tamarin-prover ex5-lemmas.spthy --prove
*
* The proof is trivial, and can be inspected in the GUI with:
*
* tamarin-prover interactive ex5-lemmas.spthy --prove
*
* or with:
*
* tamarin-prover interactive ex5-lemmas.spthy
*
* if you want to carry out the proof interactively.
*/
end