A BSP algorithm for on-the-fly checking CTL* formulas on security protocols |
| |
Authors: | Frédéric Gava Franck Pommereau Michaël Guedj |
| |
Affiliation: | 1. LACL, University of Paris-East, Créteil, France 2. IBISC, University of évry, évry, France
|
| |
Abstract: | This paper presents a distributed (Bulk-Synchronous Parallel or bsp) algorithm to compute on-the-fly whether a structured model of a security protocol satisfies a ctl \(^*\) formula. Using the structured nature of the security protocols allows us to design a simple method to distribute the state space under consideration in a need-driven fashion. Based on this distribution of the states, the algorithm for logical checking of a ltl formula can be simplified and optimised allowing, with few tricky modifications, the design of an efficient algorithm for ctl \(^*\) checking. Some prototype implementations have been developed, allowing to run benchmarks to investigate the parallel behaviour of our algorithms. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|