October 11, 2012

Michael Guedj (LACL) 14h, salle des thèses

It has long been a challenge to determine conclusively whether a given protocol is secure or not. The development of formal techniques that can check various security properties is an important tool to meet this challenge. This document contributes to the development of such techniques by model security protocols using an algebra of coloured Petri net call ABCD and reduce time to checked the protocols using parallel computations. We exploit the well-structured nature of security protocols and match it to a model of parallel computation called BSP. The structure of the protocols is exploited to partition the state space and reduce cross transitions while increasing computation locality. At the same time, the BSP model allows to simplify the detection of the algorithm termination and to load balance the computations. We consider the problem of checking a LTL and CTL* formulas over labelled transition systems (LTS) that model security protocols. A prototype implementation has been developed, allowing to run benchmarks.