Model-Checking Security Protocol with Propositional Projection Temporal Logic

您当前的位置：

首页 >

文章列表页 >

Model-Checking Security Protocol with Propositional Projection Temporal Logic

更新时间：2025-07-09

- Model-Checking Security Protocol with Propositional Projection Temporal Logic
- Vol. 44, Issue 8, Pages: 30-35(2010)
- 作者机构：
  
  1. 西安电子科技大学计算理论与技术研究所,西安,710071
  2. 武汉大学软件工程国家重点实验室,武汉,430072
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP301
- Online First：10 August 2010，
  
  Published：2010
- 稿件说明：
移动端阅览
Model-Checking Security Protocol with Propositional Projection Temporal Logic[J]. 2010, 44(8): 30-35.
DOI：

Model-Checking Security Protocol with Propositional Projection Temporal Logic[J]. 2010, 44(8): 30-35. DOI：

摘要

针对无条件安全通信协议

特别是Russian Cards协议的安全性验证问题

提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型; 利用chop算子将多个交互事件进行顺序复合

以表达协议所期望的通信序列; 由projection算子定义了协议在该序列上的安全性质

再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入

以完成验证工作.验证结果表明

由协议规则构造的Russian Cards通信协议是安全可靠的

该方法也适用于一般的无条件安全通信协议的验证.

Abstract

A method of model-checking is proposed based on propositional projection temporal logic(PPTL)to verify the security of unconditional security communication protocols

in particular the Russian Cards protocols. The protocol model is built up in ProMeLa language according to the rules of constructing Russian Cards protocol that are given in our previous work. The security properties are defined by PPTL

that is

the chop operator is used to compose interactive events sequentially and to formalize the expected communication sequence

and the projection operator is employed to express the security properties over the sequence. Then the PPTL properties are transformed into Never Claim structures. The verification is done in a widely-used model checker-SPIN with the ProMeLa model and the Never Claim properties as the inputs. Experimental results show that Russian Cards protocols constructed using the protocol rules are safe and reliable. The model-checking method is also applicable in verifying ordinary unconditional security communication protocols.

关键词

Keywords

references

DUAN Zhenhua, YANG Chen. Unconditional secure communication: a Russian Cards protocol [J]. Journal of Combinatorial Optimization, 2010, 19(4): 501-530.

CLARKE E M, EMERSON E A, SISTLA A P. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems, 1986, 8(2): 244-263.

HOLZMANN G J. The spin model checker: primer and reference manual [M]. Reading, Mass, USA: Addison-Wesley, 2003.

VAN DITMARSCH H P, VAN DER HOEK W, VANDER MEYDEN R, et al. Model checking Russian Cards [J]. Electronic Notes in Theoretical Computer Science, 2006,149(2):105-123.

DUAN Zhenhua. Temporal logic and temporal logic programming [M]. Beijing, China: Science Press of China, 2006.

王小兵, 段振华. 面向投影时序逻辑的Web 服务模型检测 [J]. 西安交通大学学报, 2009,43(4): 39-44.

WANG Xiaobing, DUAN Zhenhua. Projection temporal logic oriented model checking for web services [J]. Journal of Xi'an Jiaotong University, 2009, 43(4): 39-44.

DUAN Zhenhua, TIAN Cong, ZHANG Li. A decision procedure for propositional projection temporal logic with infinite models [J]. Acta Informatica, 2008,45(1): 43-78.

TIAN Cong, DUAN Zhenhua. Propositional projection temporal logic, Büchi Automata and Omega-Regular Expressions[C]∥Proceedings of TAMC'08. Berlin, Germany: Springer, 2008, 4897: 47-58.

Model of Russian Cards protocol [EB/OL].[2010-01-01]. http:∥www.keepandshare.com/doc/view.php?id=1637338da=y.

利用投影时序逻辑的多内核进程调度建模与验证. 西安交通大学学报,2010, 44(10):52-57.

信息不确定条件下时间序列的关联分析法.西安交通大学学报,2010, 44(6):67-71.

一种新的动态批密钥更新算法. 西安交通大学学报,2009, 43(12):65-69.

基于隐马尔可夫模型的无线局域网媒体接入控制层入侵检测方法. 西安交通大学学报,2009, 43(12):26-30.

提取有效规则的关联分类算法. 西安交通大学学报,2009, 43(4):22-25.

用伪二叉树法则构造多目标Pareto最优解集的方法. 西安交通大学学报,2009, 43(2):29-32.

具有局部验证者撤销的短群签名方案. 西安交通大学学报,2008, 42(10):1250-1253.

多核并行测试系统研究. 西安交通大学学报,2008, 42(6):683-687.

一种基于最小覆盖的复杂Web 服务组合方法. 西安交通大学学报,2008, 42(8):945-949.

面向移动协同的扩展式动态环境演算范型研究. 西安交通大学学报,2008, 42(4):427-430.

一类随机性EOQ模型的关键路径存贮策略. 西安交通大学学报,2008, 42(4):431-435.

基于随机密钥预分布模型的安全定向扩散协议. 西安交通大学学报,2007, 41(12):1423-1426.

基于扩展投影时序逻辑的组合Web服务描述与验证. 西安交通大学学报,2007, 41(10):1155-1159.

新的有效叛逆者追踪方案. 西安交通大学学报,2007, 41(8):931-933.

非否认协议公平性分析的扩展串空间方法. 西安交通大学学报,2007, 41(6):6-20.

基于SWIM卡公钥认证的二阶段握手加密套接层协议. 西安交通大学学报,2007, 41(6):669-673.

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic

An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols

Test Case Generation Based on UML2.0 Models

Projection Temporal Logic Oriented Model Checking for Web Services

Design and Implementation of Security Protocol for In-Vehicle FlexRay Buses

Related Author

段振华 1

杨琛 1

王育民 1

陈静 2

李磊 1

Related Institution

实验室

武汉大学软件工程国家重点实验室

National Key Laboratory of Integrated Service Networks, Xidian University

State Key Laboratory of Integrated Service Networks, Xidian University

College of Computer Science and Technology, Jilin University

⁰