A BSP algorithm for on-the-fly checking CTL* formulas on security protocols

Frédéric Gava (1) , Michael Guedj (1) , Franck Pommereau (2)

1 LACL - Laboratoire d'Algorithmique Complexité et Logique
2 IBISC - Informatique, Biologie Intégrative et Systèmes Complexes

This paper presents a distributed algorithm to compute on-the-fly whether a structured model of a security protocol satisfies or not a CTL* formula. The design of this simple and still efficient algorithm is possible by using the structured nature of security protocols. A prototype implementation has been developed, allowing to run benchmarks.

Keywords: BSP; CTL; Security Protocols

Domains: Modeling and Simulation; Networking and Internet Architecture [cs.NI]

Frédéric Gava, Michael Guedj, Franck Pommereau. A BSP algorithm for on-the-fly checking CTL* formulas on security protocols. 13th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT 2012), Dec 2012, Beijing, China. pp.79--84, ⟨10.1109/PDCAT.2012.12⟩. ⟨hal-00950415⟩