SE547: Homework 5

Deadline: 5.30pm, Thursday 19 February 2004.


The file hw5.cry contains a Cryptyc specification of a broken protocol (note that this uses the standard prelude file prelude.cry).

The homework is to make as few changes as possible to the protocol, but get it to satisfy the secrecy, authenticity and freshness properties. Your protocol should be verified with the Cryptyc typechecker.

Submit your answer as a plain text file using Courses On Line.