In the second part of the course we studied a static analysis
technique (control flow analysis) for proving secrecy/forward secrecy
properties on crypto protocols. We used a tool in the lab (Rewrite)
which performed this analysis.

Typical exam exercises on this part are about running the analysis
technique "on paper". Of course, a computer is able to run algorithms
much faster than a human, so exercises will not be about the analysis
of a full real-world protocol, but on small excerpts which can be
handled on paper. Below, I mention a few examples.

*** Formalization Exercise

Consider the following protocol excerpt.  Alice (A) and Bob (B) share
a symmetric key K.  A generates a fresh symmetric key K2, encrypts it
with K, and sends it to B.  B receives K, generates a random number N,
and sends its encryption with K2 to A.  A then sends to B the hash of
N.

Formalize the above protocol steps using the applied-pi notation.

(End of the exercise)

I will not be picky on requiring the exact syntax, but your answer
must be clear and not ambiguous. I would expect something like the
following.

new K .
   ( # Alice
     new K2 . out enc(K2,K) . in X . out hash(dec(X,K2)) . ()
   | # Bob
     in Y . let K2 = dec(Y,K) . new N . out enc(N,K2) . ()
   )


*** Tree Automaton Generation Exercise

Consider the following specification

  ( new K . out cons(cons(K,1),2) . ()
  | ! . in X . out fst(X) . ()
  )

Generate a tree automaton representing an over approximation for the
sets of messages exchanged by the above code, as done by the control
flow analysis, by running the function gen(...) on it. Specify the
states of the resulting automaton (the "@x" labels ) as well as its
transitions (@x -> f(@y)).

(End of exercise)

I will not require you to name the @x labels exactly as gen() does, or
even generating exactly the same transitions, but you have to provide
an automaton which is correct and can be easily related to the
specification. For instance, the following would be acceptable even if
the actual gen()-generated automaton is slightly different.

  @K_bar -> K , next(@K_bar)
  @K -> val(@K_bar)
  @out-above -> cons(cons(@K,1),2)

  @out-below -> @out-repl
  @in-repl -> @in-below
  @X -> @in-repl  
  @out-repl -> fst(@X)
  @in-repl -> @out-repl

  @in-above -> @out-below , @in
  @in-below -> @out-above , @in
  @out -> @out-above , @out-below

Again, variants of the above will be accepted, provide they do
over-approximate the message flow.

*** Tree Automaton Completion Exercise

Consider the tree automaton A

   @a -> f(@b,@b)
   @b -> 1 , 2 , h(@b)

and the rewriting rule

   f(h(X),X) => g(X)

Applying the completion algorithm, construct a tree automaton
over-approximating the language of A up to rewriting.

(End of exercise)

Here you should notice that the rule is not left linear, so you
need an over approximation for intersection as well. E.g.

    @b intersects @b : yes  ( there's 1 )
    @a intersects @a : yes  ( f(1,1) )
    @a intersects @b : no
    @b intersects @a : no   ( symmetric )

Note that you have to keep this table updated when you add further
transitions to the automaton A.

Running the completion algorithm, the rule is triggered since
@b intersects @b, hence we add the following to the automaton:

   @a -> g(@b)

It is then easy to check that the intersection approximation is not
affected by this new transition. Also, the rewriting rule is not
triggered on any new cases. So, we reach a fixed point, and
the augmented automaton is the final result.

Of course, in the exam expect a few more iterations, due to the added
transition triggering the rewriting rule again.