Proof-checking protocols using bisimulations

被引：0

作者：

Röckl, C ^{[1
]}

Esparza, J ^{[1
]}

机构：

[1] Tech Univ Munich, Fak Informat, D-80290 Munich, Germany

来源：

CONCUR'99: CONCURRENCY THEORY | 1999年 / 1664卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We report on our experience in using the Isabelle/HOL theorem prover to mechanize proofs of observation equivalence for systems with infinitely many states, and for parameterized systems. We follow the direct approach: An infinite relation containing the pair of systems to be shown equivalent is defined, and then proved to be a weak bisimulation. The weak bisimilarity proof is split into many cases, corresponding to the derivatives of the pairs in the relation. Isabelle/HOL automatically proves simple cases, and guarantees that no case is forgotten. The strengths and weaknesses of the approach are discussed.

引用

页码：525 / 540

页数：16

共 50 条

[41] Proof checking and logic programming
Miller, Dale
PROCEEDINGS OF THE 17TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2015), 2015, : 18 - 18
[42] Proof Checking and Logic Programming
Miller, Dale
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2015), 2015, 9527 : 3 - 17
[43] Checking Interface Interaction Protocols Using Aspect-oriented Programming
Anh-Hoang Truong
Thanh-Binh Trinh
Dang Van Hung
Viet-Ha Nguyen
Nguyen Thi Thu Trang
Pham Dinh Hung
SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2008, : 382 - +
[44] Synthesis of attack actions using model checking for the verification of security protocols
Basagiannis, Stylianos
Katsaros, Panagiotis
Pombortsis, Andrew
SECURITY AND COMMUNICATION NETWORKS, 2011, 4 (02) : 147 - 161
[45] Using automatable proof obligations for component-based design checking
Rangarajan, M
Alexander, P
Abu-Ghazaleh, NB
ECBS '99, IEEE CONFERENCE AND WORKSHOP ON ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 1999, : 304 - 310
[46] Specification, proof, and model checking of the Mondex electronic purse using RAISE
George, Chris
Haxthausen, Anne E.
FORMAL ASPECTS OF COMPUTING, 2008, 20 (01) : 101 - 116
[47] Fast, automatic checking of security protocols
Kindred, D
Wing, JM
PROCEEDINGS OF THE SECOND USENIX WORKSHOP ON ELECTRONIC COMMERCE, 1996, : 41 - 52
[48] Model Checking Distributed Protocols in Must
Enea, Constantin
Giannakopoulou, Dimitra
Kokologiannakis, Michalis
Majumdar, Rupak
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (OOPSLA2):
[49] Nested Proof Compilation and Proof Checking in Universal Pattern Logic
Pan, Wuming
Guo, Bing
ROUGH SETS AND KNOWLEDGE TECHNOLOGY, PROCEEDINGS, 2009, 5589 : 358 - 366
[50] Complexity of Checking Freshness of Cryptographic Protocols
Liang, Zhiyao
Verma, Rakesh M.
INFORMATION SYSTEMS SECURITY, PROCEEDINGS, 2008, 5352 : 86 - 101

← 1 2 3 4 5 →