Universiteit van Amsterdam

Events

Institute for Logic, Language and Computation

Please note that this newsitem has been archived, and may contain outdated information or links.

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

Speaker: Jesse Hughes (KUN)
Title: The Coinductive Approach to Verifying Cryptographic Protocols
Date: Tuesday 12 November 2002
Time: 14:15 - 16:00 uur
Location: TU Eindhoven, HG 6.96

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 ().

Please note that this newsitem has been archived, and may contain outdated information or links.