12 November 2002, Zuidelijk Interuniversitair Colloquium (ZIC), Jesse Hughes

We look at a new way of specifying and verifying cryptographic protocols using the Coalgebraic Class Specification Language (CCSL). Our approach starts by providing a CCSL specification which models a cryptographic protocol (and inherits from a more abstract class specification). We include with the specification the correctness conditions to be proved (representing, typically, secrecy and authentication). This specification is compiled into a number of PVS theories. The correctness theorems are then proven within PVS, using a temporal logic derived from the coalgebraic specification of the protocol. We will conclude with a comparison with other approaches for analyzing cryptographic protocols. The main distinguishing feature of our approach is that it takes coalgebraic theory as its foundation.

For more information, see http://www.win.tue.nl/zic/ or contact Francien Dechesne (f.dechesne at uvt.nl).