Artificial.spthy

theory Artificial
begin

/*
   Protocol:	Example
   Modeler: 	Simon Meier, Benedikt Schmidt
   Date: 	January 2012
  
   Status: 	working
  
   This is the artificial protocol from our CSF'12 paper, which we use to
   illustrate constraint solving and characterization. Note that, for
   characerization, you have to call the tamarin-prover as follows.

    tamarin-prover --prove --stop-on-attack=NONE your_protocol.spthy

   The --stop-on-attack=NONE flag ensures that all solved constraint systems
   are explored by the constraint solver. By default, it stops as soon as the
   first attack is found. Note that depending on the protocol,
   characterization might take a long time, as there are many slightly
   different possible attacks.

   As a more interesting example try characterizing the setup of a session-key
   between two honest agents in the TLS.spthy example, which models a TLS
   handshake using signatures.

     tamarin-prover --prove --stop-on-attack=NONE TLS.spthy +RTS -N

   Note that we add the +RTS -N to tell the Haskell runtime system that it
   should use as many cores as your system provides. For TLS, this speeds-up
   the proof generation/characterization quite a bit. After this call, the
   tool will output the complete set of cases, which it had to explore for
   finding all counter-examples to this property. Exactly, two of the cases
   will be of the form

     SOLVED (trace found)

   They correspond to the _only_ two ways of setting up a session-key between
   honest agents: one for the client and one for the server.

 */

builtin: symmetric-encryption

rule Step1:
  [ Fr(~x), Fr(~k) ] 
  --> 
  [ St(~x, ~k), Out(senc{~x}~k), Key(~k) ]

rule Step2:
  [ St(x, k), In(<x,x>) ] 
  --[ Fin(x, k) ]-> 
  [ ]

rule Reveal_key:
    [ Key(k) ]
  --[ Rev(k) ]->
    [ Out(k) ]

lemma Characterize_Fin:
  "not( Ex k S #i.  Fin(S, k) @ i )
  "

end