Themes in True-Concurrency and the Verification of Cryptographic Protocols

Speaker: Sibylle Froeschle

13th February 2006 , 2pm , G21/22 Devonshire Building

Abstract

The talk will proceed in two parts. In the first part I will present highlights of my work on the computational power of true-concurrency.In the second part I will discuss ongoing work on the verification of cryptographic protocols. True-concurrency is often perceived as both difficult to tackle and computationally hard. This is exemplified by hereditary history preserving bisimilarity (hhp-b): whether this notion is decidable was a renowned open problem for many years until it was finally proved undecidable by Jurdzi{'n}ski and Nielsen; only a few positive results could be achieved for restricted classes (Fr{"o}schle 2005). The negative findings are contrasted by a positive trend for true-concurrency in the infinite-state world. In particular, Lasota and I have recently resolved that hhp-b is polynomial-time decidable for the class Basic Parallel Processes. The hope to be able to validate cryptographic protocols automatically seems to have been thwarted by the fact that most security properties such as secrecy have turned out to be undecidable. On the other hand, one could argue that the undecidability proofs exhibited so far do leave room for positive results: most of these proofs exploit properties of the formal models used to represent protocols rather than characteristics possessed by realistic protocols. Based on this insight, one goal of my research is to characterize natural classes of protocols with decidable security properties.