安全協(xié)議X.509三路認證協(xié)議驗證實驗報告姓 名： 學(xué) 號： 學(xué) 院： 成 績： 任課教師： 二一二年十月二十三日II計算機類課程實驗報告姓 名主講教師專 業(yè)班級學(xué) 號實驗日期課程名稱安全協(xié)議小組成員一、 實驗名稱：X509三路認證協(xié)議的驗證。二、實驗?zāi)康模?加深對X509三路認證協(xié)議的理解。2掌握軟件分析安全協(xié)議的基本方法，認識安全協(xié)議的基本描述規(guī)則，構(gòu)建完備的知識體系。三、實驗內(nèi)容及要求分析X509三路認證協(xié)議，并使用Scyther協(xié)議驗證軟件對其進行安全驗證，完成詳盡的報告。1建立對X509三路認證協(xié)議的認識，在此基礎(chǔ)上分析其破解途徑。2學(xué)會使用軟件驗證安全協(xié)議的方法，即協(xié)議的代碼描述、攻擊方法的分析。3深入總結(jié)實驗，進一步發(fā)覺安全協(xié)議更深層次的知識四、實驗材料、工具、或軟件Microsoft Windows7；Python2.6；Scyther1.0五、實驗步驟（或記錄）本次實驗共分四步執(zhí)行：第一步：查閱相關(guān)資料，系統(tǒng)地認識X509三路認證協(xié)議；第二步：思考該協(xié)議的驗證流程，推敲其攻擊破解的方法；第三步：分析協(xié)議的代碼描述，并做出詳細的解釋；第四步：透過Scyther生成的攻擊圖，分析其具體的攻擊流程。下面按照這四個步驟開始實驗并詳細敘述。一、認識X509三路認證協(xié)議 1.AB：TA,NA,B,EB(KAB),SigA(TA,NA,B,EB(KAB) / A給B發(fā)送TA（確保消息的新鮮性）、隨機數(shù)NA（A給B的挑戰(zhàn)）、B的主體標(biāo)識（表明這條消息是發(fā)給B的），用B的公鑰加密的會話秘鑰KAB，還有A的簽名。 2.BA：TB,NB,A,NA,EA(KBA),SigB(TB,NB,A,NA,EA(KBA) /B用私鑰解密得到會話秘鑰KBA，用A的公鑰加密，把產(chǎn)生的時間戳TB，隨機數(shù)NB，A的主體標(biāo)識，得到的隨機數(shù)NA和加密后的會話秘鑰，還有B的簽名發(fā)送給A 3.AB：NB,B, SigA(NB,B) /A給B發(fā)送NB,B和A的簽名表示自己收到消息并確定自己的身份二、 X509三路認證協(xié)議攻擊1. A-I(B):A, Ta, Na, B, Xa, YaPK(B)SK(A) /I截獲A給B發(fā)送的 消息2. I(A)-B:A, Ta, Na, B, Xa, YaPK(B)SK(A) /I冒充A將截獲的 消息轉(zhuǎn)發(fā)給B3. B-I(A):B, Tb, Nb, A, Na, Xb, YbPK(A)SK(B) /B用A公鑰 解密得到隨機數(shù)Na，自己產(chǎn)生時間戳Tb，隨機數(shù)Nb，用自己的私鑰加密Tb, Nb, A, Na, Xb和用A的公鑰加密的Yb，然后發(fā)送給I4. A-I:A, Ta, Na, C, Xa, YaPK(I)SK(A) /A對I發(fā)起會話5. I-A:I, Ti, Nb, A, Na,Xi, YiPK(A)SK(I) /I用合法的身份 將Ti，A，Na,Xi,用A公鑰加密的Yi和從B那解密得到的Nb用自己的私鑰加密后發(fā)送給A6. A-I:A, NbSK(A) /A回復(fù)給I用自己的私鑰加密的Nb， I因此得到NbSK(A)7. I(A)-B:A, NbSK(A) /I將從A出得到信息轉(zhuǎn)發(fā)給B,成功冒充 A三、分析代碼描述# CCITT X.509 (3) /X.509三路認證協(xié)議# Modelled after the description in the SPORE library# http:/www.lsv.ens-cachan.fr/spore/ccittx509_3.html# Note:# The protocol description also states that Xa and Ya should be fresh# this can not be verified using scyther#const pk: Function; /定義一個公鑰secret sk: Function; /定義一個私鑰inversekeys(pk,sk); /聲明一對匹配的公、私鑰usertype Timestamp; /聲明用戶自定義類型的時間戳protocol ccitt509-3(I,R) /協(xié)議ccitt509-3中有兩個實體I，R role I /人物I const Ta: Timestamp; /定義一個常量Ta作為時間戳 var Tb: Timestamp; /定義一個變量Tb作為時間戳 const Na,Xa,Ya: Nonce; /定義I產(chǎn)生的隨機常量Na,Xa,Ya var Xb,Nb,Yb: Nonce; /定義R產(chǎn)生的隨機變量Xb,Nb,Yb send_1(I,R, I,Ta, Na, R, Xa,Yapk(R)sk(I); /I用R的公鑰加密I產(chǎn)生的隨機數(shù)Ya，再用自己的私鑰加密信息Ta, Na, R, Xa,和加密后的Ya，然后發(fā)送給R，確保了Ya的機密性 read_2(R,I, R,Tb, Nb, I, Na, Xb,Ybpk(I)sk(R); /I收到從R發(fā)來的用R的私鑰加密的信息，用R的公鑰解密得到Tb, Nb, I, Na, Xb以及用I的公鑰加密的Yb send_3(I,R, I, Nbsk(I); /I將信息Nb用自己的私鑰加密發(fā)送給R，完成認證 claim_I1(I,Nisynch); /聲明I完成單射一致性 claim_I2(I,Secret,Ya); /聲明I產(chǎn)生的隨機數(shù)Ya是秘密的 claim_I3(I,Secret,Yb); /聲明I獲得的隨機數(shù)Yb是秘密的 role R /人物R var Ta: Timestamp; /定義一個變量Ta作為時間戳 const Tb: Timestamp; /定義一個常量Tb作為時間戳 var Na,Xa,Ya: Nonce; /定義隨機變量Na,Xa,Ya const Xb,Yb,Nb: Nonce; /定義隨機常量Xb,Nb,Yb read_1(I,R, I,Ta, Na, R, Xa,Yapk(R)sk(I); /讀取I發(fā)送的第一條信息 send_2(R,I, R,Tb, Nb, I, Na, Xb,Ybpk(I)sk(R); /R讀取I發(fā)來的信息后，對I發(fā)出的認證信息 read_3(I,R, I, Nbsk(I); /R讀取I發(fā)送的信息，通過認證 claim_R1(R,Nisynch); /聲明R完成單射一致性 claim_R2(R,Secret,Ya); /聲明隨機數(shù)Ya是秘密的 claim_R3(R,Secret,Yb); /聲明隨機數(shù)Yb是秘密的 # 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); /通過協(xié)商所得的Eve的私鑰， Eve是合法用戶，其身份得到Alice和Bob的承認四、分析攻擊流程掃描結(jié)果顯