-
题名NSPK协议的Spin模型检测
被引量：3
- 1
-
-
作者
陈道喜
张广泉
陈冬火
-
机构
苏州大学计算机科学与技术学院
-
出处
《微电子学与计算机》
CSCD
北大核心
2008年第10期58-60,64,共4页
-
基金
江苏省高校自然科学研究项目(05KJB520119
08KJB520010)
重庆市自然科学基金项目(2006BB2259)
-
文摘
NSPK协议是一个经典的认证密码协议.通过建立该协议的Promela模型,采用线性时序逻辑描述模型性质,并用模型检测工具Spin进行验证,进而生成入侵者的攻击序列.
-
关键词
模型检测
nspk协议
SPIN
-
Keywords
model checking
nspk protocol
Spin
-
分类号
TS311
[轻工技术与工程]
-
-
题名NSPK协议的Promela语言建模及分析
- 2
-
-
作者
田国良
陈春玲
-
机构
南京邮电大学计算机学院
-
出处
《电力系统通信》
2008年第8期52-55,59,共5页
-
文摘
重点提出了对NSPK协议进行建模设计的思想和方法,阐述了如何用Promela语言实现模型的关键技术。使用Spin对该模型进行行为模拟和属性校验,结果既能保证协议的正常执行,也能帮助发现安全缺陷。
-
关键词
SPIN
PROMELA
nspk
建模
-
Keywords
SPIN
promela
nspk
modeling
-
分类号
TN915.04
[电子电信—通信与信息系统]
-
-
题名基于可信平台模块的NSPK协议
- 3
-
-
作者
孙春燕
池亚平
方勇
-
机构
北京电子科技学院
西安电子科技大学通信工程学院陕西
北京工业大学计算机学院
北京电子科技学院北京
-
出处
《网络安全技术与应用》
2007年第7期31-32,共2页
-
文摘
本文针对Needham-Schroeder公钥认证协议存在的问题,利用TPM的相关功能对协议进行了改进,提出了基于TPM的NSPK认证协议。解决了攻击者仿冒实体A与实体B共享秘密数据的安全缺陷,使其安全性有了显著提高。
-
关键词
nspk协议
Lowe攻击
TPM
平台证实
-
Keywords
nspk protocol
Lowe-attack
TPM
attestation
-
分类号
TP393.04
[自动化与计算机技术—计算机应用技术]
-
-
题名Dolev-Yao攻击者模型的形式化描述
被引量：9
- 4
-
-
作者
唐郑熠
李祥
-
机构
贵州大学计算机软件与理论研究所
-
出处
《计算机工程与科学》
CSCD
北大核心
2010年第8期36-38,45,共4页
-
文摘
模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev-Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。
-
关键词
Dolev-Yao攻击者模型
形式化描述
模型检测
SPIN
nspk
A(0)
-
Keywords
Dolev-Yao intruder model
formalization description
model checking
SPIN
nspk
A（0）
-
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
-
-
题名SAL框架下的安全协议分析技术研究
- 5
-
-
作者
李超
董荣胜
郭云川
-
机构
桂林电子科技大学计算机系
中国科学院计算技术研究所
-
出处
《计算机科学》
CSCD
北大核心
2006年第B12期40-43,共4页
-
基金
广西自然科学基金项目（编号：0542052）资助.
-
文摘
SAL是一种新的结合模型检验和定理证明技术的分析框架。它使用一种过渡性的中间语言将不同验证工具统一在其框架之中，以便保证安全协议的验证不会顾此失彼。本文对基于SAL框架下的安全协议分析技术进行了研究，介绍了SAL中间语言描述安全协议的方法，包括消息项中协议主体、入侵者、现时值、公私密钥、对称密钥、加密、解密、DH问题等的描述，协议规则与性质的描述，给出了在SAL下刻画入侵者模型和建立通信模型的一般方法，并以经典的NSPK协议为例，找到了一个已知的认证性攻击。
-
关键词
SAL(Symbolic
ANALYSIS
Laboratory)
模型检验
定理证明
安全协议
nspk协议
-
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
-
