Title :
A BSP Algorithm for On-the-fly Checking LTL Formulas on Security Protocols
Author :
Gava, Frédéric ; Guedj, Michaël ; Pommereau, Franck
Author_Institution :
LACL, Univ. of Paris-East, Creteil, France
Abstract :
This paper presents a Bulk-Synchronous Parallel (BSP) algorithm to compute on-the-fly whether a structured model of a security protocol satisfies a LTL formula. Using the structured nature of the security protocols allows us to design a simple and efficient parallelisation of an algorithm which constructs the state-space under consideration in a need-driven fashion. A prototype implementation has been developed, allowing to run benchmarks.
Keywords :
cryptographic protocols; parallel algorithms; BSP algorithm; LTL formula; bulk-synchronous parallel algorithm; labelled transition systems; on-the-fly checking LTL formulas; security protocol; security protocols; Algorithm design and analysis; Computational modeling; Educational institutions; Partitioning algorithms; Protocols; Prototypes; Security; BSP; LTL; Security Protocols;
Conference_Titel :
Parallel and Distributed Computing (ISPDC), 2012 11th International Symposium on
Conference_Location :
Munich/Garching, Bavaria
Print_ISBN :
978-1-4673-2599-8
DOI :
10.1109/ISPDC.2012.10
