Syntax Description

Here, we explain the formal syntax of the security protocol theory format that is processed by Tamarin.

Comments are C-style and are allowed to be nested:

/* 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.

  theory  ::=  'theory' (ident: theory_name) ('configuration' ':' '"' commandline '"')? 'begin' _body_item* 'end' /./*
  _body_item  ::=  preprocessor 
                   | _signature_spec 
                   | global_heuristic 
                   | tactic 
                   | process 
                   | let 
                   | export 
                   | _rule 
                   | restriction 
                   | case_test 
                   | _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  ::=  built_ins 
                            | functions 
                            | equations 
                            | predicates 
                            | macros 
                            | options
  _function_sym  ::=  function_untyped 
                            | function_typed
  equations  ::=  >('equations' ('[' 'convergent' ']')? ':' equation (',' equation)* ','?)
  equation  ::=  (_term: left) '=' (_term: right)

Note that the equations must be convergent and have the Finite Variant Property (FVP), and do not allow the use of fixed public names in the terms. Tamarin provides built-in sets of function definitions and 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 Section Cryptographic Messages. You need to enable it to parse terms containing exponentiations, e.g., g ^ x.

  built_ins  ::=  'builtins' ':' built_in (',' built_in)* ','?
  built_in  ::=  'diffie-hellman' 
                  | 'hashing' 
                  | 'symmetric-encryption' 
                  | 'asymmetric-encryption' 
                  | 'signing' 
                  | 'bilinear-pairing' 
                  | 'xor' 
                  | 'multiset' 
                  | 'natural-numbers' 
                  | 'revealing-signing' 
                  | 'locations-report' 
                  | 'reliable-channel' 
                  | 'dest-pairing' 
                  | 'dest-signing' 
                  | 'dest-symmetric-encryption' 
                  | 'dest-asymmetric-encryption'

A global heuristic sets the default heuristic that will be used when autoproving lemmas in the file. The specified proof method ranking can be any of those discussed in Section Heuristics.

  global_heuristic  ::=  'heuristic' ':' (_proof_method_ranking+: proof_method_ranking)
  param  ::=  /[^"]*/

The tactics allow the user to write their own heuristics based on the lemmas there are trying to prove. Their use is descibed in in Section Using a Tactic.

  tactic  ::=  'tactic' ':' ident presort? ((prio+ deprio*) 
                              | (prio* deprio+))
  presort  ::=  'presort' ':' standard_proof_method_ranking
  prio  ::=  'prio' ':' ('{' post_ranking '}')? _function+
  deprio  ::=  'deprio' ':' ('{' post_ranking '}')? _function+
  post_ranking  ::=  'smallest' 
                              | 'id'
  _function  ::=  or_function 
                              | and_function 
                              | not_function 
                              | std_function
  and_function  ::=  <LOGICAL_AND(_function '&' _function)
  not_function  ::=  LOGICAL_NOT('not' _function)
  function_name  ::=  'regex' 
                              | 'isFactName' 
                              | 'isInFactTerms' 
                              | 'dhreNoise' 
                              | 'defaultNoise' 
                              | 'reasonableNoncesNoise' 
                              | 'nonAbsurdConstraint'

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 variants can be explicitly given, as well as the left and right instances of a rule in diff-mode. (When called with --diff, Tamarin will parse diff_rule instead of rule).

  _rule  ::=  rule 
                               | diff_rule
  rule  ::=  simple_rule variants?
  diff_rule  ::=  simple_rule 'left' (rule: left) 'right' (rule: right)
  simple_rule  ::=  'rule' modulo? (ident: rule_identifier) rule_attrs? ':' rule_let_block? premise ('-->' 
                               | action_fact) conclusion
  variants  ::=  'variants' simple_rule (',' simple_rule)*
  modulo  ::=  '(' 'modulo' ('E' 
                               | 'AC') ')'
  rule_attrs  ::=  '[' rule_attr (',' rule_attr)* ','? ']'
  rule_attr  ::=  rule_attr_color 
                               | 'no_derivcheck' 
                               | 'issapicrule' 
                               | rule_process 
                               | rule_role
  rule_let_block  ::=  'let' rule_let_term+ 'in'
  rule_let_term  ::=  ((msg_var_or_nullary_fun 
                               | nat_var): left) '=' (_term: right)
  msg_var_or_nullary_fun  ::=  VARIABLE((ident: variable_identifier) ('.' natural)? (':' 'msg')?)
  hexcolor  ::=  (''' @('#')? @(/[0-9a-fA-F]{1,6}/) ''') 
                               | (@('#')? @(/[0-9a-fA-F]{1,6}/))

