TU Wien:Formal Methods for Security and Privacy VU (Maffei)/Exam 2020-07

Exam consisted of four parts:

1. Typing for Cryptographic Protocols (30 points, 3 exercises):
   1. Does a given process hold secrecy/integrity, give a type derivation if yes or a counter-example if not
   2. Find an appropriate type instantiation for a given process
   3. Show the incompleteness of the given type system by example of a process that preserves secrecy and integrity but does not type check
2. Protocol Analysis (20 points, 2 exercises):
   1. Does a given protocol satisfy (non-)injective agreement, if not describe an attack and propose a minimal modification to fix it
   2. Give an intuitive explanation why two protocols do or do not hold injective agreement or show an attack)
3. Information Flow (20 points, 2 exercises):
   1. Prove incompleteness of the given type system for non-interference by counterexample
   2. Give a type derivation for a given program or show why it fails)
4. Static Analysis (30 points, 2 exercises):
   1. Show all intermediate and final configurations of a short program given small-step semantics
   2. For three different abstractions argue whether the given soundness claim holds and give example programs)