《安全協(xié)議理論與方法-中國科學(xué)技術(shù)大學(xué).ppt》由會員分享，可在線閱讀，更多相關(guān)《安全協(xié)議理論與方法-中國科學(xué)技術(shù)大學(xué).ppt（40頁珍藏版）》請在裝配圖網(wǎng)上搜索。

1、安全協(xié)議理論與方法,基于推理結(jié)構(gòu)性方法,Kailar邏輯,可追究性的分析。 內(nèi)容：某個主體要向第三方證明另一方對某 個公式負有責(zé)任。,Kailar邏輯的基本結(jié)構(gòu),術(shù)語集合(基本語句)。 推理規(guī)則及公理。 基于的假設(shè)。,Kailar術(shù)語集合,A,B,C: 協(xié)議主體。 M：由一個主體發(fā)送給另一個主體的消息。 TTP: 可信第三方。 Ki: 主體i的公開密鑰。 Ki-1:與K對應(yīng)的主體i的秘密密鑰。 x,y:為命題。,Kailar術(shù)語集合續(xù),Kailar邏輯的基本語句如下： 強證明 弱證明 簽名認證 消息解釋 聲明斷言 簽名消息的接收 信任,Kailar術(shù)語集合續(xù),(1).強證明：A CanPro

2、of x 如果對于任一主體B, A執(zhí)行一系列操作之后沒有向B泄漏任何秘密消息y(y不等于x)并且能夠使B相信x，則稱主體A能夠證明命題x。包括以下兩種情況： 可傳遞的證明 不可傳遞的證明,Kailar術(shù)語集合續(xù),可傳遞的證明 如果A可向B證明x之后，B可向其他主體證明x的成立，則稱A對于x的證明是可傳遞給B的。 2）不可傳遞的證明 如果B在A向其證明了x之后，并不能夠向其他主體證明x是成立的，則稱A對于x的證明是不可傳遞給B的。,Kailar術(shù)語集合續(xù),(2)弱證明：A CanProof x to B 主體A可在不泄漏任何秘密的前提下向一個特定主體B證明x的成立。 可傳遞證明 不可專遞證明,K

3、ailar術(shù)語集合續(xù),簽名認證 Ka可用于認證A對消息的簽名，而且毫無疑問地可以將A與用Ka-1加密的消息相聯(lián)系。 消息解釋x in m x為m中的可被理解的一個域或聯(lián)合域。 通?？杀焕斫獾挠蛑该魑幕蛑黧w擁有密鑰的加密域。,Kailar術(shù)語集合續(xù),聲明斷言：A says x 主體A聲明x并對x及其所能夠推導(dǎo)的公式負責(zé)，而且如果A對一個消息串負責(zé)，那么A也對每一個 子消息負責(zé)，即： A says (X,Y) = A says x,Kailar術(shù)語集合續(xù),簽名消息的接收：A Received m SignedWith K-1 A Received m SignedWith K-1: x in

4、m A Received x SignedWith K-1,Kailar術(shù)語集合續(xù),信任: A Is TrustedOn x A 對公式x具有管轄權(quán)。信任可分為兩個級別： 全局信任：如果A是全局可信的, 那么對于所有主體有 A Is TrustedOn x。 2)非全局信任：如果A是非全局可信的, 那么對于所有主體有 A Is TrustedOn x by B。,Kailar分析假設(shè),數(shù)字簽名算法 誠實性 消息完整性 服務(wù)器的有效性,Kailar分析假設(shè),數(shù)字簽名算法 假設(shè)算法是完美的，不會被破解，可提供消息源的認證、消息內(nèi)容的完整性和消息發(fā)送者的不可否認性。 誠實性 在非對稱密碼體制中

5、，主體不會將其私鑰泄漏給其他人而在對稱密碼體制中，主體不會偽裝成與其共享密鑰的主體。,Kailar分析假設(shè),(3)消息完整性 不可能用其他消息部分偽造簽名消息或者計算出主體的私鑰密鑰并進而偽造簽名。 服務(wù)器的有效性 語句A CanProof x 表明，在未來某個時間A可以發(fā)送一些消息來證明x，而一旦出現(xiàn)拒絕服務(wù)問題使得A無法發(fā)送消息以證明x的成立，那么此類問題將被消除以保證服務(wù)器的有效性。,Kailar基本推理規(guī)則,一般規(guī)則 1)聯(lián)接 2)蘊含 3)信仰關(guān)系 4)強弱證明關(guān)系 5)全局與非全局的可信性 可追究性規(guī)則 1)簽名2)信任,Kailar基本推理規(guī)則,一般規(guī)則 聯(lián)接 Conj:A C

