您所在的位置:http://www.qk114.net > 论文 > 计算机论文 > 正文

NSSK协议的SPIN模型检测

   摘要:安全协议是以密码学为基础的消息交换协议。针对传统的改进NSSK安全协议,通过使用Promela语言对协议进行建模,并使用SPIN模型检测工具进行验证,发现仍然存在安全漏洞,攻击者可以冒充合法者进行通信。針对上述缺陷,提出了一种有效的改进方案,主要是在协议中增加了自身产生的随机数和发送者的身份标识,该改进方案提高了协议安全性。 

  关键词:安全协议; 安全漏洞;NSSK;SPIN;模型检测
DOIDOI:10.11907/rjdk.171239
中图分类号:TP309文献标识码:A文章编号:16727800(2017)010018504
0引言
如今,随着信息逐渐成为重要的战略资源,信息化水平已成为衡量一个国家现代化水平和综合国力的重要标志。同时,信息安全问题也成为人们重点关注的一个问题。安全协议是以密码学为基础的消息交换协议,其目的是在网络环境下提供各种安全服务。安全协议可以分为密钥交换协议、认证协议、电子商务协议、安全多方计算协议等多种类型。简单安全协议虽然只是简单消息的传递,但消息之间存在微妙、复杂的关系。NSSK协议[12]是一个经典的认证密码协议,不少学者在NSSK协议研究中提出了一些NSSK认证方案,但这些方案也不是完全安全的,仍然存在风险。2014年Hu等主要根据GSMR系统现有的安全威胁和必须采取的安全措施,采用一种改进的NSSK安全协议来保障车载设备与RBC之间的安全通信。通过分析发现,其存在着一些安全缺陷,因此提出了改进方案。
本文使用SPIN模型检测工具对NSSK协议的改进方案进行验证和分析,发现存在着攻击。因此,针对该攻击提出一种改进方案,以提高协议安全性。
1模型检测及工具SPIN
系统的设计和验证需要SPIN模型检测器的支持,首先形式化描述整个系统模型,对模型进行分析,发现语法错误,如果没有发现语法错误,则需要对系统进行交互模拟运行,直到系统设计达到预期为止。然后,SPIN会生成一个优化的onthefly验证程序,该程序将被编译后执行,如果在执行过程中发现了任何违背正确性的反例,则会返回交互模拟执行状态,继续进行检测诊断,以确定产生反例的原因。因此,它的建模方法是:定义进程模板,将每个进程模板的行为视为一种行为规范,实际系统可以被看作一个或多个异步进程模板实例的组合。SPIN是一种基于计算机科学的形式化方法,它将先进的理论验证方法应用于大型软件系统的验证中,目前在工业界和学术界得到了广泛应用。
SPIN的基本结构如图1所示,其描述了整个检测过程。
2协议介绍
2.1NSSK协议原理及存在的问题
NSSK协议是一个经典的认证密码协议。协议先通过对两个主体的身份进行认证,通信主体需要经过5个阶段的通信过程,才能获得安全通信过程的会话密钥。
协议符号说明:A表示用户A的身份标识;B表示用户B的身份标识;S表示服务器;Nb表示用户B产生的随机数;Na表示用户A产生的随机数;Kbs表示用户B与S之间的共享密钥;Kas表示用户A与S之间的共享密钥;Kab表示用户A和用户B的会话密钥。
协议的步骤如下:
(1)A→S:A,B,Na
(2)S→A:{Na,B,Kab,{Kab,A}Kbs}Kas
(3)A→B:{Kab,A}Kbs
(4)B→A:{Nb}Kab
(5)A→B:{Nb-1}Kab
在此协议中,用户A和用户B进行秘密通信,用户A会向服务器S请求分配一个会话密钥来保证通信内容的秘密性。协议前3个消息主要是服务器分配会话密钥给合法用户,后两个消息主要是合法用户之间的相互验证。
具体过程为:①协议开始时,合法用户A将用户A的身份标识、用户B的身份标识以及用户A产生的随机数Na组成消息1,发送给服务器S,告诉服务器它将与用户B进行通信;②服务器S在接收到消息1时,随机产生一个Kab,这是为双方分配的会话密钥,同时将A的身份标识和Kab用B的密钥Kbs加密生成一个证书,然后将证书、用户A在消息1发送的Na、用户B的身份标识和会话密钥Kab用A的密钥Kas加密组成消息2发送给A;③用户A接收到消息2时,用密钥Kas解密消息得到会话密钥Kab和证书{Kab,A}Kbs,然后再将证书组成消息3发送给用户B;④用户B接收到消息3时,用密钥Kbs解密得到会话密钥Kab,再用Kab加密自身产生的随机数Nb组成消息4,发送给用户A;⑤用户A接收到消息4后,用会话密钥Kab解密得到Nb,再将Nb与1进行运算后,将得到的结果用Kab进行加密组成消息5发送给用户B。这里的Nb-1可以用Nb来代替,只是用来区别消息4,而消息4和消息5是为了防止中间人攻击。
在此协议中,在消息4中用户A是通过Nb来确认用户B的身份,在消息5中用户B是通过Nb-1来确认用户A的身份。这里的Kab表示用户A和用户B之间的会话密钥,只有用户A和用户B可以对其解密。
该协议比较简单,实现起来也较为容易,但在文献[8]中,Denning和Sacco在1981年发现了一个攻击,发现此协议不能抵抗“新鲜性”攻击,如果一个攻击者拥有过期的会话密钥,能够冒充用户A,通过重放消息3,来实施以下攻击:
(1)A→S:A,B,Na
(2)S→A:{Na,B,Kab,{Kab,A}Kbs}Kas
(3)I(A)→B:{ K′ab,A}Kbs
(4)B→I(A):{N′b}K′ab
(5)I(A)→B:{N′b-1}K′ab
其中,I(X)表示攻击者可以冒充合法用户X接收和发送消息。通过上面的攻击过程,使合法用户B相信自己得到的会话密钥K′ab是执行当前协议回合的结果。因此,该攻击是有效的。
 在2001年,王贵林、卿斯汉等在文献[12]又提出攻击者可以冒充合法用户B实施以下攻击:
(1)A→S:A,B,Na
(2)S→A:{Na,B,Kab,{Kab,A}Kbs}Kas
(3)A→I(B):{Kab,A}Kbs
(4)I(B)→A:NI
(5)A→I(B):{{NI}K-1ab-1}Kab
其中,NI和{Nb}Kab格式相同,攻击者冒充用户B发送消息给用户A,用户A收到消息4,然后对其进行所谓的解密,并将得到的结果与1进行运算后,将运算后的结果用Kab加密发给用户B。用户A以为用户B知道了会话密钥,但实际上,B根本没有参加整个协议的执行过程,甚至可能还是离线的。因此,该攻击是有效的。
 
本站主营各类论文发表论文发表职称论文发表论文代写代发表服务!
加盟 加盟陈主编:QQ:22848269 咨询电话 垂询电话:13541216041 邮箱投诉邮箱:[email protected]
QQ客户 客服杨老师:QQ:61771950 咨询电话 垂询热线:02880885761 邮箱 咨询邮箱:[email protected]
QQ咨询 客服邓老师:QQ:61771951 咨询电话 垂询热线:02880885762 邮箱导咨询邮箱[email protected]
联系地址 联系地址: 四川大学望江校区 成都市一环路南一段24号 邮编: 610065
常年法律顾问支持:四川川达律师事务所 信息产业部备案:蜀ICP备08008442号
专业,诚信,快捷,权威的论文发表网