Rule annotations do not influence the rule’s semantics. A color is represented as a triplet of 8 bit hexadecimal values optionally preceded by ‘#’, and is used as the background color of the rule when it is rendered in graphs.

The let-block allows more succinct specifications. The equations are applied in a bottom-up fashion. For example,

let x = y
    y = <z,x>
in [] --> [ A(y)]    is desugared to    [] --> [ A(<z,y>) ]

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.

Macros works similarly to let-blocks, but apply globally to all rules.

  macros  ::=  'macros' ':' macro (',' macro)*
  macro  ::=  (ident: macro_identifier) '(' (_non_temporal_var (',' _non_temporal_var)*)? ')' '=' (_term: term)
  _non_temporal_var  ::=  pub_var 
                          | fresh_var 
                          | msg_var_or_nullary_fun 
                          | nat_var

Configuration blocks allow the specification of certain Tamarin command line options in the model file itself. Options passed over the command line override options given in a configuration block.

configuration := 'configuration' ':' '"' option (' ' option)* '"'
option          := '--auto-sources' | ('--stop-on-trace' '=' search_method)
search_method := 'DFS' | 'BFS' | 'SEQDFS' | 'NONE'

Restrictions specify restrictions on the set of traces considered, i.e., they filter the set of traces of a protocol. The formula of a restriction is available as an assumption in the proofs of all security properties specified in this security protocol theory. In observational equivalence mode, restrictions can be associated to one side.

  restriction  ::=  ('restriction' 
                         | 'axiom') (ident: restriction_identifier) restriction_attr? ':' '"' (_formula: formula) '"'
  restriction_attr  ::=  '[' ('left' 
                         | 'right') ']'

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. When exporting, one may indicate which lemmas should only be included in certain output formats.

  _lemma  ::=  lemma 
                         | diff_lemma 
                         | accountability_lemma 
                         | equiv_lemma 
                         | diff_equiv_lemma
  lemma  ::=  'lemma' modulo? (ident: lemma_identifier) diff_lemma_attrs? ':' trace_quantifier? '"' (_formula: formula) '"' (_proof_skeleton: proof_skeleton)?
  lemma_attr  ::=  'sources' 
                         | 'reuse' 
                         | 'use_induction' 
                         | ('output=' '[' language (',' language)* ']') 
                         | ('hide_lemma=' ident) 
                         | ('heuristic=' (_proof_method_ranking+: proof_method_ranking))
  trace_quantifier  ::=  'all-traces' 
                         | 'exists-trace'

In observational equivalence mode, lemmas can be associated to one side.

  diff_lemma  ::=  'diffLemma' modulo? (ident: lemma_identifier) diff_lemma_attrs? ':' (_proof_skeleton: proof_skeleton)?
  diff_lemma_attrs  ::=  '[' (diff_lemma_attr 
                         | lemma_attr) (',' (diff_lemma_attr 
                         | lemma_attr))* ','? ']'
  diff_lemma_attr  ::=  'left' 
                         | 'right'

A proof skeleton is a complete or partial proof as output by the Tamarin prover. It indicates the proof method used at each step, which may include multiple cases.

  _proof_skeleton  ::=  solved 
                               | mirrored 
                               | by_method 
                               | method_skeleton 
                               | cases
  solved  ::=  'SOLVED'
  mirrored  ::=  'MIRRORED'
  by_method  ::=  'by' _proof_methods
  method_skeleton  ::=  _proof_methods (_proof_skeleton: proof_skeleton)
  cases  ::=  case ('next' case)* 'qed'
  _proof_methods  ::=  >(proof_method 
                               | step+)
  proof_method  ::=  'sorry' 
                               | 'simplify' 
                               | ('solve' '(' constraint ')') 
                               | 'contradiction' 
                               | 'induction' 
                               | 'rule-equivalence' 
                               | 'backward-search' 
                               | 'ATTACK'
  natural  ::=  /[0-9]+/
  natural_subscript  ::=  ('₀' 
                               | '₁' 
                               | '₂' 
                               | '₃' 
                               | '₄' 
                               | '₅' 
                               | '₆' 
                               | '₇' 
                               | '₈' 
                               | '₉')+

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: comment_identifier) @('{*' /[^*]*\*+([^}*][^*]*\*+)*/ '}')

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 the grammar.