6、anProve x; A CanProve y A CanProof (xy) 蘊含 Inf:A CanProve x; xy A CanProve y,Kailar基本推理規(guī)則,信仰關(guān)系 (A Blieves x) iff(A CanProve x to A) A 相信x,當(dāng)且僅當(dāng)A能夠?qū)ζ渥约鹤C明x是成立的。 強弱證明關(guān)系 (S:C CanProve y)(A CanProve x) (S: C CanProve y to B)(A CanProve x to B),Kailar基本推理規(guī)則,全局與非全局的可信性 (S: C Is TrustedOn y) (A CanProve x) (

7、S:C Is TrustedOn y by B)(A CanProve x to B) 解釋：如果C是為y所信任的，能夠?qū)е翧能證明x,那么，在同樣條件下，C通過B為y所信任可導(dǎo)致A能向B證明x的成立。,Kailar基本推理規(guī)則,可追究性規(guī)則 簽名 當(dāng)一個主體對一個消息簽名之后，則簽名消息就 與主體進行了綁定并具有可追究性。 Sign:A Receives (m SignedWith K-1);x in m; A CanProve (K Authenticates B) A CanProve (B Says x),Kailar基本推理規(guī)則,信任 Trust:A CanProve (B Says

8、 x); A CanProve (B IsTrustedOn x) A CanProve x 如果A能夠證明B聲明了x,并且能夠證明B對公式有管轄權(quán)，那么A能夠證明公式x成立。,Kailar邏輯的應(yīng)用實例,明確協(xié)議的可追究性目標。 說明協(xié)議語句，并將其轉(zhuǎn)化為邏輯公式。(關(guān)注簽名) 初始化協(xié)議假設(shè)條件。 運用推理規(guī)則對形式化分析協(xié)議是否達成可追究性目標。如果未達成則意味著協(xié)議有漏洞。,Kailar邏輯的應(yīng)用實例續(xù),CMP1 協(xié)議(電子郵件的不可否認性) AB:A,B,S,h(M), Kks,A,B,S,Mka-1k BS:A,B,S,h(M)kb-1, Kks,A,B,S,Mka-1k SB:A

9、,B,S,Mka-1ks-1 SA:A,B,S,h(M)kb-1,B,Mks-1 本協(xié)議將反復(fù)執(zhí)行3) 4)步，以保證A和B都能收到相應(yīng)的消息。,Kailar邏輯的應(yīng)用實例續(xù),CMP1協(xié)議的目標形式化描述為： (G1)A CanProve (B received M) (G2)B CanProve(A Sent M),Kailar邏輯的應(yīng)用實例續(xù),協(xié)議語句的形式化： 2)S Receives h(M)SignedWith kb-1 2”) S Receives h(M)SignedWith ka-1 3) B Receives h(M) SignedWith ka-1) SignedWith

