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

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

2、信任2021/4/16Kailar術(shù)語集合續(xù)(1).強(qiáng)證明：A CanProof x如果對(duì)于任一主體B, A執(zhí)行一系列操作之后沒有向B泄漏任何秘密消息y(y不等于x)并且能夠使B相信x，則稱主體A能夠證明命題x。包括以下兩種情況： 可傳遞的證明1)不可傳遞的證明2021/4/17Kailar術(shù)語集合續(xù)可傳遞的證明如果A可向B證明x之后，B可向其他主體證明x的成立，則稱A對(duì)于x的證明是可傳遞給B的。2）不可傳遞的證明如果B在A向其證明了x之后，并不能夠向其他主體證明x是成立的，則稱A對(duì)于x的證明是不可傳遞給B的。2021/4/18Kailar術(shù)語集合續(xù)(2)弱證明：A CanProof x to

3、 B主體A可在不泄漏任何秘密的前提下向一個(gè)特定主體B證明x的成立?？蓚鬟f證明不可專遞證明2021/4/19Kailar術(shù)語集合續(xù)簽名認(rèn)證Ka可用于認(rèn)證A對(duì)消息的簽名，而且毫無疑問地可以將A與用Ka-1加密的消息相聯(lián)系。消息解釋x in mx為m中的可被理解的一個(gè)域或聯(lián)合域。通?？杀焕斫獾挠蛑该魑幕蛑黧w擁有密鑰的加密域。2021/4/110Kailar術(shù)語集合續(xù)聲明斷言：A says x 主體A聲明x并對(duì)x及其所能夠推導(dǎo)的公式負(fù)責(zé)，而且如果A對(duì)一個(gè)消息串負(fù)責(zé)，那么A也對(duì)每一個(gè) 子消息負(fù)責(zé)，即：A says (X,Y) = A says x2021/4/111Kailar術(shù)語集合續(xù)簽名消息的接收：

4、A Received m SignedWith K-1A Received m SignedWith K-1: x in m A Received x SignedWith K-12021/4/112Kailar術(shù)語集合續(xù)信任: A Is TrustedOn xA 對(duì)公式x具有管轄權(quán)。信任可分為兩個(gè)級(jí)別：全局信任：如果A是全局可信的, 那么對(duì)于所有主體有 A Is TrustedOn x。2) 非全局信任：如果A是非全局可信的, 那么對(duì)于所有主體有 A Is TrustedOn x by B。2021/4/113Kailar分析假設(shè)數(shù)字簽名算法誠實(shí)性消息完整性服務(wù)器的有效性2021/4/114

5、Kailar分析假設(shè)數(shù)字簽名算法 假設(shè)算法是完美的，不會(huì)被破解，可提供消息源的認(rèn)證、消息內(nèi)容的完整性和消息發(fā)送者的不可否認(rèn)性。誠實(shí)性在非對(duì)稱密碼體制中，主體不會(huì)將其私鑰泄漏給其他人而在對(duì)稱密碼體制中，主體不會(huì)偽裝成與其共享密鑰的主體。2021/4/115Kailar分析假設(shè)(3) 消息完整性 不可能用其他消息部分偽造簽名消息或者計(jì)算出主體的私鑰密鑰并進(jìn)而偽造簽名。服務(wù)器的有效性語句A CanProof x 表明，在未來某個(gè)時(shí)間A可以發(fā)送一些消息來證明x，而一旦出現(xiàn)拒絕服務(wù)問題使得A無法發(fā)送消息以證明x的成立，那么此類問題將被消除以保證服務(wù)器的有效性。2021/4/116Kailar基本推理規(guī)則

