/*
Tutorial for the Tamarin prover for security protocol analysis
==============================================================

Authors: 	Simon Meier, Benedikt Schmidt
Date: 	        September 2012


Introduction
------------

This user guide assumes that you have a copy of the submitted draft of Meier's
PhD thesis, which is  available from
http://www.infsec.ethz.ch/research/software/tamarin.

The input files for the Tamarin prover have the extension .spthy, which is
short for 'security protocol theory'. A security protocol theory specifies

  1. the signature and equational theory to use for the message algebra,
  2. the set of multiset rewriting rules modeling the protocol and
     the adversary capabilities, and
  3. the guarded trace properties whose satisfiability or validity we wish to
     check for this set of multiset rewriting rules.

We explain each of these parts where they occur in the following security
protocol theory. Before we start, let us add a few notes on the syntax.
As you probably noticed, comments are C-style. All identifiers are
case-sensitive. The parser is layout-insensitive, i.e., your are free to use
whitespace as it suits you. We provide a complete specification of the input
syntax in the REFERENCE MANUAL (available at doc/MANUAL.md).


Modeling a security protocol
----------------------------

Every security protocol theory starts with a header of the following form.
*/

theory Tutorial
begin

/*
Obviously, you can replace 'Tutorial' with any name you like to give
your theory. After 'begin', you can declare function symbols,
equations that they must satisfy, multiset rewriting rules, and lemmas
specifying security properties. Moreover, you can also insert formal
comments, to structure your theory. We give examples of each of these
elements while modeling a simple protocol.

In this protocol, a client C generates a fresh symmetric key 'k', encrypts it
with the public key of a server 'S' and sends it to 'S'. The server confirms
the receipt of the key by sending back its hash to the client. In
Alice-and-Bob notation the protocol would read as follows.

  C -> S: aenc{k}pk(S)
  C <- S: h(k)

This protocol is artificial and it satisfies only very weak security
guarantees. We can prove that from the perspective of the client, the freshly
generated key is secret provided that the server is uncompromised.

We model this protocol in three steps. First, we declare the function symbols
and the equations defining them. Then, we introduce multiset rewriting rules
modeling a public key infrastructure (PKI) and the protocol. Finally, we state
the expected security properties.


Function Signature and Equational Theory
----------------------------------------

We model hashing using the unary function 'h'.
We model asymmetric encryption by declaring
  a binary function 'aenc' denoting the encryption algorithm,
  a binary function 'adec' denoting the decryption algorithm, and
  a unary function 'pk' denoting the algorithm computing a public
  key from a private key.
*/

functions: h/1, aenc/2, adec/2, pk/1
equations: adec(aenc(m, pk(k)), k) = m

/*
The above equation models the interaction between calls to these three
algorithms. All such user-specified  equations must be subterm-convergent
rewriting rules, when oriented from left to right. This means that the
right-hand-side must be a subterm of the left-hand-side or a nullary
function symbol.

Certain equational theories are used very often when modeling
cryptographic messages. We therefore provide builtins definitions for
them, using the keyword 'builtins'. The above theory could also be
enabled using the declaration

  builtins: hashing, asymmetric-encryption

We support the following builtins theories:

  diffie-hellman, signing, asymmetric-encryption, symmetric-encryption,
  hashing

Note that the theory for hashing only introduces the function symbol 'h/1'
and contains no equations.
Apart from 'diffie-hellman', all of these theories are subterm-convergent and
can therefore also be declared directly, as above. You can inspect their
definitions by uncommenting the following two line-comments and calling

  tamarin-prover Tutorial.spthy

*/

// builtins: diffie-hellman, signing, asymmetric-encryption, symmetric-encryption,
//          hashing

/*
The call 'tamarin-prover Tutorial.spthy' parses the Tutorial.spthy file,
computes the variants of the multiset rewriting rules, checks their
wellformedness (explained below), and pretty-prints the theory. The
declaration of the signature and the equations can be found at the top of the
pretty-printed theory.

Proving all lemmas contained in the theory is as simple as adding the
flag '--prove' to the call; i.e.,

  tamarin-prover Tutorial.spthy --prove

However, let's not go there yet. We first have to model the PKI and our
protocol.


Modeling the Public Key Infrastructure
--------------------------------------
*/

// Registering a public key
rule Register_pk:
  [ Fr(~ltk) ]
  -->
  [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]

