Complete reference: link
rule RuleName:
let t3 = t2 in // optional
[ F1(t1, t2) ] // premise (multiset/list of facts)
--[ L(t1) ]->
[ F2(t3) ] // conclusion (multiset/list of facts)
F1
,F2
are factsL
is an action factt1
,t2
,t3
are terms
Out(m)
- Sendm
(only in conclusion)In(m)
- Receivem
(only in premise)Fr(x)
- Generate unguessable/fresh valuex
(only in premise)
Complete reference: link
- Messages (anything), e.g.,
m
- Constants, e.g.,
'constant'
- Unguessable (fresh) values, e.g.,
~k
- Public values, e.g,
$P
- Function application
f(t1, t2)
Define function senc
with 2 arguments and sdec
with 2 arguments:
functions: senc/2, sdec/2
Define equation for aforementioned functions:
equations: sdec(senc(m, k), k) = m
Import built-in theory symmetric-encryption
(which "imports" custom definition from above):
builtins: symmetric-encryption
Complete reference: link
All v. p
: For allv
,p
holdsEx v. p
: For somev
,p
holdsL(t1, ...) @ #x
: Action factL
occurs at timepoint#x
with argumentst1, ...
- You can use the reserved action fact
K(x)
to express that the adversary knows termx
. - Sometimes, you may also need to use
KU(x)
in auxiliary lemmas.KU
means that the adversary used termx
to construct a message.
- You can use the reserved action fact
#i < #j
: Timepoint#i
is smaller than timepoint#j
t1 = t2
/#i = #j
: Terms (or timepoints) are equal- Standard logical operands:
p & q
,p | q
,not p
,p ==> q
(equivalent top | not q
)
Properties you want to be true of your model.
// Usually: verify that something you expect to be impossible is impossible
lemma ForAll:
all-traces
"All m #x. Secret(m) @ #x ==> not Ex #y. K(m) @ #y"
// Usually: verify that something you expect to be possible is possible
lemma ForSome:
exists-trace
"Ex #t. ProtocolCompleted() @ #t"
Assumptions of your model. Often used to implement "helpers".
restriction Eq:
"All t1 t2 #x. Eq(t1, t2) @ #x ==> t1 = t2"
- Variables must start with a letter or _
- Capitalized variables must start with a capital letter or _
- Generally, Tamarin is case-sensitive and ignores repeated line breaks, spaces, or tabs
- Note: This syntax definition is not complete!
<MODEL> ::=
theory <VAR>
begin
{ <IMPORT> / <F-DEF> / <EQ-DEF> / <RULE> / <LEMMA> / <RESTRICTION> }*
end
<IMPORT> ::=
builtins: LIST{ <THEORY> }+
<F-DEF> ::=
functions: LIST{ <VAR>/<INT> }+
<EQ-DEF> ::=
equations: LIST{ <TERM> = <TERM> }+
<RULE> ::=
rule <VAR>:
{ let LIST{ <VAR> = <TERM> }+ in }?
[ LIST{ <FACT> }* ] --{[ LIST{ <ACTION-FACT> }* ]-}?> [ LIST{ <FACT> }* ]
<LEMMA> ::=
lemma <VAR>{[ LIST{ <ANNOTATION> }* ]}?:
{ exists-trace / all-traces }?
"<FORMULA>"
<RESTRICTION> ::=
restriction <VAR>:
"<FORMULA>"
<FORMULA> ::=
All LIST{ {#}?<VAR> }+. <FORMULA>
/ Ex LIST{ {#}?<VAR> }+. <FORMULA>
/ <FORMULA> & <FORMULA>
/ <FORMULA> | <FORMULA>
/ not <FORMULA>
/ <FORMULA> ==> <FORMULA>
/ <FACT> @ {#}?<VAR>
/ {#}?<VAR> < {#}?<VAR>
/ <TERM> = <TERM>
<TERM> ::=
{ ~ / $ }?<VAR>
/ '<STRING>'
/ <VAR>( LIST{ <TERM> }* )
<ACTION-FACT> ::=
{!}?<CAPITALIZED-VAR>( LIST{ <TERM> }* )
<RESERVED-FACT> ::=
Out(<TERM>) / In(<TERM>) / Fr({~}?<VAR>)
<FACT> ::=
<ACTION-FACT> / <RESERVED-FACT>
Conventions:
<P> ::= Q
defines patternP
to beQ
<P>
references patternP
P / Q
meansP
orQ
{ P }?
means optionallyP
(P
may be omitted){ P }*
means zero or more repetitions ofP
{ P }+
means one or more repetitions ofP
LIST{ P }*
means a list of zero or more repetitions ofP
, conjoined with,
, e.g.,P, P
LIST{ P }+
means a list of one or more repetitions ofP
, conjoined with,