安全協(xié)議理論與方法,基于推理結(jié)構(gòu)性方法,Kailar邏輯,可追究性的分析。 內(nèi)容：某個(gè)主體要向第三方證明另一方對某 個(gè)公式負(fù)有責(zé)任。,Kailar邏輯的基本結(jié)構(gòu),術(shù)語集合(基本語句)。 推理規(guī)則及公理。 基于的假設(shè)。,Kailar術(shù)語集合,A,B,C: 協(xié)議主體。 M：由一個(gè)主體發(fā)送給另一個(gè)主體的消息。 TTP: 可信第三方。 Ki: 主體i的公開密鑰。 Ki-1:與K對應(yīng)的主體i的秘密密鑰。 x,y:為命題。,Kailar術(shù)語集合續(xù),Kailar邏輯的基本語句如下： 強(qiáng)證明 弱證明 簽名認(rèn)證 消息解釋 聲明斷言 簽名消息的接收 信任,Kailar術(shù)語集合續(xù),(1).強(qiáng)證明：A CanProof 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可在不泄漏任何秘密的前提下向一個(gè)特定主體B證明x的成立。 可傳遞證明 不可專遞證明,Kailar術(shù)語集合續(xù),簽名認(rèn)證 Ka可用于認(rèn)證A對消息的簽名，而且毫無疑問地可以將A與用Ka-1加密的消息相聯(lián)系。 消息解釋x in m x為m中的可被理解的一個(gè)域或聯(lián)合域。 通?？杀焕斫獾挠蛑该魑幕蛑黧w擁有密鑰的加密域。,Kailar術(shù)語集合續(xù),聲明斷言：A says x 主體A聲明x并對x及其所能夠推導(dǎo)的公式負(fù)責(zé)，而且如果A對一個(gè)消息串負(fù)責(zé)，那么A也對每一個(gè) 子消息負(fù)責(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 m A Received x SignedWith K-1,Kailar術(shù)語集合續(xù),信任: A Is TrustedOn x A 對公式x具有管轄權(quán)。信任可分為兩個(gè)級別： 全局信任：如果A是全局可信的, 那么對于所有主體有 A Is TrustedOn x。 2)非全局信任：如果A是非全局可信的, 那么對于所有主體有 A Is TrustedOn x by B。,Kailar分析假設(shè),數(shù)字簽名算法 誠實(shí)性 消息完整性 服務(wù)器的有效性,Kailar分析假設(shè),數(shù)字簽名算法 假設(shè)算法是完美的，不會被破解，可提供消息源的認(rèn)證、消息內(nèi)容的完整性和消息發(fā)送者的不可否認(rèn)性。 誠實(shí)性 在非對稱密碼體制中，主體不會將其私鑰泄漏給其他人而在對稱密碼體制中，主體不會偽裝成與其共享密鑰的主體。,Kailar分析假設(shè),(3)消息完整性 不可能用其他消息部分偽造簽名消息或者計(jì)算出主體的私鑰密鑰并進(jìn)而偽造簽名。 服務(wù)器的有效性 語句A CanProof x 表明，在未來某個(gè)時(shí)間A可以發(fā)送一些消息來證明x，而一旦出現(xiàn)拒絕服務(wù)問題使得A無法發(fā)送消息以證明x的成立，那么此類問題將被消除以保證服務(wù)器的有效性。,Kailar基本推理規(guī)則,一般規(guī)則 1)聯(lián)接 2)蘊(yùn)含 3)信仰關(guān)系 4)強(qiáng)弱證明關(guān)系 5)全局與非全局的可信性 可追究性規(guī)則 1)簽名2)信任,Kailar基本推理規(guī)則,一般規(guī)則 聯(lián)接 Conj:A CanProve x; A CanProve y A CanProof (xy) 蘊(yùn)含 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是成立的。 強(qiáng)弱證明關(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) (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)一個(gè)主體對一個(gè)消息簽名之后，則簽名消息就 與主體進(jìn)行了綁定并具有可追究性。 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 CanProve (B IsTrustedOn x) A CanProve x 如果A能夠證明B聲明了x,并且能夠證明B對公式有管轄權(quán)，那么A能夠證明公式x成立。,Kailar邏輯的應(yīng)用實(shí)例,明確協(xié)議的可追究性目標(biāo)。 說明協(xié)議語句，并將其轉(zhuǎn)化為邏輯公式。(關(guān)注簽名) 初始化協(xié)議假設(shè)條件。 運(yùn)用推理規(guī)則對形式化分析協(xié)議是否達(dá)成可追究性目標(biāo)。如果未達(dá)成則意味著協(xié)議有漏洞。,Kailar邏輯的應(yīng)用實(shí)例續(xù),CMP1 協(xié)議(電子郵件的不可否認(rèn)性) 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,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)用實(shí)例續(xù),CMP1協(xié)議的目標(biāo)形式化描述為： (G1)A CanProve (B received M) (G2)B CanProve(A Sent M),Kailar邏輯的應(yīng)用實(shí)例續(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) A Receives (h(M)SignedWith kb-1 SignedWith ks-1 4”) A Receives (B,M) SignedWith ks-1,Kailar邏輯的應(yīng)用實(shí)例續(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) B Received h(M),Kailar邏輯的應(yīng)用實(shí)例續(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è)。 后四條是擴(kuò)展假設(shè)，合理性需要推敲。,Kailar邏輯的應(yīng)用實(shí)例續(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 SignedWith 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)用實(shí)例續(xù),2.由上述結(jié)論和初始假設(shè)I6,應(yīng)用蘊(yùn)含規(guī)則可得： I6: B Says h(M) B Received h(M) 蘊(yùn)含規(guī)則：Inf:A CanProve x; xy A CanProve y 結(jié)論：S CanProve (B Received h(M),Kailar邏輯的應(yīng)用實(shí)例續(xù),3.由公式2”)和初始假設(shè)I3,應(yīng)用簽名規(guī)則可得： 公式2) S Receives h(M)SignedWith ka-1 I3:B,S CanProve (Ka Authenticates A) 結(jié)論：S CanProve (A Says M),Kailar邏輯的應(yīng)用實(shí)例續(xù),4.由上述結(jié)論和初始假設(shè)I5，應(yīng)用蘊(yùn)含規(guī)則可得： 初始假設(shè)I5: A Says M A Sent M S CanProve (A Sent M),Kailar邏輯的應(yīng)用實(shí)例續(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é)論：B CanProve (S Says (M SignedWIthks-1),Kailar邏輯的應(yīng)用實(shí)例續(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)用實(shí)例續(xù),7. 對上述結(jié)論再次應(yīng)用簽名規(guī)則可得： 結(jié)論：B CanProve (A Says M) 8.由上述結(jié)論和初始假設(shè)I5,應(yīng)用蘊(yùn)含規(guī)則可得： 結(jié)論 ：(G2)B CanProve (A Sent M),Kailar邏輯的應(yīng)用實(shí)例續(xù),證明G1 1. 同理，由公式4) 和初始假設(shè)I1、I4和I6，應(yīng)用簽名、信任和蘊(yùn)含規(guī)則可得： 結(jié)論： ACanProve (B Receives h(M),Kailar邏輯的應(yīng)用實(shí)例續(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)用實(shí)例續(xù),3.對以上結(jié)果和初始假設(shè)I7，應(yīng)用蘊(yùn)含規(guī)則可得： I7:S Say (B,M) S Says (M had been sent to B) 結(jié)論：A CanProve S Says (M had been sent to B),Kailar邏輯的應(yīng)用實(shí)例續(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)用實(shí)例續(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)用蘊(yùn)含規(guī)則可得： (G2) A CanProve (B Received M) 故CMP1協(xié)議滿足可追究性。,Kailar 邏輯的缺陷,Kailar邏輯只能分析協(xié)議的可追究性，不能分析協(xié)議的公平性。 Kailar邏輯在解釋協(xié)議語句時(shí)，只能解釋那些簽過名的明文消息，因此限制了使用范圍。 推理之前需要引入一些初始化假設(shè)。共有的缺陷。,