/* The above rule models registering a public key. It makes use of the
   following syntax.

   Facts always start with an upper-case letter and do not have to be declared.
   If their name is prefixed with an exclamation mark '!', then they are
   persistent. Otherwise, they are linear. Note that you must use every fact
   name consistently; i.e., you must always use it with the same arity, casing,
   and multiplicity. Otherwise, the tamarin prover complains that the theory
   is not wellformed.

   The 'Fr' fact is a builtins fact. It denotes a freshly generated fresh name.
   See the paper for details.

   We denote the sort of variables using prefixes:

     ~x  denotes  x:fresh
     $x  denotes  x:pub
     #i  denotes  i:temporal
     i   denotes  i:msg

     'c' denotes a public name 'c \in PN'; i.e., a fixed, global constant

   Thus, the above rule can be read as follows. First, freshly generate a
   fresh name 'ltk', the new private key and nondeterministically choose a
   public name 'A', the agent for which we are generating the key-pair.
   Then, generate the persistent fact !Ltk($A, ~ltk), which denotes the
   association between agent 'A' and its private key 'ltk, and generate the
   persistent fact !Pk($A, pk(~ltk)), which denotes the association between the
   agent 'A' and its public key 'pk(~ltk)'.

   We allow the adversary to retrieve any public key using the following rule.
   Intuitively, it just reads a public-key database entry and sends the public
   key to the network using the builtins fact 'Out' denoting a message sent to
   the network. See our paper for more information.
*/

rule Get_pk:
  [ !Pk(A, pk) ]
  -->
  [ Out(pk) ]

/*
   We model the dynamic compromise of long-term private keys using the following
   rule. Intuitively, it reads a private-key database entry and sends it to
   the adversary. This rule has an observable 'LtkReveal' action stating that
   the long-term key of agent 'A' was compromised. We will use this action in
   the security property below to determine which agents are compromised.
*/

rule Reveal_ltk:
    [ !Ltk(A, ltk) ]
  --[ LtkReveal(A) ]->
    [ Out(ltk) ]


/*

Modeling the protocol
----------------------

Recall that we want to model the following protocol.

  C -> S: aenc{k}pk(S)
  C <- S: h(k)

We model it using the following three rules.
*/

// Start a new thread executing the client role, choosing the server
// non-deterministically.
rule Client_1:
    [ Fr(~k)         // choose fresh key
    , !Pk($S, pkS)   // lookup public-key of server
    ]
  -->
    [ Client_1( $S, ~k )       // Store server and key for next step of thread
    , Out( aenc{'1', ~k}pkS )  // Send the encrypted session key to the server
                               // We add the tag '1' to the request to allow
                               // the server to check whether the decryption
                               // was successful.
    ]

rule Client_2:
    [ Client_1(S, k)   // Retrieve server and session key from previous step
    , In( h(k) )       // Receive hashed session key from network
    ]
  --[ SessKeyC( S, k ) ]-> // State that the session key 'k'
    []                     // was setup with server 'S'

// A server thread answering in one-step to a session-key setup request from
// some client.
rule Serv_1:
    [ !Ltk($S, ~ltkS)                          // lookup the private-key
    , In( request )                            // receive a request
    ]
  --[ Eq(fst(adec(request, ~ltkS)), '1')
    , AnswerRequest($S, snd(adec(request, ~ltkS)))   // Explanation below
    ]->
    [ Out( h(snd(adec(request, ~ltkS))) ) ]    // Return the hash of the
                                               // decrypted request.

/* Above, we model all applications of cryptographic algorithms explicitly.
   Call 'tamarin-prover Tutorial.spthy' to inspect the finite variants of the
   Serv_1 rule, which list all possible interactions of the destructors used.
   In our proof search, we will consider all these interactions.

   We also model that the server explicitly checks that the first component of
   the request is equal to '1'. We  model this by logging the claimed equality
   and then adapting the security property such that it only considers traces
   where all 'Eq' actions occur with two equal arguments. Note that 'Eq' is NO
   builtin fact. Guarded trace properties are strong enough to formalize this
   requirement without builtin support. Note that inequalities can be modeled
   analogously.

   We log the session-key setup requests received by servers to allow
   formalizing the authentication property for the client.


Modeling the security properties
--------------------------------

The syntax for specifying security properties uses

  All      for universal quantification, temporal variables are prefixed with #
  Ex       for existential quantification, temporal variables are prefixed with #
  ==>      for implication
  &        for conjunction
  |        for disjunction
  not      for  negation

  f @ i    for action constraints, the sort prefix for the temporal variable 'i'
           is optional

  i < j    for temporal ordering, the sort prefix for the temporal variables 'i'
           and 'j' is optional

  #i = #j  for an equality between temporal variables 'i' and 'j'
  x = y    for an equality between message variables 'x' and 'y'

Note that apart from public names (delimited using single-quotes), no terms
may occur in guarded trace properties. Moreover, all variables must be
guarded. The error message for an unguarded variable is currently not very
good.

For universally quantified variables, one has to check that they all occur in
an action constraint right after the quantifier and that the outermost logical operator
inside the quantifier is an implication.
For existentially quantified variables, one has to check that they all occur in
an action constraint right after the quantifier and that the outermost logical
operator inside the quantifier is a conjunction.
Note also that currently the precedence of the logical connectives is not
specified. We therefore recommend to use parentheses, when in doubt.
*/

