文档介绍：安全协议实验报告一、实验题目:安全协议分析二、实验目的:使用scyther对协议的安全性进行分析,掌握scyther分析协议的方法三、 -1:(roleI{freshTa:Timestamp;//产生Ta为时间戳freshNa,Xa,Ya:Nonce;//产生Na,Xa,Ya为随机数send_l(T,R,T,{Ta,Na,R,Xa,{Ya}pk(R)}sk(T));〃发送消息到R,消息为Ta,Na,Xa,用R的公钥加密的Ya,并用I的私钥加密claim2(1,Nisynch);Thisclaimisuselessastherearenoprecedingrecvevents}roleRvarTa:Timestamp;//定义Ta为时间戳varNa,Xa,Ya:Nonce;//定义Na,Xa,Ya为随机数recv_l(I,R,I,(Ta,Na,R,Xa,(Ya}pk(R)}sk(I))://接收来自I的消息,消息为Ta,Na,Xa,用R的公钥加密的Ya,并用T的私钥加密claim_3(R,Nisynch);//断言:非单射一致性#ThereshouldalsobeFreshXaandFreshYaclaimshere})-1:(roleI{freshTa:Timestamp;//产生时间戳TavarTb:Timestamp;//定义时间戳TbfreshNa,Xa,Ya:Nonce;//产生随机数Na,Xa,YavarXb,Nb,Yb:Nonce;//定义随机数Xb,Nb,Ybsend1(I,R,I,{Ta,Na,R,Xa,{Ya}pk(R)}sk(I));//I发送消息给R,消息为Ta,Na,Xa,用R的公钥加密的Ya,并用T的私钥加密recv2(R,I,R,{Tb,Nb,I,Na,Xb,{Yb}pk(I)}sk(R));//接收来自R的消息,消息为Tb,Nb,Na,Xb,用T的公钥加密的Yb,并用R的私钥加密send_3(I,R,I,{Nb}sk(I));//发送用自己私钥加密的Nb给RclaimT1(T,Nisynch);〃断言:有非单射一致性claimJ2(I,Secret,Ya);〃断言:Ya有保密性claim13(1,Secret,Yb);//断言:Yb有保密性roleR(varTa:Timestamp;//定义时间戳TafreshTb:Timestamp;//产生时间戳TbvarNa,Xa,Ya:Nonce;//定义随机数Na,Xa,Ya:freshXb,Yb,Nb:Nonce;//产生随机数Xb,Yb,Nbrecv1(I,R,I,{Ta,Na,R,Xa,{Ya}pk