We provide special syntax for tuples, multisets, xors, multiplications, exponentiation, nullary and binary function symbols. An n-ary tuple <t1,...,tn> 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.

  _term  ::=  tuple_term 
                  | mset_term 
                  | nested_term 
                  | nullary_fun 
                  | binary_app 
                  | nary_app 
                  | _literal
  mset_term  ::=  <MUL_SET((nat_term: left) ('++' 
                  | '+') (nat_term: right))
  nat_term  ::=  <ADD((xor_term: left) '%+' (xor_term: right))
  xor_term  ::=  <EXCLUSIVE_OR((mult_term: left) ('XOR' 
                  | '⊕') (mult_term: right))
  mult_term  ::=  <MULTIPLY((exp_term: left) '*' (exp_term: right))
  exp_term  ::=  >EXPONENTIAL((_term: base) '^' (_term: exponent))

Tamarin’s parser checks that functions were previously defined and are used with the correct arity.

    nullary_fun := <all-nullary-functions-defined-up-to-here>
    binary_app  := binary_fun '{' tupleterm '}' term
    binary_fun  := <all-binary-functions-defined-up-to-here>
    nary_app    := nary_fun '(' multterm* ')'

External tools may instead use the following grammar and check these conditions after parsing.

  binary_app  ::=  FUNCTION((ident: function_identifier) '{' (_term: argument) (',' (_term: argument))*? '}' (_term: argument))
  nary_app  ::=  FUNCTION((ident: function_identifier) '(' arguments ')')

Literals and variables appear in many forms.

  _literal  ::=  pub_name 
                          | fresh_name 
                          | _non_temporal_var 
                          | comp_var 
                          | _custom_type_var
  _non_temporal_var  ::=  pub_var 
                          | fresh_var 
                          | msg_var_or_nullary_fun 
                          | nat_var

