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

被引：5

作者：

Gava, Frederic ^{[1
]}

Pommereau, Franck ^{[2
]}

Guedj, Michael ^{[1
]}

机构：

[1] Univ Paris East, LACL, Creteil, France

[2] Univ Evry, IBISC, Evry, France

来源：

JOURNAL OF SUPERCOMPUTING | 2014年 / 69卷 / 02期

关键词：

BSP; LTL; CTL*; Security protocols; State-space; Model-checking; MODEL CHECKING; STATE; TOOL;

D O I：

10.1007/s11227-014-1099-8

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：629 / 672

页数：44

共 50 条

[1] A BSP algorithm for on-the-fly checking CTL* formulas on security protocols
Frédéric Gava
Franck Pommereau
Michaël Guedj
[J]. The Journal of Supercomputing, 2014, 69 : 629 - 672
[2] A BSP algorithm for on-the-fly checking CTL* formulas on security protocols
Gava, Frederic
Guedj, Michael
Pommereau, Franck
[J]. 2012 13TH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS, AND TECHNOLOGIES (PDCAT 2012), 2012, : 79 - 84
[3] On-the-fly model checking of RCTL formulas
Beer, I
Ben-David, S
Landver, A
[J]. COMPUTER AIDED VERIFICATION, 1998, 1427 : 184 - 194
[4] ON-THE-FLY AUTOMATIC GENERATION OF SECURITY PROTOCOLS
Kiyomoto, Shinsaku
Ota, Haruki
Tanaka, Toshiaki
[J]. ICEIS 2008: PROCEEDINGS OF THE TENTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS, VOL ISAS-2: INFORMATION SYSTEMS ANALYSIS AND SPECIFICATION, VOL 2, 2008, : 97 - 104
[5] On-the-fly model checking of fair non-repudiation Protocols
Li, Guoqiang
Ogawa, Mizuhito
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 511 - +
[6] Heuristic on-the-fly model checking algorithm for extended TGBA
[J]. Wang, Xi, 1600, Science Press (37):
[7] Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation
Bulychev, Peter
Chatain, Thomas
David, Alexandre
Larsen, Kim G.
[J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2009, 5813 : 73 - 87
[8] On-the-fly Probabilistic Model Checking
Latella, Diego
Loreti, Michele
Massink, Mieke
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (166): : 45 - 59
[9] Distributed On-the-Fly Equivalence Checking
Joubert, Christophe
Mateescu, Radu
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 128 (03) : 47 - 62
[10] On-the-Fly Model Checking with Neural MCTS
Xu, Ruiyang
Lieberherr, Karl
[J]. NASA FORMAL METHODS (NFM 2022), 2022, 13260 : 557 - 575

← 1 2 3 4 5 →