安全协议课程实验报告姓名主讲教师吴汉炜专业信息安全班级2学号201016163100实验日期2012-10-23课程名称安全协议小组成员一、实验名称：NSPK(Needham-SchroederPublic-KeyProtocol)的验证二、实验目的：1．加深对NS公钥协议的理解。2．掌握软件分析安全协议的基本方法，认识安全协议的基本描述规则，构建完备
的知识体系。
三、实验内容及要求分析NS协议，并使用Scyther协议验证软件对其进行安全验证，完成详尽的报告。1．建立对Needham-Schroeder公钥协议的认识，在此基础上分析其破解途径。2．学会使用软件验证安全协议的方法，即协议的代码描述、攻击方法的分析。
3．深入总结实验，进一步发觉安全协议更深层次的知识。
四、实验材料、工具、或软件MicrosoftWindows7；Python2.6；Scyther1.0五、实验步骤（或记录）本次实验共分四步执行：第一步：查阅相关资料，系统地认识Needham-Schroeder公钥协议；第二步：思考该协议的验证流程，推敲其攻击破解的方法；第三步：分析协议的代码描述，并做出详细的解释；第四步：透过Scyther生成的攻击图，分析其具体的攻击流程。下面按照这四个步骤开始实验并详细叙述。
一、认识NS协议Needham-Schroeder公钥协议时最早提出的密钥建立协议之一，用来提供双向实体认证，但选择性地使用交换随机数ni和nr，ni和nr作为密钥建立的共享秘密。
1.()()Rpk
INiRI,:→
2.()()Ipk
NrNiIR,:→
3.()()Rpk
NrRI:→
二、NS公钥协议攻击Lowe发现下述攻击可以使R不能确认最后一条消息是否来自I。因为I从来没有详细地声明她欲与R对话，故R不能得到任何保证I知道R是她的对等实体。1.()()Epk
INiEI,:→
1~.()()Rpk
INiRE,:→
2~.()()Ipk
NrNiER,:→
2.()()Ipk
NrNiIE,:→
3.()()Epk
NrEI:→
3~.()()Rpk
NrRE:→
上述攻击方法中I与E为正常通信，但是I充当了信使（Oracle），使E成功假冒I与R进行了通信。
三、分析代码描述/**Needham-Schroederprotocol*/
//PKIinfrastructureconstpk:Function;//定义公钥常量pksecretsk:Function;//定义私钥skinversekeys(pk,sk);//一对公私钥
//Theprotocoldescriptionprotocolns3(I,R)//两个实体I和R{roleI//协议发起者{constni:Nonce;//I自己产生的为常量varnr:Nonce;//不是自己产生的为变量
send_1(I,R,{ni,I}pk(R));//用R的公钥加密ni和I，并发送给Rread_2(R,I,{ni,nr}pk(I));//I接收消息，被挑战send_3(I,R,{nr}pk(R));//I响应挑战
claim_i1(I,Secret,ni);//声明I已获取秘密随机数ni，安全目标，要求ni是秘密的claim_i2(I,Secret,nr);//声明I已获取秘密随机数nrclaim_i3(I,Niagree);//声明I完成非单射一致性claim_i4(I,Nisynch);//声明I完成单射一致性（最严格），协议只允许一个回合}
roleR//协议响应者{varni:Nonce;//不是自己产生的，I产生的为变量constnr:Nonce;//R自己产生的随机数为常量
read_1(I,R,{ni,I}pk(R));send_2(R,I,{ni,nr}pk(I));read_3(I,R,{nr}pk(R));
claim_r1(R,Secret,ni);claim_r2(R,Secret,nr);claim_r3(R,Niagree);claim_r4(R,Nisynch);}}
//Anuntrustedagent,withleakedinformation不受信任的代理人与被泄露的消息constEve:Agent;//攻击者扮演了代理人的角色：实体EveuntrustedEve;compromisedsk(Eve);//代理人的密钥sk（Eve）
四、分析攻击流程导出其完整的流程图如下：4对其分片分析如下：绿色和蓝色均为正常通信，橘色为攻击。
//①Bob是发起方I，他要与Eve正常通信，用Eve的公钥加密随机数ni后发送给Eve。
//②攻击者最初的知识只有：Eve接收到消息后用自己的私钥解密得到ni。然后再用Alice（R）的公钥加密（ni，I）并发送给Alice。
//③Alice从Eve处接收到带有Bob身份标识的认证，解密后用Bob的公钥加密自己和Bob的随机数（ni,nr），发送给Eve，Eve原样发送给Bob。6
六、实验存在问题和解决办法实验存在的主要问题是在第二步中没有加入身份标识，解决办法如下：
1.()()Rpk
INiRI,:→
2.()()Ipk
RNrNiIR,,:→
3.()()Rpk
NrRI:→
加入该身份标识后，由于Eve无法看到第二步中用I的公钥加密的内容，也无法将其中的R修改为他自己的身份标识E。所以如果Eve想让I当预言机，那么他与I的正常通信中，若转发上述第二步消息，则I解密后会发现里面的身份标识为R而不是E，那么I就不会成为预言机。
//④Bob从Eve处接收后，认为在与Eve完成①中的步骤，Bob解密出nr，用Eve的公钥加密后发送给Eve。Eve解密出nr后用Alice的公钥加密发送给Alice，Alice解密后认证Eve为Bob，Eve达到了冒充Bob的目的，在此过程中Alice为Eve的预言机。该协议不满足单射一致性。X.509标准一路和三路认证姓名主讲教师吴汉炜专业信息安全班级2
学号201016163100实验日期2012-10-30课程名称安全协议小组成员一、实验名称：CCITT协议中X.509标准一路和三路认证。二、实验目的：1．加深对X.509协议的理解。2．掌握软件分析安全协议的基本方法，认识安全协议的基本描述规则，构建完备的知识体系。
三、实验内容及要求分析X.509协议，并使用Scyther协议验证软件对其进行安全验证，完成详尽的报告。1．建立对X.509协议的认识，在此基础上分析其破解途径。
2．学会使用软件验证安全协议的方法，即协议的代码描述、攻击方法的分析。3．深入总结实验，进一步发觉安全协议更深层次的知识。四、实验材料、工具、或软件MicrosoftWindowsXP；Python2.6；Scyther1.0五、实验步骤（或记录）本次实验共分四步执行：第一步：查阅相关资料，系统地认识X.509协议；第二步：思考该协议的验证流程，推敲其攻击破解的方法；第三步：分析协议的代码描述，并做出详细的解释；第四步：透过Scyther生成的攻击图，分析其具体的攻击流程。下面按照这四个步骤开始实验并详细叙述。
一、认识X.509协议ITU（以前的CCITT）和ISO一起标准化了X.500系列建议来提供通信目录服务。X.509标准共有三个具体的协议，分别有1个、2个和3个消息流。后两个协议都是在其之前的协议上增加一条消息而来。目的都是从A到B传输会话密钥，后两个协议还从B到A传输会话密钥。下面我们主要来分析一路和三路认证。（1）一路认证：A,B:principalNa,Nb:nonceTa,Tb:timestampYa,Yb:userdataXa,Xb:userdataPK,SK:principal->key(keypair)
1.A->B:A,{Ta,Na,B,Xa,{Ya}PK(B)}SK(A)（2）三路认证：A,B:principalNa,Nb:nonceTa,Tb:timestampYa,Yb:userdataXa,Xb:userdataPK,SK:principal->key(keypair)
1.A->B:A,{Ta,Na,B,Xa,{Ya}PK(B)}SK(A)2.B->A:B,{Tb,Nb,A,Na,Xb,{Yb}PK(A)}SK(B)3.A->B:A,{Nb}SK(A)
二、X.509协议攻击（1）一路认证攻击：1.A->I(B):A,{Ta,Na,B,Xa,{Ya}PK(B)}SK(A)2.I->B:I,{Ta,Na,B,Xa,{Ya}PK(B)}SK(I)上述攻击方法中A想与B通信，但I假冒B接收，修改身份标识，然后转发给B，这样对于A和B来说虽然认证性可以保证，但是Ta,Na,Xa的机密性无法保证。
四、三路认证攻击：1.A->I(B):A,{Ta,Na,B,Xa,{Ya}PK(B)}SK(A)1`.I(A)->B:A,{Ta,Na,B,Xa,{Ya}PK(B)}SK(A)2`.B->I(A):B,{Tb,Nb,A,Na,Xb,{Yb}PK(A)}SK(B)1``.A->I:A,{Ta',Na',I,Xa',{Ya'}PK(I)}SK(A)2``.I->A:I,{Ti,Nb,A,N'a,Xi,{Yi}PK(A)}SK(I)3``.A->I:A,{Nb}SK(A)3`.I(A)->B:A,{Nb}SK(A)上述攻击中，I预先存储了一次A主动发起的会话，然后等待A联络B时截断通信并冒充B得到A发起的会话，接收消息。接着I假冒A转发该消息给B，当B要求I完成会话时，I利用事先存储的与A正常通信，将A当成预言机，得到{Nb}SK(A)，然后冒充A转发给B。这样对于A来说Xa、Ta、Na、Xb、Tb、Nb的机密性无法保证，认证性可以保证。对于B来说，Xa、Ta、Na、Xb、Tb、Nb的机密性无法保证，认证性也无法保证。
三、分析代码描述（1）一路认证：#CCITTX.509(1)##ModelledafterthedescriptionintheSPORElibrary#http://www.lsv.ens-cachan.fr/spore/ccittx509_1.html##Note:#TheattackinSPOREisnotfoundasthisisnotanattackagainst#synchronisation,butanattackagainstthefreshnessofXaandYa#whichcancurrentlynotbemodelledinscyther