《身份认证协议的模型检测分析》由会员分享，可在线阅读，更多相关《身份认证协议的模型检测分析（7页珍藏版）》请在金锄头文库上搜索。
1、第26卷第2期2003年2月计算机学报CHINESE JOURNAL OF COMPUTERSVol.26 No.2Feb.2003身份认证协议的模型检测分析徐蔚文陆鑫达(上海交通大学计算机科学与工程系上海200030)收稿日期:2002-03-07;修改稿收到日期:2002-09-24.本课题得到国家自然科学基金(60173103)资助.徐蔚文,女,1975 年生,博士研究生,主要研究协议的形式化验证方法.E-mail:xu-ww .陆鑫达,男,1938 年生,教授,博士生导师,主要研究方向为高性能计算、网络计算.摘要提出一个直观、易用的模型来模拟和验证身份认证协议,并给出基于Spin(模型
2、检测工具)的实现,它不仅可以模拟多对参与者同时进行会话,而且还有效缩减了状态空间,从而避免了以前文献中提到的状态爆炸现象.同时该文用Needham-Schroeder 公钥协议和TMN 协议来说明如何应用该模型.关键词身份认证协议;模型检测;Spin中图法分类号:TP309Model Checking of Authentication ProtocolsXU Wei-WenLU Xin-Da(Departmentof Computer ScienceandEngineering, ShanghaiJiaotong University , Shanghai 200030)AbstractTh
3、e increasing popularity of distributed systems and the emergence of new technologies,such as electronic commerce, demand new security solutions.The corresponding cornerstone of securi-ty is often authentication, therefore easy to use methods and tools for modeling and verification of au-thentication
4、 are needed.This paper develops a way of verifying authentication protocols using modelchecking.Model checking has been proven to be a very useful technique for verifying hardware de-signs.By modeling circuits as finite-state machines, and exploring all possible execution traces, modelchecking can f
5、ind a number of errors in real world designs.Like hardware designs, authentication pro-tocols are very subtle, and can also have bugs which are difficult to find.Specially , this paper presentsa simpler model for modeling and verifing authentication protocols, which not only adapts to the situa-tion
6、 with multi-pairs of participants but also efficiently reduces the sizes of the state space and avoidsstates explosion problem mentioned in previousliteratures.Also this paper implements the modelusingModel Checker Spin .Needham-Schroeder Public Key protocol and TMN protocol examples are illus-trate
7、d to show how this framework is applied.Keywordsauthentication;model checking ;Spin1引言近年来,对身份认证协议的形式化模拟和验证受到越来越来多的关注.因为身份认证协议一般很短,而且并不十分复杂,可以用一些非形式化的证明方法来分析或验证它的正确性.但如果这些协议并发执行,分析它们的行为就非常困难.因此许多学者都致力于研究有效分析这些协议的方法,目前关于模拟和验证身份认证协议的方法大致有三种:数学证明、逻辑演绎和模型检测.Bellare, Rogaway, Shoup和Rubin给出了一个关于安全协议正确性的严格的
8、数学证明 1 .他们利用伪随机函数的性质和数学证明方法证明:当入侵者试图从协议会话(session)所产生的密钥中截获一个密钥时,不具有统计优势.关于逻辑演绎方面,一个成功推理安全协议的最早尝试是BAN 逻辑, 它是由Burrows, Abadi和Needham 3三人提出的,因而称为BAN 逻辑.BAN逻辑是一种基于信任的逻辑,它可以表达和演绎安全协议所涉及的属性,也能表达入侵者的行为规则.尽管应用这个框架自动证明协议的正确性不很直观,但BAN 逻辑仍以其简单和高度抽象等优点受广大研究者的欢迎.第三种技术是模型检测(model checking).它的基本思想是将协议表示成一个状态集合和一个
9、状态转移集合,而且入侵者的各种行为、往来于协议参与者之间的消息以及那些所有参与者都知道的信息也都被考虑进这个状态集合和状态转移集合.遍历整个状态空间,检查是否能够到达某个感兴趣的状态,或者到达可以引发某个感兴趣的行为的状态.已经有很多种模型检测工具被用来模拟和验证安全协议.Meadows 利用Dolev-Yao的推广模型 4 开发了一个基于PROLOG 的model-checking 工具 5 .在他们的系统中,用户可以利用一组描述入侵者如何产生知识的规则来模拟协议.Woo和Lam提出了一个更直观的身份认证协议的模型 2 .该模型类似于顺序编程,独立模拟每个协议参与者.Lowe利用CSP的 m
10、odel-checking 工具 FDR 分析了 Needham-Schroeder Public-Key身份认证协议 6 ,成功地发现了以前未公布的错误.但不幸的是,安全协议的CSP模型非常不直观,而且它是以参与者的时限(nonce,参与者发布的具有时效性的随机数)为参数的,也就是说,这个模型只能模拟协议的一次运行.若要证明整个协议的正确性,还需要做进一步证明.此外,ZheDang等利用ASTRAL Model Checking工具分析了加密协议 7 .张玉清等利用SMV 分析了只有一对主体参加的Needham-Schroeder公钥协议 10 .关于对Spin的应用,Audun Jeasa
11、ng 8提出了一些关于如何用Spin/Promela模拟和验证安全协议的思想,并给出了关于实现技术的简短描述,同时也提出了一些困难,如系统描述、模型实现以及状态爆炸等.本文给出一个简单的模型,它不仅可以模拟协议的多次运行,而且还可以模拟多对主体同时进行身份认证.给出了该模型的Spin实现,从而使身份认证协议的验证变得简单易用.2身份认证协议模型身份认证协议通常运行在连接协议参与者(也称主体)的网络上,并且参与者可以在这个网络(通信媒体)上进行异步通信.通信媒体本质上是被动的,可以被怀有恶意的主体利用、截获或干涉网络通信的内容.网络包含一个主体(principal)集合,其中一部分主体是可靠的,
12、它们总是按照协议的规则进行动作,相应地,另外一些主体是不可靠的,它们可以进行破坏性操作.因为不可靠主体能破坏通信媒体,所以可以将它与通信媒体一起模拟成一个进程,称为入侵者.入侵者能够存储、解密传输在媒体中的消息,它也能加密数据产生新的消息,并将其发送出去以误导可靠主体.同一主体在不同的协议会话中起不同的作用,例如发起一个协议会话的主体称为发起者,而被发起者所联系的主体称为响应者.容易看出,协议可以被转化为一个命令(如SEND, RECEIVE, NEWNONCE)序列 9 .实事上,这种转化可从协议运行中产生的消息序列自动地对应过来.一旦生成了这个动作序列,它们的交叉复合便构成了整个协议的模型
13、.2.1主体模型主体可用一个二元组S , p来表示,其中,S 是局部信息,包括会话的局部状态、一个密钥集和一个时限(nonce)集;p是一个在一组规则约束下的动作序列,通过这组规则可以确定在给定的通话中,究竟哪个用户充当发起者,哪个用户充当响应者.2.2协议模型身份认证协议模型实质上是一组主体动作的异步复合.所以全局状态可被模拟成一组主体动作的异步复合和一组计数器,这组记数器以一对相互会话主体的id为下标.因此身份认证模型可以表示成一个三元组, Ci(j, k), Cr(j, k)表示, 其中,是一组可靠主体与一个不可靠主体动作的异步复合,它产生一个异步交叉语意,但一对相互进行通信的进程仍是同
14、步的;Ci(j ,k)为主体id 主体id N时, 主体j向主体k发起会话的次数与主体k完成响应主体j的次数之差;Cr(j ,k)为主体 id 主体id N 时, 主体j开始响应主体k 的次数与主体k 完成发起主体j的次数之差.2.3协议的基本动作主体可以执行的动作可被分成内部动作和通信动作.内部动作可以异步执行,任何主体都允许执行内部动作,并当有多个主体同时参与协议时,用交叉196 计算机学报 2003年复合来模拟所有可能行为.通信动作包括发送和接收,它仅当一对进程同时进行状态转移时出现.有4种关键的动作:BegInit, EndInit, BegRe-spond 和EndRespond,
15、其语义如下:BegInit(k)表示向k 发起会话请求.EndInit(j)表示完成与j的会话请求.BegRespond(j)表示开始响应j的会话请求.EndRespond(j)表示完成对j的会话响应.这些动作蕴含在每个主体的具体动作中,例如Needham Schroeder协议中主体A通过向B发送消息Na, A Kb,首先发起会话请求,这个发送消息的动作就是BegInit(B)动作.类似的,主体B 收到这个消息时,首先要对其解密,这就是BegRespond(A)动作.当A收到由B发来的响应信息 Na,Nb Ka后,便完成了发起动作(即EndInit(B);当B收到由 A发来的确认信息后,便完
16、成了响应动作(EndRespond(A).2.4模型的动作语意用以上4个动作触发全局变量的更新就可以实时监视以下内容:当用户j完成了与k 的会话(执行EndInit(k)时,用户k 是否已经参与到此次通话(执行BegRespond(j).具体如下:主体j BegInit k Ci(j,k)Ci(j,k)+1;主体k EndRespond j Ci(j,k)Ci(j,k)-1 ;主体j BegRespond k Cr(j,k)Cr(j,k)+1;主体k EndInit j Cr(j,k)Cr(j,k)-1.第一行表示,当主体j向k发出动作BegInit时,全局变量Ci(j,k)加1;第二行表示,当主体k 完成响应j的动作时,全局变量Ci(j,k)减1;第三行表示,当主体j开始响应k时,全局变量Cr(j,k)加1;第四行表示,当主体k向j发起通话的动作结束时,全局变量Cr(j,k)减1.3身份验证协
