8th International Workshop on Security Issues in Concurrency

09:20 - 09:30	Welcome

09:30 - 10:30	Invited talk: Sjouke Mauw. "Oh grandma, what big teeth you have!" Understanding authentication in security protocols

10:30 - 11:00	Coffee break

11:00 - 11:30	Bernardo Toninho and Luis Caires. A Spatial-Epistemic Logic for Reasoning about Security Protocols.
11:30 - 12:00	Stephanie Delaune, Steve Kremer, Mark Ryan and Graham Steel. A Formal Analysis of Authentication in the TPM (short paper)

12:00 - 14:30	Lunch

14:30 - 15:30	Invited talk: Jean Goubault-Larrecq. "Logic Wins!"

15:30 - 16:00	Coffee break

16:00 - 16:30	Eike Best, Philippe Darondeau and Roberto Gorrieri. On the Decidability of Non Interference over Unbounded Petri Nets.
16:30 - 17:00	Loic Helouet and Aline Roumy. Covert channel detection using Information Theory.

17:00 - 17:10	Closing

Sjouke Mauw, University of Luxembourg

Title: "Oh grandma, what big teeth you have!"
Understanding authentication in security protocols

Over the past few decades, research in security protocols led to the development of a number of authentication notions, ranging from weak properties, such as aliveness, to stronger properties, like full injective agreement. Currently, authentication is considered as one of the best understood security requirements in security protocol research.

In this talk I will give an overview of the various forms of authentication and I will discuss their relation and application. I will briefly present ongoing research on a new and intuitive characterization of the strongest authentication notion, injective synchronisation.
Jean Goubault-Larrecq, ENS Cachan

Title: "Logic Wins!"

Clever algorithm design is sometimes superseded by simple encodings into logic. In particular, we claim that it is particularly simple to encode sound abstractions of security protocols in H1, a decidable fragment of first-order Horn clauses. After reviewing a variant of Nielson, Nielson and Seidl's work on H1 and the spi-calculus, we describe a verification algorithm designed with the same spirit, and which applies to hardware circuit descriptions written in VHDL. We shall describe the new challenges posed by VHDL, in particular the particular semantics of 'wait' instructions, and the effect of signal updates and of timeouts.