User manual for the Tamarin prover ================================== Date: 2012/06/04 Authors: Simon Meier , Benedikt Schmidt Installation ============ See http://www.infsec.ethz.ch/research/software#TAMARIN for detailed installation instructions for Linux and Mac. The Tamarin prover also runs on Windows. Drop us a mail, if you would like access to a precompiled binary. Syntax highlighting ------------------- We provide syntax highlighting files for the 'vim' text editor. Here, we describe how to install them. Let DATA_PATH be the parent directory of the examples directory output in Tamarin's help message. The 'vim' syntax highlighting files are found at DATA_PATH/etc/ To install them, copy 'DATA_PATH/etc/filepath.vim' to the '~/.vim' directory and copy 'DATA_PATH/etc/spthy.vim' to the '~/.vim/syntax directory'. If one of these directories does not exist, then just create it. Usage ===== Once you have installed the 'tamarin-prover' executable, calling it without any arguments will print a help message explaining its different modes and the paths to example files. We suggest that you first have a look at the 'Tutorial.spthy' file referenced there. Once, you have done that, you probably want to start modeling your own protocols. We normally use the following workflow to do that. 1. Copy the example protocol that is most similar to the one your are modeling. Let us assume that this copy is named 'myproto.spthy'. 2. Modify the protocol piece by piece and call 'tamarin-prover myproto.spthy' to ensure that it still parses and all well-formedness checks pass. This way you get immediate feedback on your changes. Moreover, you can see the expansions of syntactic sugar like the built-in signatures for hashing or asymmetric encryption. 3. Once you are satisfied with your model, check if the automated prover succeeds in analyzing your protocol by calling 'tamarin-prover myproto.spthy --prove' 4. If the Tamarin prover does not terminate, then you can either bound the proof-depth using the '--bound' flag or you can switch to the interactive GUI to analyze what is going wrong. Call 'tamarin-prover interactive myproto.spthy' and try to construct the proof interactively. If you want to bound the proof depth of the autoprover in interactive mode, you can call the Tamarin prover as follows. 'tamarin-prover interactive myproto.spthy --bound=7' Note that you can also use the GUI to sanity check your model. Just go through the message theory and check that it really models what you intent to model. Moreover, the precomputed case distinctions, described below, give a good overview about the behaviour/specification of your protocol. If something is wrong with your model, then it is likely that you can see it already from the precomputed case distinctions. Additional Theory ================= Most of the theory behind the Tamarin prover is described in our CSF 2012 paper, whose extended version is available from http://www.infsec.ethz.ch/research/software#TAMARIN The implementation exploits a slightly more restricted definition of normal dependency graphs and adapted versions of the constraint solving rules that also allow security properties to refer to the conclusions of normal construction rules. A technical report documenting this version of the constraint solver is under preparation. From a usage perspective, the changes are minor and explained below in the sections on `Induction` and `Typing Invariants over the Extended Traces`. Moreover, we added a constraint solving rule that allows to reason about protocols that make use of exclusive access to linear facts. A typical example is 'loops/Minimal_Create_Use_Destroy.spthy'. The corresponding constraint reduction rule is explained below. Apart from the above changes to the constraint solving rules, we also refined the theory in two ways that allow to share work between different constraint reduction steps. First, we store multiple constraint reduction steps in the form of *precomputed case distinctions*. Second, we delay the enumeration of the finite variants of multiset rewriting rules using an *equation store*. We explain both of these refinements below. Precomputed Case Distinctions ----------------------------- Apart from unification, the most common step performed by Tamarin is the enumeration of the possible origins of an open premise. Most of these backwards steps result in a number of trivial further constraint reduction steps being applied immediately. Instead of applying them over and over during proof/counter-example construction, we precompute the result of doing one backwards step and use the resulting precomputed case distinctions during proof/counter-example search. This precomputation is sound because the applicability of all our constraint reduction rules is invariant under set union and instantiation. We precompute cases for an arbitrary instance of every protocol fact and every outermost constructor of a message. Inductive Strengthening ----------------------- The normal form conditions that we impose on dependency graphs can be seen as a strong invariant on security protocol execution. As we have shown in our case studies many security properties follow from these normal form conditions. For some protocols, we must however strengthen security properties before being able to prove them using our backwards reasoning technique. This strengthening works by transforming the security property according to the induction scheme associated with the set of traces of a protocol. Intuitively, this strengthening amounts to searching for traces that violate the security property, but do not contain any prefix that violates the security property. Stated differently, we focus on first violations of security properties with respect to the prefix-order on traces. Properties that should be proven using induction can be marked with the attribute [use_induction]. In the interactive GUI, one can just select `induction` as a proof method provided the constraint system contains just one guarded trace property. For examples of protocols where inductive strengthening is required for a successful proof, see the directories `examples/loops` and `examples/related_work`. Typing Invariants over the Extended Traces ------------------------------------------ Note that every protocol communicating via the public network/adversary implicitly contains loops. The adversary may send messages received from a later step of one instance a role to an earlier step of another instance of the same role. These loops manifest themselves during backwards reasoning as infinite proof branches. For trivial loops where all messages are also received as plain-text, we can prune these branches using the constraint reduction rule N6. To prune more complicated loops, e.g., loops stemming from receiving an encrypted message and sending out some of its contents, we need so called typing invariants. A typing invariant specifies the possible instantiations of a message variable sent to the adversary. We describe these instantiations by relating an action logging the instantiation in the rule sending the variable to actions logging the possible instantiations in the rules sending the contents of this variable. See the 'classic/NSLPK3.spthy' file for an example of a typing invariant. To enable the specification of the case that the intruder constructed the message that a variable is instantiated with, we changed every construction rule such that a KU-action logs the rule's conclusion. Properties referring to this KU-actions can only be evaluated over the traces of normal dependency graphs of a protocol. We call these traces the 'extended traces of a protocol'. Note that we cannot transfer the validity of properties over extended traces to the validity of these properties over standard traces stemming from the multiset rewriting semantics. However, we can use these properties over extended traces as lemmas during the proof of a property over standard traces using the lemma attribute [reuse] or [typing]. The goal of typing invariants is to ensure that all chain-constraints are solved during the precomputation of the case distinctions. We use a two-step process to achieve this. We first precompute the so-called *untyped case distinctions* without the assumption of the validity of any typing invariant. These untyped precomputed case are used during the proof of a typing invariant. We then use the typing invariants to refine the untyped case distinctions to typed case distinctions. They are used during the proofs of properties other than typing invariants. In the input file, all typing invariants are marked with the [typing] attribute. In the GUI, you can inspect both the untyped and typed precomputed case distinctions. A typing invariant achieves its goal, if the typed precomputed case distinctions are marked with "all chains solved". Reasoning about Exclusivity --------------------------- We say that a fact symbol 'f' has `unique instances with respect to a security protocol 'P', if all instances of 'f' occur with cardinality <= 1 in all reachable states of 'P'. As computing the set of fact symbols with unique instances with respect to a security protocol 'P' is undecidable, we use a simple under-approximation to this set. We gather all linear fact symbols that occur in all conclusions either as a copy of themselves or a copy of the term of a Fr-fact. For facts with unique instances, we can use a further constraint reduction rule. This rule states that it is impossible that there is a node 'i' with a premise with a unique fact instance and an edge with the same fact instance from a node 'j' to a node 'k' such that 'j' < 'i' < 'k'. Together with inductive strengthening, this simple construction suffices for many protocols to reason about their exclusive use of a linear fact symbol to model locked access to a resource. Equation Store -------------- We store equations in a special form to allow delaying case splits on them. This allows for example to determine the shape of a signed message without case splitting on its variants. In the GUI, you can see the equation store being pretty printed as follows. free-substitution 1. fresh-substitution-group ... n. fresh substitution-group The free-substitution represents the equalities that hold for the free variables in the constraint system in the usual normal form, i.e., a substitution. The variants of a protocol rule are represented as a group of substitutions mapping free variables of the constraint system to terms containing only fresh variables. The different fresh-substitutions in a group are interpreted as a disjunction. Logically, the equation store represents expression of the form x_1 = t_free_1 & ... & x_n = t_free_n & ( (Ex y_111 ... y_11k. x_111 = t_fresh_111 & ... & x_11m = t_fresh_11m) | ... | (Ex y_1l1 ... y_1lk. x_1l1 = t_fresh_1l1 & ... & x_1lm = t_fresh_1lm) ) & .. & ( (Ex y_o11 ... y_o1k. x_o11 = t_fresh_o11 & ... & x_o1m = t_fresh_o1m) | ... | (Ex y_ol1 ... y_olk. x_ol1 = t_fresh_ol1 & ... & x_1lm = t_fresh_1lm) ) Security Protocol Theories ========================== A security protocol theory specifies a signature, an equational theory, a security protocol, and several lemmas, which formalize security properties. The paper explaining the theory behind Tamarin has been published at CSF 2012 and its extended version is available from http://www.infsec.ethz.ch/research/software#TAMARIN Here, we explain the formal syntax of the security protocol theory format that is processed by Tamarin. We recommend first reading the 'Tutorial.spthy' example before delving into the following section. Comments are C-style: /* for a multi-line comment */ // for a line-comment All security protocol theory are named and delimited by 'begin' and 'end'. We explain the non-terminals of the body in the following paragraphs. security_protocol_theory := 'theory' ident 'begin' body 'end' body := (signature_spec | rule | lemma | formal_comment)+ Here, we use the term signature more liberally to denote both the defined function symbols and the equalities describing their interaction. Note that our parser is stateful and remembers what functions have been defined. It will only parse function applications of defined functions. signature_spec := functions | equations | built_in functions := 'functions' ':' (ident '/' arity) list equations := 'equations' ':' (term '=' term) list arity := digit+ Note that the equations must be subterm-convergent. Tamarin provides built-in sets of function definitions and subterm convergent equations. They are expanded upon parsing and you can therefore inspect them by pretty printing the file using 'tamarin-prover your_file.spthy'. The built-in 'diffie-hellman' is special. It refers to the equations given in the paper. You need to enable it to parse terms containing exponentiations, e.g., g ^ x. built_in := 'builtins' ':' built_ins list built_ins := 'diffie-hellman' | 'hashing' | 'symmetric-encryption' | 'asymmetric-encryption' | 'signing' Multiset rewriting rules are specified as follows. The protocol corresponding to a security protocol theory is the set of all multiset rewriting rules specified in the body of the theory. rule := 'rule' ident ':' [let_block] '[' facts ']' ( '-->' | '--[' facts ']->') '[' facts ']' let_block := 'let' (ident '=' term)+ 'in' The let-block allows more succinct specifications. The equations are applied in a bottom-up fashion. For example, let x = y y = in [] --> [ A(y)] is desugared to [] --> [ A() ] This becomes a lot less confusing if you keep the set of variables on the left-hand side separate from the free variables on the right-hand side ;-) Lemmas specify security properties. By default, the given formula is interpreted as a property that must hold for all traces of the protocol of the security protocol theory. You can change this using the 'exists-trace' trace quantifier. lemma := 'lemma' ident [lemma_attrs] ':' [trace_quantifier] '"' formula '"' lemma_attrs := '[' ('typing' | 'reuse' | 'use_induction') ']' trace_quantifier := 'all-traces' | 'exists-trace' Formal comments are used to make the input more readable. In contrast to /*...*/ and //... comments, formal comments are stored and output again when pretty-printing a security protocol theory. formal_comment := ident '{*' ident* '*}' For the syntax of terms, you best look at our examples. A common pitfall is to use an undefined function symbol. This results in an error message pointing to a position slightly before the actual use of the function due to some ambiguity in our grammar. We provide special syntax for tuples, multiplications, exponentiation, nullary and binary function symbols. An n-ary tuple is parsed as n-ary, right-associative application of pairing. Multiplication and exponentiation are parsed left-associatively. For a binary operator 'enc' you can write 'enc{m}k' or 'enc(m,k)'. For nullary function symbols, there is no need to write 'nullary()'. Note that the number of arguments of an n-ary function application must agree with the arity given in the function definition. tupleterm := multterm list multterm := expterm ('*' expterm)* expterm := term ('^' term )* term := '<' tupleterm '>' // n-ary right-associative pairing | '(' multterm ')' // a nested term | nullary_fun | binary_app | nary_app | literal nullary_fun := binary_app := binary_fun '{' tupleterm '}' term binary_fun := nary_app := nary_fun '(' multterm* ')' literal := "'" ident "'" // a fixed, public name | '$' ident // a variable of sort 'pub' | "~'" ident "'" // a fixed, fresh name | "~" ident // a variable of sort 'fresh' | "#" ident // a variable of sort 'temp' | ident // a variable of sort 'msg' Facts do not have to be defined up-front. This will probably change once we implement user-defined sorts. Facts prefixed with '!' are persistent facts. All other facts are linear. There are six reserved fact symbols: In, Out, KU, KD, and K. KU and KD facts are used for construction and deconstruction rules. KU-facts also log the messages deduced by construction rules. Note that KU-facts have arity 2. Their first argument is used to track the exponentiation tags. See the 'loops/Crypto_API_Simple.spthy' example for more information. facts := fact list fact := ['!'] ident '(' multterm list ')' Formulas are trace formulas as described in our paper. Note that we are a bit more liberal with respect to guardedness. We accept a conjunction of atoms as guards. formula := atom | '(' iff ')' | ( 'All' | 'Ex' ) ident+ '.' iff iff := imp '<=>' imp imp := disjuncts '==>' disjuncts disjuctions := conjuncts ('|' disjuncts)+ // left-associative conjuncts := negation ('|' disjuncts)+ // left-associative negation := 'not' formula atom := tvar '<' tvar // ordering of temporal variables | '#' ident '=' '#' ident // equality between temporal variables | multterm '=' multterm // equality between terms | fact '@' tvar // action | 'T' // true | 'F' // false | '(' formula ')' // nested formula // Where unambiguous the '#' sort prefix can be dropped. tvar := ['#'] ident Identifiers always start with a character. Moreover, they must not be one of the reserved keywords 'let', 'in', or 'rule'. ident := alpha (alpha | digit)* Developing Tamarin ================== The Tamarin prover is under active development. We are grateful to receive bug-reports at 'https://github.com/tamarin-prover/tamarin-prover/issues'. If you consider building on top of Tamarin, then you might consider integrating your idea into the main source repository. Please feel free to contact us such that we can discuss the next steps towards fully verified systems :-)