DocumentCode
1984043
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
fYear
2012
fDate
25-29 June 2012
Firstpage
11
Lastpage
18
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Parallel and Distributed Computing (ISPDC), 2012 11th International Symposium on
Conference_Location
Munich/Garching, Bavaria
Print_ISBN
978-1-4673-2599-8
Type
conf
DOI
10.1109/ISPDC.2012.10
Filename
6341488
Link To Document