-
题名基于Spin的安全协议形式化验证技术
被引量：4
- 1
-
-
作者
冉俊轶
吴尽昭
-
机构
中国科学院成都计算机应用研究所
中国科学院大学
广西混杂计算与集成电路设计分析重点实验室(广西民族大学)
北京交通大学计算机与信息技术学院
-
出处
《计算机应用》
CSCD
北大核心
2014年第A02期85-90,共6页
-
基金
国家自然科学基金资助项目(11371003)
广西自然科学基金资助项目(2011GXNSFA018154
+2 种基金
2012GXNSFGA060003)
广西区主席科技资金资助项目(10169-1)
广西教育厅科研资助项目(201012MS274)
-
文摘
针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法:模型检测过程中的存储状态数减少,使模型复杂度降低约40%;迁移状态数减少,使验证效率提升约44%。
-
关键词
安全协议
形式化验证
Spin模型检测
Promela语义模型
ltl公式
密钥分配中心协议
-
Keywords
security protocol
formal verification
Spin model checking
Promela semantic model
Linear Timing Logic（ltl） formula
key contribution center protocol
-
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
-
-
题名LTL公式到自动机的转换
被引量：4
- 2
-
-
作者
郭建
边明明
韩俊岗
-
机构
西安电子科技大学微电子学院
西安邮电学院计算机系
-
出处
《计算机科学》
CSCD
北大核心
2008年第7期241-243,276,共4页
-
基金
国家自然科学基金(NO.90607008)资助
陕西省教育厅项目(07JK373)资助
-
文摘
在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法。该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机。此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换。
-
关键词
模型检验
Buchi自动机
选择Buchi自动机
ltl公式
-
Keywords
Model checking,Buchi automata, Alternating buchi automata, Linear temporal logic
-
分类号
TP301.1
[自动化与计算机技术—计算机系统结构]
TP311.13
[自动化与计算机技术—计算机科学与技术]
-
-
题名LTL性质的可监视性
- 3
-
-
作者
王伟芳
樊丽丽
李宝凤
赵光峰
-
机构
唐山师范学院数学与计算科学学院
-
出处
《唐山师范学院学报》
2021年第3期18-20,共3页
-
基金
唐山师范学院科研基金项目(2016C12)。
-
文摘
以LTL的语义和可监视的定义为依据,证明了LTL性质的可监视性,得到了φ1∪φ2可监视的几个充分条件,还证明了可监视性在∨,■,○下是封闭的,在∪下不是封闭的。
-
关键词
可监视
ltl公式
模型检验
拓扑
-
Keywords
monitorable
ltl formula
model checking
topology
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名RGPS服务层元模型正确性验证
- 4
-
-
作者
张莉
杨淑贞
杨浩
-
机构
浙江长征职业技术学院计算机与信息技术系
浙江传媒学院新媒体学院
-
出处
《软件导刊》
2016年第12期8-10,共3页
-
基金
浙江省教育厅一般科研项目(2016)
浙江省教育中心2014年研究课题(JA049)
-
文摘
随着网络式软件复杂程度的日益增加,如何确保网络式软件功能和性能的正确性越发重要。根据网络式软件的特点,在RGPS需求元建模框架的指导下,提出RGPS服务层元模型正确性验证。首先用BPEL语言和WSDL语言把RGPS服务层元模型描述成BPEL模型,再用Promela语言实现BPEL模型的建模,最后输入LTL公式对RGPS服务层元模型进行安全性和活性验证分析。以城市交通出行系统为例,采用RGPS需求元模型为框架,构建城市交通出行系统服务层元模型。
-
关键词
网络式软件
BPEL
PROMELA
ltl公式
正确性验证
-
分类号
TP306
[自动化与计算机技术—计算机系统结构]
-
