安全協(xié)議理論與方法-中國科學技術大學.ppt

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

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

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

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

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

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

6、 x; A CanProve y A CanProof (xy) 蘊含 Inf:A CanProve x; xy A CanProve y,Kailar基本推理規(guī)則,信仰關系 (A Blieves x) iff(A CanProve x to A) A 相信x,當且僅當A能夠?qū)ζ渥约鹤C明x是成立的。 強弱證明關系 (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) (S:C Is

7、TrustedOn y by B)(A CanProve x to B) 解釋：如果C是為y所信任的，能夠?qū)е翧能證明x,那么，在同樣條件下，C通過B為y所信任可導致A能向B證明x的成立。,Kailar基本推理規(guī)則,可追究性規(guī)則 簽名 當一個主體對一個消息簽名之后，則簽名消息就 與主體進行了綁定并具有可追究性。 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 x); A

8、CanProve (B IsTrustedOn x) A CanProve x 如果A能夠證明B聲明了x,并且能夠證明B對公式有管轄權，那么A能夠證明公式x成立。,Kailar邏輯的應用實例,明確協(xié)議的可追究性目標。 說明協(xié)議語句，并將其轉(zhuǎn)化為邏輯公式。(關注簽名) 初始化協(xié)議假設條件。 運用推理規(guī)則對形式化分析協(xié)議是否達成可追究性目標。如果未達成則意味著協(xié)議有漏洞。,Kailar邏輯的應用實例續(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,B,S,Mk

9、a-1ks-1 SA:A,B,S,h(M)kb-1,B,Mks-1 本協(xié)議將反復執(zhí)行3) 4)步，以保證A和B都能收到相應的消息。,Kailar邏輯的應用實例續(xù),CMP1協(xié)議的目標形式化描述為： (G1)A CanProve (B received M) (G2)B CanProve(A Sent M),Kailar邏輯的應用實例續(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 ks-1 4)

10、 A Receives (h(M)SignedWith kb-1 SignedWith ks-1 4”) A Receives (B,M) SignedWith ks-1,Kailar邏輯的應用實例續(xù),協(xié)議的初始假設 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) B Recei

11、ved h(M),Kailar邏輯的應用實例續(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 前四條是基本假設。 后四條是擴展假設，合理性需要推敲。,Kailar邏輯的應用實例續(xù),邏輯分析： 1.由公式2) 和初始假設I2，應用簽名規(guī)則可得： 公式2) S Receives h(M)SignedWith kb-1 初始假設A,S CanProve (Kb Authenticates B) A Receives (m SignedWith K-1);

12、x in m; A CanProve (K Authenticates B) A CanProve (B Says x) 結(jié)論：S CanProve (B Says h(M),Kailar邏輯的應用實例續(xù),2.由上述結(jié)論和初始假設I6,應用蘊含規(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邏輯的應用實例續(xù),3.由公式2”)和初始假設I3,應用簽名規(guī)則可得： 公式2) S Receives h(M)SignedWit

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

14、e (S Says (M SignedWIthks-1),Kailar邏輯的應用實例續(xù),由上述結(jié)論和初始假設I4,應用信任規(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邏輯的應用實例續(xù),7. 對上述結(jié)論再次應用簽名規(guī)則可得： 結(jié)論：B CanProve (A Says M) 8.由上述結(jié)論和初始假設I5,應用蘊含規(guī)則可得： 結(jié)

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

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