安全协议课程实验报告
姓名主讲教师吴汉炜
专
业
信息安全
班级
2
学
号
201016163100实验日期2012-10-23
课程名称
安全协议
小组成员
一、实验名称：
NSPK(Needham-Schroeder Public-Key Protocol)的验证二、实验目的：
1．加深对NS 公钥协议的理解。
2．掌握软件分析安全协议的基本方法，认识安全协议的基本描述规则，构建完备的知识体系。三、实验内容及要求
分析NS 协议，并使用Scyther 协议验证软件对其进行安全验证，完成详尽的报告。1．建立对Needham-Schroeder 公钥协议的认识，在此基础上分析其破解途径。2．学会使用软件验证安全协议的方法，即协议的代码描述、攻击方法的分析。3．深入总结实验，进一步发觉安全协议更深层次的知识。四、实验材料、工具、或软件
Microsoft Windows7；Python2.6；Scyther1.0五、实验步骤（或记录）
本次实验共分四步执行：
第一步：查阅相关资料，系统地认识Needham-Schroeder 公钥协议；第二步：思考该协议的验证流程，推敲其攻击破解的方法；第三步：分析协议的代码描述，并做出详细的解释；
第四步：透过Scyther 生成的攻击图，分析其具体的攻击流程。下面按照这四个步骤开始实验并详细叙述。
一、认识NS 协议
Needham-Schroeder 公钥协议时最早提出的密钥建立协议之一，用来提供双向实体认证，但选择性地使用交换随机数ni 和nr ，ni 和nr 作为密钥建立的共享秘密。
1.()()R pk I Ni R I ,:→
2.()()I pk Nr Ni I R ,:→
3.()()
R pk Nr R I :→二、NS 公钥协议攻击
Lowe 发现下述攻击可以使R 不能确认最后一条消息是否来自I 。因为I 从来没有详细地声明她欲与R 对话，故R 不能得到任何保证I 知道R 是她的对等实体。
1.()()E pk I Ni E I ,:→1~.()()R pk I Ni R E ,:→2~.()()I pk Nr Ni E R ,:→
2.()()I pk Nr Ni I E ,:→
3.()()E pk Nr E I :→3~.()()
R pk Nr R E :→上述攻击方法中I 与E 为正常通信，但是I 充当了信使（Oracle ），使E 成功假冒I 与R 进行了通信。三、
分析代码描述
/*
*Needham-Schroeder protocol */
//PKI infrastructure
const pk:Function;//定义公钥常量pk secret sk:Function;//定义私钥sk inversekeys (pk,sk);//一对公私钥//The protocol description protocol ns3(I,R)//两个实体I 和R {
role I//协议发起者{
const ni:Nonce;//I 自己产生的为常量var nr:Nonce;//不是自己产生的为变量
send_1(I,R,{ni,I}pk(R));//用R 的公钥加密ni 和I ，并发送给R read_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 已获取秘密随机数nr claim_i3(I,Niagree);//声明I 完成非单射一致性
claim_i4(I,Nisynch);//声明I完成单射一致性（最严格），协议只允许一个回合}
role R//协议响应者
{
var ni:Nonce;//不是自己产生的，I产生的为变量
const nr: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);
}
}
//An untrusted agent,with leaked information不受信任的代理人与被泄露的消息
const Eve:Agent;//攻击者扮演了代理人的角色：实体Eve
untrusted Eve;
compromised sk(Eve);//代理人的密钥sk（Eve）
四、分析攻击流程
导出其完整的流程图如下：
//④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．深入总结实验，进一步发觉安全协议更深层次的知识。
四、实验材料、工具、或软件
Microsoft WindowsXP；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:principal
Na,Nb:nonce
Ta,Tb:timestamp
Ya,Yb:userdata
Xa,Xb:userdata
PK,SK:principal->key(keypair)
1.A->B:A,{Ta,Na,B,Xa,{Ya}PK(B)}SK(A)
（2）三路认证：