/*
Note that you can specify additional restrictions that restrict the set of
considered traces. In this example, we restrict our attention to traces where
all equality checks succeed. */

restriction Equality_Checks_Succeed: "All x y #i. Eq(x,y) @ i ==> x = y"

/*
The following two properties should be self-explanatory.
Note that the order between restrictions and lemmas does not matter. All restrictions are
always available/assumed in the proofs of all security properties.
*/

lemma Client_session_key_secrecy:
  " /* It cannot be that a  */
    not(
      Ex S k #i #j.
        /* client has set up a session key 'k' with a server'S' */
        SessKeyC(S, k) @ #i
        /* and the adversary knows 'k' */
      & K(k) @ #j
        /* without having performed a long-term key reveal on 'S'. */
      & not(Ex #r. LtkReveal(S) @ r)
    )
  "


lemma Client_auth:
  " /* For all session keys 'k' setup by clients with a server 'S' */
    ( All S k #i.  SessKeyC(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. AnswerRequest(S, k) @ a)
         /* or the intruder performed a long-term key reveal on 'S'
            before the key was setup. */
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

/*
Note that we can also strengthen the authentication property to a version of
injective authentication. Our formulation is stronger than the standard
formulation of injective authentication, as it is based on uniqueness instead
of counting. For most protocols, that guarantee injective authentication one
can also prove such a uniqueness claim, as they agree on appropriate fresh
data.
*/

lemma Client_auth_injective:
  " /* For all session keys 'k' setup by clients with a server 'S' */
    ( All S k #i.  SessKeyC(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. AnswerRequest(S, k) @ a
           /* and there is no other client that had the same request */
           & (All #j. SessKeyC(S, k) @ #j ==> #i = #j)
       )
         /* or the intruder performed a long-term key reveal on 'S'
            before the key was setup. */
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

/*
  You can verify them by calling

    tamarin-prover --prove Tutorial.spthy

  This will first output some logging from the constraint solver and then the
  Tutorial security protocol theory with the lemmas and their attached
  (dis)proofs.

  Note that when adding inconsistent restrictions, you can prove any property. To
  check that there still exist traces, you can state an 'exists-trace' lemma.
  When modeling protocols such existence proofs are very useful sanity checks.

  The following property must be provable, as otherwise there would be no
  possibility to setup a session key with a honest sever.
*/

lemma Client_session_key_honest_setup:
  exists-trace
  " Ex S k #i.
        SessKeyC(S, k) @ #i
      & not(Ex #r. LtkReveal(S) @ r)
  "

/*

Interactive proof visualization and construction
------------------------------------------------

Just call

  tamarin-prover interactive Tutorial.spthy

This will start a web-server that loads all security protocol theories in the
same directory as Tutorial.spthy. Point your browser to

  http://localhost:3001

and explore the the Tutorial theory interactively by clicking on the
'Tutorial' entry in the table of loaded theories. You can prove a lemma
interactively by clicking on the available proof methods (corresponding to
applications of constraint reduction rules) or by calling the 'autoprover' by
right-clicking on a node in the theory overview. Note that that the proof
methods in the GUI are sorted according to our heuristic. Always selecting the
first proof method will result in the same proof as the ones constructed by
the 'autoprover' and '--prove'.


Conclusion
----------

By now, you should have enough knowledge to understand the case studies
included with Tamarin. Recall that you can find them in the directory listed
at the bottom of the help message, when calling 'tamarin-prover' without any
arguments. Note that Tamarin also outputs the path to the reference MANUAL
specifying and explaining the grammar of security protocol theories and giving
some additional hints on additional theory exploited by Tamarin. If you have
further questions, please do not hesitate to contact either

  Benedikt Schmidt    benedikt.schmidt@inf.ethz.ch
  Simon Meier         iridcode@gmail.com
  Cas Cremers         cas.cremers@cs.ox.ac.uk


BTW, every security protocol theory must be delimited with 'end'.

             (-: HAPPY PROVING :-)
*/

end