6、一般規(guī)則1)聯(lián)接2)蘊(yùn)含3)信仰關(guān)系4)強(qiáng)弱證明關(guān)系5)全局與非全局的可信性可追究性規(guī)則1)簽名2)信任2021/4/117Kailar基本推理規(guī)則一般規(guī)則聯(lián)接Conj: A CanProve x; A CanProve yA CanProof (xy)蘊(yùn)含Inf:A CanProve x; xyA CanProve y2021/4/118Kailar基本推理規(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

7、 to B)(A CanProve x to B)2021/4/119Kailar基本推理規(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的成立。2021/4/120Kailar基本推理規(guī)則可追究性規(guī)則簽名當(dāng)一個(gè)主體對(duì)一個(gè)消息簽名之后，則簽名消息就與主體進(jìn)行了綁定并具有可追究性。Sign:A Receives (m SignedWith K-1);x in

8、 m; A CanProve (K Authenticates B)A CanProve (B Says x)2021/4/121Kailar基本推理規(guī)則信任Trust:A CanProve (B Says x); A CanProve (B IsTrustedOn x)A CanProve x如果A能夠證明B聲明了x,并且能夠證明B對(duì)公式有管轄權(quán)，那么A能夠證明公式x成立。2021/4/122Kailar邏輯的應(yīng)用實(shí)例明確協(xié)議的可追究性目標(biāo)。說明協(xié)議語句，并將其轉(zhuǎn)化為邏輯公式。(關(guān)注簽名)初始化協(xié)議假設(shè)條件。運(yùn)用推理規(guī)則對(duì)形式化分析協(xié)議是否達(dá)成可追究性目標(biāo)。如果未達(dá)成則意味著協(xié)議有漏洞。20

9、21/4/123Kailar邏輯的應(yīng)用實(shí)例續(xù)CMP1 協(xié)議(電子郵件的不可否認(rèn)性)AB:A,B,S,h(M), Kks,A,B,S,Mka-1kBS:A,B,S,h(M)kb-1, Kks,A,B,S,Mka-1kSB: A,B,S,Mka-1ks-1SA: A,B,S,h(M)kb-1,B,Mks-1本協(xié)議將反復(fù)執(zhí)行3) 4)步，以保證A和B都能收到相應(yīng)的消息。2021/4/124Kailar邏輯的應(yīng)用實(shí)例續(xù)CMP1協(xié)議的目標(biāo)形式化描述為：(G1) A CanProve (B received M)(G2) B CanProve(A Sent M)2021/4/125Kailar邏輯的應(yīng)用實(shí)

10、例續(xù)協(xié)議語句的形式化：2)S Receives h(M)SignedWith kb-12”) S Receives h(M) SignedWith ka-13) B Receives h(M) SignedWith ka-1) SignedWith ks-14) A Receives (h(M)SignedWith kb-1 SignedWith ks-1 4”) A Receives (B,M) SignedWith ks-12021/4/126Kailar邏輯的應(yīng)用實(shí)例續(xù)協(xié)議的初始假設(shè)I1: A,B CanProve (Ks Authenticates S)I2: A,S CanProve

11、 (Kb Authenticates B)I3: B,S CanProve (Ka Authenticates A)I4: A,B CanProve (S IsTrusted (S say)I5: A Says M A Sent MI6: B Says h(M) B Received h(M)2021/4/127Kailar邏輯的應(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è)，合理性需要推敲。2021/4/1

12、28Kailar邏輯的應(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)2021/4/129Kailar邏輯的應(yīng)用實(shí)例續(xù)2.由上述結(jié)論和初始假設(shè)I6,應(yīng)用蘊(yùn)含規(guī)則可得：I6: B Says h(M) B R

13、eceived h(M)蘊(yùn)含規(guī)則：Inf:A CanProve x; xyA CanProve y結(jié)論：S CanProve (B Received h(M)2021/4/130Kailar邏輯的應(yīng)用實(shí)例續(xù)3.由公式2”)和初始假設(shè)I3,應(yīng)用簽名規(guī)則可得：公式2) S Receives h(M)SignedWith ka-1I3: B,S CanProve (Ka Authenticates A)結(jié)論：S CanProve (A Says M)2021/4/131Kailar邏輯的應(yīng)用實(shí)例續(xù)4.由上述結(jié)論和初始假設(shè)I5，應(yīng)用蘊(yùn)含規(guī)則可得：初始假設(shè)I5: A Says M A Sent MS C

14、anProve (A Sent M)2021/4/132Kailar邏輯的應(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)2021/4/133Kailar邏輯的應(yīng)用實(shí)例續(xù)由上述結(jié)論和初始假設(shè)I4,應(yīng)用信任規(guī)則可得：信任規(guī)則：Trust:A CanProve (B Says x); A CanProve (B IsTrusted

15、On x)A CanProve xI4:A,B CanProve (S IsTrusted (S say)結(jié)論：B CanProve (M SignedWith Ks-1)2021/4/134Kailar邏輯的應(yīng)用實(shí)例續(xù)7. 對(duì)上述結(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)2021/4/135Kailar邏輯的應(yīng)用實(shí)例續(xù) 證明G11. 同理，由公式4) 和初始假設(shè)I1、I4和I6，應(yīng)用簽名、信任和蘊(yùn)含規(guī)則可得：結(jié)論： ACanProve (B Receive

16、s h(M)2021/4/136Kailar邏輯的應(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)2021/4/137Kailar邏輯的應(yīng)用實(shí)例續(xù)3.對(duì)以上結(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)2021/4/138Kailar邏輯的應(yīng)用實(shí)例續(xù)4.對(duì)以上結(jié)果和初始假設(shè)I4,應(yīng)用信

17、任規(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)2021/4/139Kailar邏輯的應(yīng)用實(shí)例續(xù)由前述結(jié)論A CanProve (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)對(duì)以上結(jié)果和初始假設(shè)I5,應(yīng)用蘊(yùn)含規(guī)則可得：(G2) A Ca