Exercises will be elaborated as we move along. Starred exercises are harder than unstarred ones. Do try them.

Lecture 1:

• 4.10, 4.12, 4.14, 4.16, 5.11, 5.12
• If you haven't done CCS already you must try some of the examples in ch 1-7 in full detail plus the associated exercises.
• Do some representative cases (not covered in Milner or in class) of the proof of prop 5.2
• Define carefully alpha-conversion and name substitution for concurrent processes.
• A name substitution is any function f: Name -> Name extended to actions such that f(tau) = tau and f(overbar(a)) = overbar(f(a)). Is strong bisimulation equivalence preserved under name substitution. What if f is injective? (*)
• Prove prop. 4.6

Lecture 2:

• 9.8, 9.10, 9.14 (*), 9.15 (**), 9.18

Lecture 3:

• 9.22, 9.25, 9.26, all exercises in ch. 10.

Lecture 4:

• 11.4, 11.13, 11.15, 11.21
• Object variables in section 11.4 are local (in a pi-calculus sense). That is, a variable A.V is not made directly available to the environment, but it can be exported, i.e. a method can pass the location of A.V as a return value. Modify the encoding so that A.V is public, i.e. directly available at the object interface. Can you produce an encoding where A.V is private in the sense that it is not exportable?

Lecture 5:

• 12.7, 12.20, 12.27, 12.30, 13.9
• Prove prop. 12.12.1

Lecture 6:

• A modal formula F is valid if P |= F for all processes P. Show that the following proof rules for modal validity are valid
  • If |- F then |- [L]F for any L
  • |- [L](F -> G) -> ([L]F -> [L]G)
• Determine whether the following formulas are valid:
  • [-](F /\ G) -> [-]F /\ [-]G
  • [-](F \/ G) -> [-]F \/ [-]G
  • [-]F -> F
• Show that concurrent processes (as in the pi-calculus book) are image finite

Lecture 7:

• Prove, using fixed point induction:
  1. mf £ f(mf)
  2. mf £ nf
  3. mf = f(f(mf))
• Assume mf = m(g o f) where o is function composition. Assume that g o f = f o g. Show, using fixed point induction, that mf = mg.
• Reprove 1.-3. above using transfinite induction.

Lecture 8:

• Express the following properties in the modal mu-calculus:
  • An a action can never happen without a b action happening first
  • Infinitely often an a and a b action are simultaneously enabled
• Prove that the modal mu-calculus is monotone in the sense that if A Í B then || f ||r[A/X] Í || f ||r[B/X]
• Define P = a.P and Q = (a'.a'.Q) + b.0. Show that the term new a (P | Q) satisfies the mu-calculus property nu X.mu Y.[tau](((<b>X) \/ Y) /\ <tau>true).
• A function f: A -> A on a complete lattice A is continuous if f(\/{a_i | i in I}) = \/{f(a_i) | i in I} for all chains {ai | i in I}. Is the modal mu-calculus continuous in this sense? (*)

Each project is based on some research paper. Probably you will find that several papers will be needed. Different sorts of projects are possible, depending on interest and paper. The preferred option will be to apply some tool or technique introduced in the paper on some protocol of interest; evaluate, identify problems and possible extensions, if relevant, or, possibly, try a different tool on the same example. Some examples of protocols or problems are given below. Alternatively, if the main contribution of the paper is an algorithm or proof system or similar, an objective could be to implement a prototype tool, or modify an existing one. If you are more theoretically inclined, an objective might be to reproduce proofs in detail. Regardless, you'll need to agree your choice of project with the lecturer.

• Contract signing/payment protocols in applied pi and ProVerif
  • Consider one or two of the contract signing/payment protocols below, model in applied pi and analyze using ProVerif
• Contract signing protocols in Isabelle
  • Same, but this time use Paulson's theorem proving framework in Isabelle
• Comparison of the ProVerif and Avispa toolsets
  •  Analyze the same non-trivial protocol in ProVerif and Avispa. Compare the approaches concerning scope, performance, etc
• Mu-calculus theorem prover
  • Implement the proof system of Sprenger and Dam below as an interactive theorem prover and do some simple experiments.
• Security protocol analysis in mobility workbench
  • Model one or two simple protocols such as NSPK and Yahalom in pi-calculus, analyze using mobility workbench. Take inspiration from finite state analyses such as those of Mitchell et al below.

References:

• Mitchell J.C., Mitchell M., and Stern U. Automated analysis of cryptographic protocols using Murphi 
• L C Paulson. The inductive approach to verifying cryptographic protocols
• C. Sprenger and M. Dam: A note on global induction mechanisms in a µ-calculus with explicit approximations

Tools:

• Mobility Workbench
• ProVerif
• Isabelle
• AVISPA

Protocols:

• N. Asokan, Matthias Schunter, Michael Waidner: Optimistic Protocols for Fair Exchange
• Juan Garay, Markus Jakobsson, Philip MacKenzie: Abuse-free Optimistic Contract Signing
• Michael Ben-Or, Oded Goldreich, Silvio Micali, Ronald Rivest: A Fair Protocol for Signing Contracts

Midterm exam

060418: Exam, ringBuffer.ps, ringBuffer.gif

Workshop

Contact

Mads Dam, CSC, E-mail: mfd at kth dot se