X509一路认证协议.doc

安全协议 X.509一路认证协议验证实验报告姓 名： 学 号： 学 院： 成 绩： 任课教师： 二一二年十月二十三日计算机类课程实验报告姓 名 主讲教师 专 业 班级 学 号 实验日期 课程名称安全协议小组成员一、 实验名称：X509一路认证协议的验证。二、实验目的：1加深对X509一路认证协议的理解。2掌握软件分析安全协议的基本方法，认识安全协议的基本描述规则，构建完备的知识体系。三、实验内容及要求分析X509一路认证协议，并使用Scyther协议验证软件对其进行安全验证，完成详尽的报告。1建立对X509一路认证协议的认识，在此基础上分析其破解途径。2学会使用软件验证安全协议的方法，即协议的代码描述、攻击方法的分析。3深入总结实验，进一步发觉安全协议更深层次的知识。四、实验材料、工具、或软件Microsoft Windows7；Python2.6；Scyther1.0五、实验步骤（或记录）本次实验共分四步执行：第一步：查阅相关资料，系统地认识X509一路认证协议；第二步：思考该协议的验证流程，推敲其攻击破解的方法；第三步：分析协议的代码描述，并做出详细的解释；第四步：透过Scyther生成的攻击图，分析其具体的攻击流程。下面按照这四个步骤开始实验并详细叙述。一、认识X509一路认证协议1.AB：TA,NA,B,EB(KAB),SigA(TA,NA,B,EB(KAB) A给B发送TA（确保消息的新鲜性）、随机数NA（A给B的挑战）、B的主体标识（表明这条消息是发给B的），用B的公钥加密的会话秘钥KAB，还有A的签名。二、X509一路认证协议攻击1.AI(B)：TA,NA,B,EB(KAB),SigA(TA,NA,B,EB(KAB) /I冒充B截获了A要给B发送的信息，并解密得到里面的内容三、分析代码描述# CCITT X.509 (1) /X.509一路认证协议# Modelled after the description in the SPORE library# http:/www.lsv.ens-cachan.fr/spore/ccittx509_1.html# Note:# The attack in SPORE is not found as this is not an attack against# synchronisation, but an attack against the freshness of Xa and Ya# which can currently not be modelled in scyther#const pk: Function; /定义一个公钥secret sk: Function; /定义一个私钥inversekeys(pk,sk); /声明一对匹配的公、私钥usertype Timestamp; /声明用户自定义类型的时间戳protocol ccitt509-1(I,R) /协议ccitt509-1中有两个实体I，R role I /人物I const Ta: Timestamp; /定义一个常量Ta作为时间戳 const Na,Xa,Ya: Nonce; /定义I产生的随机常量Na,Xa,Ya send_1(I,R, I,Ta, Na, R, Xa,Yapk(R)sk(I); /I用R的公钥加密I产生 的随机数Ya，再用自己的私钥加密信息Ta, Na, R, Xa,和加密后的Ya，然后发送给R # claim_2(I,Nisynch); /声明I完成单射一致性 # This claim is useless as there are no preceding read events role R /人物R var Ta: Timestamp; /定义一个变量Ta作为时间戳 var Na,Xa,Ya: Nonce; /定义随机变量Na,Xa,Ya read_1(I,R, I,Ta, Na, R, Xa,Yapk(R)sk(I); /R读取I发送的用I私钥加密的信息 claim_3(R,Nisynch); /声明R完成单射一致性 # There should also be Fresh Xa and Fresh Ya claims here const Alice,Bob,Eve: Agent; /实体Alice,Bob,Eve是代理者untrusted Eve; /Eve是不受信任的const ne: Nonce; /定义常量neconst te: Timestamp; /定义时间戳te是常量compromised sk(Eve); /通过协商所得的Eve的私钥， Eve是合法用户，其身份得到Alice和Bob的承认四、分析攻击流程扫描结果显示协议存在攻击