10、ks-1 4) A Receives (h(M))SignedWith kb-1 SignedWith ks-1 4”) A Receives (B,M) SignedWith ks-1,Kailar邏輯的應(yīng)用實例續(xù),協(xié)議的初始假設(shè) I1:A,B CanProve (Ks Authenticates S) I2:A,S CanProve (Kb Authenticates B) I3:B,S CanProve (Ka Authenticates A) I4:A,B CanProve (S IsTrusted (S say)) I5:A Says M A Sent M I6:B Says h(M

11、) B Received h(M),Kailar邏輯的應(yīng)用實例續(xù),I7:S Say (B,M) S Say (M had been sent to B) I8:B Receives h(M) M had been sent to B B Received M 前四條是基本假設(shè)。 后四條是擴展假設(shè)，合理性需要推敲。,Kailar邏輯的應(yīng)用實例續(xù),邏輯分析： 1.由公式2) 和初始假設(shè)I2，應(yīng)用簽名規(guī)則可得： 公式2) S Receives h(M)SignedWith kb-1 初始假設(shè)A,S CanProve (Kb Authenticates B) A Receives (m SignedW

12、ith K-1);x in m; A CanProve (K Authenticates B) A CanProve (B Says x) 結(jié)論：S CanProve (B Says h(M)),Kailar邏輯的應(yīng)用實例續(xù),2.由上述結(jié)論和初始假設(shè)I6,應(yīng)用蘊含規(guī)則可得： I6: B Says h(M) B Received h(M) 蘊含規(guī)則：Inf:A CanProve x; xy A CanProve y 結(jié)論：S CanProve (B Received h(M)),Kailar邏輯的應(yīng)用實例續(xù),3.由公式2”)和初始假設(shè)I3,應(yīng)用簽名規(guī)則可得： 公式2) S Receives h(

13、M)SignedWith ka-1 I3:B,S CanProve (Ka Authenticates A) 結(jié)論：S CanProve (A Says M),Kailar邏輯的應(yīng)用實例續(xù),4.由上述結(jié)論和初始假設(shè)I5，應(yīng)用蘊含規(guī)則可得： 初始假設(shè)I5: A Says M A Sent M S CanProve (A Sent M),Kailar邏輯的應(yīng)用實例續(xù),5. 由公式3) 和初始假設(shè)I1,應(yīng)用簽名規(guī)則可得： 3) B Receives h(M) SignedWith ka-1) SignedWith ks-1 I1:A,B CanProve (Ks Authenticates S) 結(jié)

14、論：B CanProve (S Says (M SignedWIthks-1)),Kailar邏輯的應(yīng)用實例續(xù),由上述結(jié)論和初始假設(shè)I4,應(yīng)用信任規(guī)則可得： 信任規(guī)則：Trust:A CanProve (B Says x); A CanProve (B IsTrustedOn x) A CanProve x I4:A,B CanProve (S IsTrusted (S say)) 結(jié)論：B CanProve (M SignedWith Ks-1),Kailar邏輯的應(yīng)用實例續(xù),7. 對上述結(jié)論再次應(yīng)用簽名規(guī)則可得： 結(jié)論：B CanProve (A Says M) 8.由上述結(jié)論和初始假設(shè)I

15、5,應(yīng)用蘊含規(guī)則可得： 結(jié)論 ：(G2)B CanProve (A Sent M),Kailar邏輯的應(yīng)用實例續(xù),證明G1 1. 同理，由公式4) 和初始假設(shè)I1、I4和I6，應(yīng)用簽名、信任和蘊含規(guī)則可得： 結(jié)論： ACanProve (B Receives h(M)),Kailar邏輯的應(yīng)用實例續(xù),2. 由公式4”) 和初始假設(shè)I1,應(yīng)用簽名規(guī)則可得： 公式4”) A Receives (B,M) SignedWith ks-1 結(jié)論：A CanProve (S Says (B,M)),Kailar邏輯的應(yīng)用實例續(xù),3.對以上結(jié)果和初始假設(shè)I7，應(yīng)用蘊含規(guī)則可得： I7:S Say (B,M

16、) S Says (M had been sent to B) 結(jié)論：A CanProve S Says (M had been sent to B),Kailar邏輯的應(yīng)用實例續(xù),4.對以上結(jié)果和初始假設(shè)I4,應(yīng)用信任規(guī)則可得： I4:A,B CanProve (S IsTrusted (S say)) 信任規(guī)則： Trust:A CanProve (B Says x); A CanProve (B IsTrustedOn x) A CanProve x 結(jié)論：A CanProve (M had been sent to B),Kailar邏輯的應(yīng)用實例續(xù),由前述結(jié)論 ACanProve (B Receives h(M)) A CanProve (M had been sent to B) 應(yīng)用聯(lián)接規(guī)則可得： A CanProve (B Receives h(M) M had been sent to B) 對以上結(jié)果和初始假設(shè)I5,應(yīng)用蘊含規(guī)則可得： (G2) A CanProve (B Received M) 故CMP1協(xié)議滿足可追究性。,Kailar 邏輯的缺陷,Kailar邏輯只能分析協(xié)議的可追究性，不能分析協(xié)議的公平性。 Kailar邏輯在解釋協(xié)議語句時，只能解釋那些簽過名的明文消息，因此限制了使用范圍。 推理之前需要引入一些初始化假設(shè)。共有的缺陷。,