When appearing in formulas or rules, they have an identifier and a sort.

  _non_temporal_var  ::=  pub_var 
                               | fresh_var 
                               | msg_var_or_nullary_fun 
                               | nat_var
  pub_var  ::=  VARIABLE(('$' (ident: variable_identifier) ('.' natural)?) 
                               | ((ident: variable_identifier) ('.' natural)? ':' 'pub'))
  fresh_var  ::=  VARIABLE(('~' (ident: variable_identifier) ('.' natural)?) 
                               | ((ident: variable_identifier) ('.' natural)? ':' 'fresh'))
  msg_var_or_nullary_fun  ::=  VARIABLE((ident: variable_identifier) ('.' natural)? (':' 'msg')?)
  nat_var  ::=  ('%' (ident: variable_identifier) ('.' natural)? (':' 'nat')?) 
                               | ((ident: variable_identifier) ('.' natural)? ':' 'nat')
  fresh_name  ::=  '~'' /[^\n']+/ '''

SAPIC processes also have (optional) types. Moreover, literals in pattern can signify with a = if they are matched or bound.

  comp_var  ::=  '=' _literal
  _custom_type_var  ::=  custom_var 
                         | any_var
  custom_var  ::=  -1(_literal ':' (ident: variable_type))

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, Fr, 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 (',' _fact)*)
  _fact  ::=  (fact -> linear_fact) 
                     | ('!' (fact -> persistent_fact))
  fact_annotes  ::=  '[' fact_annote (',' fact_annote)* ']'
  fact_annote  ::=  '+' 
                     | '-' 
                     | 'no_precomp'

facts := fact (',' fact)*
fact  := ['!'] ident '(' [msetterm (',' msetterm)*] ')' [fact_annotes]
fact_annotes := '[' fact_annote (',' fact_annote)* ']'
fact_annote  := '+' | '-' | 'no_precomp'

Fact annotations can be used to adjust the priority of corresponding proof methods in the heuristics, or influence the precomputation step performed by Tamarin, as described in Section Advanced Features.

Formulas are trace formulas as described previously. Note that we are a bit more liberal with respect to guardedness. We accept a conjunction of atoms as guards.

formula     := imp [('<=>' | '⇔') imp]
imp         := disjunction [('==>' | '⇒') imp]
disjunction := conjunction (('|' | '∨') conjunction)* // left-associative
conjunction := negation (('&' | '∧') negation)*       // left-associative
negation    := ['not' | '¬'] atom
atom        := '⊥' | 'F' | '⊤' | 'T'           // true or false
             | '(' formula ')'                 // nested formula
             | 'last' '(' node_var ')'         // 'last' temporal variable for induction
             | fact '@' node_var               // action
             | node_var '<' node_var           // ordering of temporal variables
             | msetterm '=' msetterm           // equality of terms
             | msetterm ('<<' | '⊏') msetterm  // subterm relation
             | node_var '=' node_var           // equality of temporal variables
             | ('Ex' | '∃' | 'All' | '∀')      // quantified formula
                    lvar+ '.' formula

lvar        := node_var | nonnode_var

Identifiers always start with a letter or number, and may contain underscores after the first character. Moreover, they must not be one of the reserved keywords let, in, or rule. Although identifiers beginning with a number are valid, they are not allowed as the names of facts (which must begin with an upper-case letter).

Full syntax

The following Treesitter-generated eBNF is regularly tested against the files in examples. It includes the aforementioned rules, and those concerning the process calculus SAPIC+.

extras  ::=  { multi_comment single_comment /\s|\\\r?\n|\u00A0/ }

conflicts  ::=  { { pub_var } { fresh_var } { msg_var_or_nullary_fun } { temporal_var } { nat_var } { pub_var fresh_var msg_var_or_nullary_fun temporal_var nat_var } { pub_var fresh_var msg_var_or_nullary_fun nat_var } { accountability_lemma diff_lemma } { lemma diff_lemma } { nary_app predicate_ref } { nullary_fun nary_app msg_var_or_nullary_fun } }

externals  ::=  { multi_comment single_comment }

precedences  ::=  { { 'NESTED' 'FUNCTION' 'VARIABLE' 'EXPONENTIAL' 'MULTIPLY' 'ADD' 'MUL_SET' 'TUPLE' 'NULLARY_FUN' 'ATOM' 'LOGICAL_NOT' 'EXCLUSIVE_OR' 'LOGICAL_AND' 'LOGICAL_OR' 'LOGICAL_IMPLICATION' 'LOGICAL_IFF' 'CHAIN_CONSTRAINT' } { 'NON_DIFF' 'DIFF' } { 'REPLICATION' 'EVENT' 'CHOICE' 'PROCESS_LET' 'LOOKUP' 'CONDITIONAL' } }

word  ::=  ident

rules:
  theory  ::=  'theory' (ident: theory_name) ('configuration' ':' '"' commandline '"')? 'begin' _body_item* 'end' /./*
  commandline  ::=  ('--auto-sources' | ('--stop-on-trace' '=' _search_strategy))+
  _search_strategy  ::=  'BFS' | 'DFS' | 'SEQDFS' | 'bfs' | 'dfs' | 'seqdfs'
  _body_item  ::=  preprocessor | _signature_spec | global_heuristic | tactic | process | let | export | _rule | restriction | case_test | _lemma | formal_comment
  preprocessor  ::=  ifdef | define | include
  ifdef  ::=  '#ifdef' _ifdef_formula _body_item* ('#else' _body_item*)? '#endif'
  define  ::=  '#define' ident
  include  ::=  '#include' '"' (param -> path) '"'
  _ifdef_formula  ::=  ifdef_nested | ifdef_or | ifdef_and | ifdef_not | ident
  ifdef_nested  ::=  NESTED('(' _ifdef_formula ')')
  ifdef_or  ::=  <LOGICAL_OR(_ifdef_formula '|' _ifdef_formula)
  ifdef_and  ::=  <LOGICAL_AND(_ifdef_formula '&' _ifdef_formula)
  ifdef_not  ::=  LOGICAL_NOT('not' _ifdef_formula)
  _signature_spec  ::=  built_ins | functions | equations | predicates | macros | options
  built_ins  ::=  'builtins' ':' built_in (',' built_in)* ','?
  built_in  ::=  'diffie-hellman' | 'hashing' | 'symmetric-encryption' | 'asymmetric-encryption' | 'signing' | 'bilinear-pairing' | 'xor' | 'multiset' | 'natural-numbers' | 'revealing-signing' | 'locations-report' | 'reliable-channel' | 'dest-pairing' | 'dest-signing' | 'dest-symmetric-encryption' | 'dest-asymmetric-encryption'
  functions  ::=  >('functions' ':' _function_sym (',' _function_sym)* ','?)
  _function_sym  ::=  function_untyped | function_typed
  function_untyped  ::=  (ident: function_identifier) '/' (natural: arity) ('[' function_attribute (',' function_attribute)* ','? ']')?
  function_attribute  ::=  'private' | 'destructor'
  function_typed  ::=  (ident: function_identifier) '(' arguments? ')' ':' (ident: function_type)
  equations  ::=  >('equations' ('[' 'convergent' ']')? ':' equation (',' equation)* ','?)
  equation  ::=  (_term: left) '=' (_term: right)
  predicates  ::=  ('predicate' | 'predicates') ':' predicate (',' predicate)*
  predicate  ::=  (predicate_def -> '') '<=>' (_formula: formula)
  predicate_def  ::=  (ident: predicate_identifier) '(' arguments? ')'
  options  ::=  'options' ':' option (',' option)* ','?
  option  ::=  'translation-state-optimisation' | 'translation-progress' | 'translation-asynchronous-channels' | 'translation-compress-events' | 'translation-allow-pattern-lookups'
  global_heuristic  ::=  'heuristic' ':' (_proof_method_ranking+: proof_method_ranking)
  _proof_method_ranking  ::=  standard_proof_method_ranking | oracle_proof_method_ranking | tactic_proof_method_ranking
  standard_proof_method_ranking  ::=  /[CISPcisp][CISPcisp]?[CISPcisp]?[CISPcisp]?/
  oracle_proof_method_ranking  ::=  ('O' | 'o') ('"' param '"')?
  tactic_proof_method_ranking  ::=  '{' ident '}'
  tactic  ::=  'tactic' ':' ident presort? ((prio+ deprio*) | (prio* deprio+))
  presort  ::=  'presort' ':' standard_proof_method_ranking
  prio  ::=  'prio' ':' ('{' post_ranking '}')? _function+
  deprio  ::=  'deprio' ':' ('{' post_ranking '}')? _function+
  post_ranking  ::=  'smallest' | 'id'
  _function  ::=  or_function | and_function | not_function | std_function
  or_function  ::=  <LOGICAL_OR(_function '|' _function)
  and_function  ::=  <LOGICAL_AND(_function '&' _function)
  not_function  ::=  LOGICAL_NOT('not' _function)
  std_function  ::=  function_name ('"' param '"')*
  function_name  ::=  'regex' | 'isFactName' | 'isInFactTerms' | 'dhreNoise' | 'defaultNoise' | 'reasonableNoncesNoise' | 'nonAbsurdConstraint'
  process  ::=  'process' ':' _process
  _process  ::=  _elementary_process | _extended_process | _stateful_process | inline_msr_process | _nested_process | location_process | predefined_process
  _elementary_process  ::=  binding | output | input | conditional | process_let | deterministic_choice | non_deterministic_choice | null
  _extended_process  ::=  event | replication
  _stateful_process  ::=  set_state | delete_state | read_state | set_lock | remove_lock
  location_process  ::=  '(' _process ')' '@' ((_literal | tuple_term): location_identifier)
  inline_msr_process  ::=  >(premise ('-->' | action_fact) conclusion (';' _process)?)
  _nested_process  ::=  '(' _process ')'
  predefined_process  ::=  <-1(_term)
  binding  ::=  >('new' _literal (';' _process)?)
  output  ::=  >(('out' '(' _term ',' _term ')' (';' _process)?) | ('out' '(' _term ')' (';' _process)?))
  input  ::=  >(('in' '(' _term ',' _term ')' (';' _process)?) | ('in' '(' _term ')' (';' _process)?))
  conditional  ::=  >CONDITIONAL('if' (_condition: condition) 'then' (_process: then) ('else' (_process: else))?)
  process_let  ::=  >PROCESS_LET('let' term_eq+ 'in' (_process: in) ('else' (_process: else))?)
  deterministic_choice  ::=  <CHOICE(_process ('|' | '||') _process)
  non_deterministic_choice  ::=  <CHOICE(_process ('+') _process)
  null  ::=  '0'
  event  ::=  >EVENT('event' _fact (';' _process)?)
  replication  ::=  >REPLICATION('!' _process (';' _process)?)
  set_state  ::=  >('insert' (_term: from) ',' (_term: to) (';' _process)?)
  delete_state  ::=  >('delete' _term (';' _process)?)
  read_state  ::=  >LOOKUP('lookup' (_term: from) 'as' (_lvar: to) 'in' (_process: in) ('else' (_process: else))? (';' _process)?)
  set_lock  ::=  >('lock' _term (';' _process)?)
  remove_lock  ::=  >('unlock' _term (';' _process)?)
  _condition  ::=  equality_check | lesser_check | predicate_ref
  equality_check  ::=  (_term | _formula) @(1('=')) (_term | _formula)
  lesser_check  ::=  _term ('(<)' | '<<') _term
  let  ::=  'let' (_term: let_identifier) '=' _process
  export  ::=  'export' (ident: export_identifier) ':' '"' export_query '"'
  _rule  ::=  rule | diff_rule
  rule  ::=  simple_rule variants?
  diff_rule  ::=  simple_rule 'left' (rule: left) 'right' (rule: right)
  simple_rule  ::=  'rule' modulo? (ident: rule_identifier) rule_attrs? ':' rule_let_block? premise ('-->' | action_fact) conclusion
  premise  ::=  '[' _facts? ']'
  action_fact  ::=  '--[' _facts_restrictions? ']->'
  conclusion  ::=  '[' _facts? ']'
  variants  ::=  'variants' simple_rule (',' simple_rule)*
  modulo  ::=  '(' 'modulo' ('E' | 'AC') ')'
  rule_attrs  ::=  '[' rule_attr (',' rule_attr)* ','? ']'
  rule_attr  ::=  rule_attr_color | 'no_derivcheck' | 'issapicrule' | rule_process | rule_role
  rule_attr_color  ::=  ('color=' | 'colour=') hexcolor
  rule_role  ::=  'role' '=' '"' (ident: role_identifier) '"'
  rule_process  ::=  'process' '=' '"' ident '"'
  rule_let_block  ::=  'let' rule_let_term+ 'in'
  rule_let_term  ::=  ((msg_var_or_nullary_fun | nat_var): left) '=' (_term: right)
  macros  ::=  'macros' ':' macro (',' macro)*
  macro  ::=  (ident: macro_identifier) '(' (_non_temporal_var (',' _non_temporal_var)*)? ')' '=' (_term: term)
  embedded_restriction  ::=  '_restrict' '(' (_formula: formula) ')'
  _facts_restrictions  ::=  <((_fact | embedded_restriction) (',' (_fact | embedded_restriction))*)
  _facts  ::=  <(_fact (',' _fact)*)
  _fact  ::=  (fact -> linear_fact) | ('!' (fact -> persistent_fact))
  fact  ::=  <((ident: fact_identifier) '(' arguments? ')' fact_annotes?)
  fact_annotes  ::=  '[' fact_annote (',' fact_annote)* ']'
  fact_annote  ::=  '+' | '-' | 'no_precomp'
  restriction  ::=  ('restriction' | 'axiom') (ident: restriction_identifier) restriction_attr? ':' '"' (_formula: formula) '"'
  restriction_attr  ::=  '[' ('left' | 'right') ']'
  case_test  ::=  'test' (ident: test_identifier) ':' '"' (_formula: formula) '"'
  _lemma  ::=  lemma | diff_lemma | accountability_lemma | equiv_lemma | diff_equiv_lemma
  lemma  ::=  'lemma' modulo? (ident: lemma_identifier) diff_lemma_attrs? ':' trace_quantifier? '"' (_formula: formula) '"' (_proof_skeleton: proof_skeleton)?
  lemma_attr  ::=  'sources' | 'reuse' | 'use_induction' | ('output=' '[' language (',' language)* ']') | ('hide_lemma=' ident) | ('heuristic=' (_proof_method_ranking+: proof_method_ranking))
  language  ::=  'spthy' | 'spthytyped' | 'msr' | 'proverif' | 'deepsec'
  diff_lemma  ::=  'diffLemma' modulo? (ident: lemma_identifier) diff_lemma_attrs? ':' (_proof_skeleton: proof_skeleton)?
  diff_lemma_attrs  ::=  '[' (diff_lemma_attr | lemma_attr) (',' (diff_lemma_attr | lemma_attr))* ','? ']'
  diff_lemma_attr  ::=  'left' | 'right'
  accountability_lemma  ::=  'lemma' (ident: lemma_identifier) ':' (ident: test_identifier) (',' (ident: test_identifier))* ('account' | 'accounts') 'for' '"' (_formula: formula) '"'
  equiv_lemma  ::=  'equivLemma' ':' (_process: first) (_process: second)
  diff_equiv_lemma  ::=  'diffEquivLemma' ':' _process
  trace_quantifier  ::=  'all-traces' | 'exists-trace'
  _proof_skeleton  ::=  solved | mirrored | by_method | method_skeleton | cases
  solved  ::=  'SOLVED'
  mirrored  ::=  'MIRRORED'
  by_method  ::=  'by' _proof_methods
  method_skeleton  ::=  _proof_methods (_proof_skeleton: proof_skeleton)
  cases  ::=  case ('next' case)* 'qed'
  case  ::=  'case' (ident: case_identifier) (_proof_skeleton: proof_skeleton)
  _proof_methods  ::=  >(proof_method | step+)
  proof_method  ::=  'sorry' | 'simplify' | ('solve' '(' constraint ')') | 'contradiction' | 'induction' | 'rule-equivalence' | 'backward-search' | 'ATTACK'
  step  ::=  'step' '(' proof_method ')'
  constraint  ::=  premise_constraint | action_constraint | chain_constraint | disjunction_split_constraint | eq_split_constraint
  premise_constraint  ::=  _fact '▶' natural_subscript temporal_var
  action_constraint  ::=  ATOM((_fact: fact) '@' ((temporal_var_optional_prefix -> temporal_var): variable))
  chain_constraint  ::=  '(' temporal_var ',' natural ')' '~~>' '(' temporal_var ',' natural ')'
  disjunction_split_constraint  ::=  CHAIN_CONSTRAINT((_formula: formula) (('||' | '∥') (_formula: formula))+)
  eq_split_constraint  ::=  'splitEqs' '(' natural ')'
  _term  ::=  tuple_term | mset_term | nested_term | nullary_fun | binary_app | nary_app | _literal
  tuple_term  ::=  TUPLE('<' ((mset_term): term) (',' (mset_term: term))* '>')
  mset_term  ::=  <MUL_SET((nat_term: left) ('++' | '+') (nat_term: right))
  nat_term  ::=  <ADD((xor_term: left) '%+' (xor_term: right))
  xor_term  ::=  <EXCLUSIVE_OR((mult_term: left) ('XOR' | '⊕') (mult_term: right))
  mult_term  ::=  <MULTIPLY((exp_term: left) '*' (exp_term: right))
  exp_term  ::=  >EXPONENTIAL((_term: base) '^' (_term: exponent))
  nested_term  ::=  NESTED('(' mset_term ')')
  nullary_fun  ::=  NULLARY_FUN((ident: function_identifier) | ((ident: function_identifier) '(' ')'))
  binary_app  ::=  FUNCTION((ident: function_identifier) '{' (_term: argument) (',' (_term: argument))*? '}' (_term: argument))
  nary_app  ::=  FUNCTION((ident: function_identifier) '(' arguments ')')
  arguments  ::=  ((_term | temporal_var): argument) (',' (_term: argument))*
  _literal  ::=  pub_name | fresh_name | _non_temporal_var | comp_var | _custom_type_var
  _non_temporal_var  ::=  pub_var | fresh_var | msg_var_or_nullary_fun | nat_var
  pub_var  ::=  VARIABLE(('$' (ident: variable_identifier) ('.' natural)?) | ((ident: variable_identifier) ('.' natural)? ':' 'pub'))
  fresh_var  ::=  VARIABLE(('~' (ident: variable_identifier) ('.' natural)?) | ((ident: variable_identifier) ('.' natural)? ':' 'fresh'))
  msg_var_or_nullary_fun  ::=  VARIABLE((ident: variable_identifier) ('.' natural)? (':' 'msg')?)
  temporal_var  ::=  ('#' (ident: variable_identifier) ('.' natural)?) | ((ident: variable_identifier) ('.' natural)? ':' 'node')
  nat_var  ::=  ('%' (ident: variable_identifier) ('.' natural)? (':' 'nat')?) | ((ident: variable_identifier) ('.' natural)? ':' 'nat')
  comp_var  ::=  '=' _literal
  _custom_type_var  ::=  custom_var | any_var
  custom_var  ::=  -1(_literal ':' (ident: variable_type))
  any_var  ::=  -1(_literal ':' 'ANY')
  temporal_var_optional_prefix  ::=  NULLARY_FUN(('#'? (ident: variable_identifier) ('.' natural)?) | ((ident: variable_identifier) ('.' natural)? ':' 'temporal'))
  pub_name  ::=  ''' /[^\n']+/ '''
  fresh_name  ::=  '~'' /[^\n']+/ '''
  _formula  ::=  iff | imp | disjunction | conjunction | negation | nested_formula | _temporal_variable_operation | action_constraint | term_eq | subterm_rel | quantified_formula | atom | predicate_ref | pre_defined
  iff  ::=  <LOGICAL_IFF((_formula: left) ('<=>' | '⇔') (_formula: right))
  imp  ::=  <LOGICAL_IMPLICATION((_formula: left) (@(1('==>')) | '⇒') (_formula: right))
  disjunction  ::=  <LOGICAL_OR((_formula: left) ('|' | '∨') (_formula: right))
  conjunction  ::=  <LOGICAL_AND((_formula: left) ('&' | '∧') (_formula: right))
  negation  ::=  LOGICAL_NOT(('not' | '¬') (_formula: formula))
  nested_formula  ::=  ATOM('(' _formula ')')
  _temporal_variable_operation  ::=  temp_var_induction | temp_var_order | temp_var_eq
  temp_var_induction  ::=  ATOM('last' '(' temporal_var ')')
  temp_var_order  ::=  ATOM(((temporal_var_optional_prefix -> temporal_var): left) '<' ((temporal_var_optional_prefix -> temporal_var): right))
  temp_var_eq  ::=  ATOM(((temporal_var_optional_prefix -> temporal_var): left) '=' ((temporal_var_optional_prefix -> temporal_var): right))
  term_eq  ::=  ATOM((_term: left) '=' (_term: right))
  subterm_rel  ::=  ATOM((_term: left) ('<<' | '⊏') (_term: right))
  quantified_formula  ::=  ATOM(('Ex' | '∃' | 'All' | '∀') (_lvar+: variable) '.' (_formula: formula))
  atom  ::=  ATOM('⊥' | 'F' | '⊤' | 'T')
  _lvar  ::=  temporal_var | _non_temporal_var
  predicate_ref  ::=  FUNCTION((ident: predicate_identifier) '(' arguments? ')')
  pre_defined  ::=  NULLARY_FUN(ident)
  hexcolor  ::=  (''' @('#')? @(/[0-9a-fA-F]{1,6}/) ''') | (@('#')? @(/[0-9a-fA-F]{1,6}/))
  ident  ::=  /[A-Za-z0-9][a-zA-Z0-9_*]*/
  param  ::=  /[^"]*/
  export_query  ::=  /(\\"|[^"])*/
  natural  ::=  /[0-9]+/
  natural_subscript  ::=  ('₀' | '₁' | '₂' | '₃' | '₄' | '₅' | '₆' | '₇' | '₈' | '₉')+
  formal_comment  ::=  (ident: comment_identifier) @('{*' /[^*]*\*+([^}*][^*]*\*+)*/ '}')