面向命题投影时序逻辑的安全协议模型检测

杨琛 1; 2; 段振华 1; 王小兵 1; 2

您当前的位置：

首页 >

文章列表页 >

面向命题投影时序逻辑的安全协议模型检测

更新时间：2025-07-09

- 面向命题投影时序逻辑的安全协议模型检测
- Model-Checking Security Protocol with Propositional Projection Temporal Logic
- 西安交通大学学报 2010年44卷第8期页码：30-35
- 作者机构：
  
  1. 西安电子科技大学计算理论与技术研究所,西安,710071
  2. 武汉大学软件工程国家重点实验室,武汉,430072
- 作者简介：
- 基金信息：
  
  : 2010-02-01. 作者简介: 杨琛(1981-),男,博士生;段振华(联系人),男,教授,博士生导师. 基金项目: 国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)
- DOI：
  中图分类号： TP301
- 网络首发：2010-08-10，
  
  纸质出版：2010
- 稿件说明：
移动端阅览
杨琛 1, 2, 段振华 1, 等. 面向命题投影时序逻辑的安全协议模型检测[J]. 西安交通大学学报, 2010,44(8):30-35.

Model-Checking Security Protocol with Propositional Projection Temporal Logic[J]. 2010, 44(8): 30-35.
杨琛 1, 2, 段振华 1, 等. 面向命题投影时序逻辑的安全协议模型检测[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.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

PPTL模型检测器实现的一个关键技术

非否认协议公平性分析的扩展串空间方法

应用UML2.0模型的测试用例生成方法

面向投影时序逻辑的Web服务模型检测

车载FlexRay总线安全协议的设计与实现