安全協(xié)議理論與方法

1、安全協(xié)議理論與方法基于推理結(jié)構(gòu)性方法SVO邏輯Syverson和Oracho提出，建立了用于推證合理性的理論模型。提供獨(dú)立明確的語義基礎(chǔ)。相當(dāng)詳細(xì)的模型。消除理解模糊，有助于準(zhǔn)確理解消息的真實(shí)含義和協(xié)議理想化。通用語義，擴(kuò)展性好，簡(jiǎn)潔。SVO邏輯的基本結(jié)構(gòu)術(shù)語集合。 推理規(guī)則及公理。 基于的假設(shè)。SVO術(shù)語集合定義T為初始術(shù)語集合, 包括互不相交的常量符號(hào)集合：主體、共享密鑰、公鑰、私鑰以及序列號(hào)等。 n維函數(shù)表示有n個(gè)變量的函數(shù)，如加、解密函數(shù)等。 消息語言MT：滿足下列性質(zhì)的最小語言集合。1)如果XT，則X是消息。2)如果X1,Xn是消息，F(xiàn)是任意一個(gè)n維函數(shù),則F(X1,Xn)是消息。3

2、)如果是公式，則是消息。SVO術(shù)語集合續(xù)4. 公式語言FT：滿足下列性質(zhì)的最小公式集合。1)如果P是原始命題，則P是公式。如果,是公式，則和是公式。P believes 和P controls 是公式，其中P是主體， 是公式。 P sees X, P says X, P said X, P received X 和fresh(X)是公式,其中P是主體, X是消息。Shared(P,K,Q),PK(P,K)和P has K是公式，其中P是主體， K是消息。SVO邏輯的推理規(guī)則及公理1. SVO邏輯遵從兩條基本推理規(guī)則() P believes SVO邏輯的推理規(guī)則及公理續(xù)1SVO邏輯共有20條公

3、理I1 相信公理對(duì)于任一主體P和公式，有：P believes P believes() P believes P believes P believes ( P believes )SVO邏輯的推理規(guī)則及公理續(xù)2(2) I2源關(guān)聯(lián)公理密鑰用于推斷消息發(fā)送者的身份。shared(P,K,Q)R received XQKQ said X(PK(Q,K)R received XK-1 Q said XPK(Q,K)表示K是主體Q的數(shù)字簽名驗(yàn)證密鑰。它表明如果主體Q收到一個(gè)簽名的消息，并且Q知道簽名的驗(yàn)證密鑰是K，就可以確定發(fā)送者身份。SVO邏輯的推理規(guī)則及公理續(xù)3I3 密鑰協(xié)商公理(PK(P, K

4、P) PK(P, Kq) shared(P,KPq,Q) Kpq= f(Kp, Kq-1) = f(Kp-1, Kq) f為密鑰協(xié)商函數(shù)，比如Diffie-Hellman密鑰交換。SVO邏輯的推理規(guī)則及公理續(xù)4I4 接收公理主體對(duì)接收到的一個(gè)級(jí)聯(lián)的加密消息可用有效的密鑰解密。P received(X1, , Xn) P received XiP received XK P has K-1 P received XSVO邏輯的推理規(guī)則及公理續(xù)5I5 看到公理P received X P sees XP sees (X1,Xn) P sees XiP sees X1P sees Xn P sees

5、 (F(X1,Xn)主體只要接收到一個(gè)消息就看到了這個(gè)消息，并且看到了這個(gè)消息的每一部分。SVO邏輯的推理規(guī)則及公理續(xù)6I6理解公理P believes (P sees F(X) P believes (P sees X) P received F(X) P believes (P sees X) P believes (P received F(X)如果一個(gè)主體理解一個(gè)消息，并看到此消息的一個(gè)函數(shù)，那么它理解它所看到的。F可視為加密函數(shù)，K為參數(shù)。SVO邏輯的推理規(guī)則及公理續(xù)7I7敘述公理一個(gè)主體說過一個(gè)級(jí)聯(lián)消息，那么它一定說過且看到消息的每一部分。P said(X1,Xn) P said

6、Xi P sees XiP says (X1,Xn) P said (X1,Xn) P says XiSVO邏輯的推理規(guī)則及公理續(xù)8仲裁公理P controls P says SVO邏輯的推理規(guī)則及公理續(xù)9I9新鮮公理如果消息的一部分是新鮮的，那么整個(gè)消息也是新鮮的。fresh(Xi) fresh(X1,Xn)fresh(X1,Xn)fresh(F(X1,Xn)fresh(X) P said X P says XSVO邏輯的推理規(guī)則及公理續(xù)10I10 共享密鑰的良好對(duì)稱性公理如果K是P，Q之間的良好密鑰當(dāng)且僅當(dāng)K是Q，P之間的良好密鑰。shared(P,K,Q) shard(Q,K,P)SVO

7、邏輯的推理規(guī)則及公理續(xù)11(11) I11所有公理P has K P sees KSVO邏輯語義計(jì)算模型Pe：代表環(huán)境,可用于模擬攻擊者的任意行為 。Si:每個(gè)主體Pi有一個(gè)局部狀態(tài)Si。全局狀態(tài): n+1維局部狀態(tài)。主體行為:發(fā)送send(X,P)、receive()和generate(X)，但只能生成集合T0中的元素SVO邏輯語義計(jì)算模型續(xù)1每一個(gè)行為導(dǎo)致狀態(tài)的一次遷移。r: 一輪協(xié)議r是一個(gè)由整數(shù)時(shí)間索引的全局變量的有限集合。r(t)：協(xié)議中的t時(shí)記為r(t)。ri(t):對(duì)應(yīng)的主體Pi的局部變量記為ri(t)。環(huán)境狀態(tài)：全局歷史、環(huán)境有效遷移集合和用于保存發(fā)給主體P而P還未收到的消息的

8、消息緩沖區(qū)。SVO邏輯語義計(jì)算模型續(xù)2主體Pi在(r,t)收到的消息集合包括：局部消息歷史中或t之前出現(xiàn)的received(X)中的X。收到的消息的級(jí)聯(lián)。P持有所收到的加密消息XK的解密密鑰，則P可得到X。SVO邏輯語義計(jì)算模型續(xù)3主體Pi在協(xié)議運(yùn)行當(dāng)中某處可看到的消息集合包含：主體已收到的消息集。主體新近生成消息集。主體初始所知的消息集。主體通過規(guī)則和公理從已知的消息集衍生的消息集。對(duì)于主體說過的消息集的定義比此嚴(yán)格。SVO邏輯語義計(jì)算模型續(xù)4主體Pi在(r,t)發(fā)送的消息集合包括：主體對(duì)已發(fā)送過消息的級(jí)聯(lián)。加密密鑰為主體所持有的加密消息的非加密部分，且此部分為主體所看到。簽名密鑰為主體所持

9、有的簽名消息的非簽名部分，且此部分為主體所看到。Hash消息中的非Hash部分，且此部分為主體所看到。SVO邏輯語義公式成立的條件定義：將每一個(gè)常量命題pT映射為點(diǎn)集(p), 即命題p為真的點(diǎn)。公式在點(diǎn)(r,t)為真記為： (r,t) 。 意味著 全真。SVO邏輯語義公式成立的條件1邏輯連接及其原始命題基本邏輯關(guān)系：(r,t) p iff(r,t) (p)。(r,t) iff(r,t) (r,t) 。(r,t) iff 在(r,t)時(shí)不成立。SVO邏輯語義公式成立的條件2原始命題接收命題(r,t) p received X當(dāng)且僅當(dāng)X屬于主體P在(r,t)時(shí)已收消息集合。SVO邏輯語義公式成立的

10、條件3看到命題和持有命題(r,t) p sees X 當(dāng)且僅當(dāng)X屬于主體P在(r,t)時(shí)已看到消息集合。(r,t) p has X 當(dāng)且僅當(dāng)X屬于主體P在(r,t)時(shí)已收消息集合。SVO邏輯語義公式成立的條件43) 述說命題(r,t) p said X 當(dāng)且僅當(dāng)對(duì)于消息M在協(xié)議t時(shí)之前，主體P發(fā)送過消息M，且X是M的子消息。SVO邏輯語義公式成立的條件54)仲裁命題(r,t) p controls ， 當(dāng)且僅當(dāng)(r,t) p says 且對(duì)于所有的t0, 有：(r,t) 。SVO邏輯語義公式成立的條件65)新鮮性命題(r,t) fresh(X)當(dāng)且僅當(dāng)對(duì)于所有主體在本輪協(xié)議前沒有說過X。SVO

11、邏輯語義公式成立的條件7四種密鑰命題：共享密鑰公開加密密鑰公開簽名密鑰公開協(xié)商密鑰SVO邏輯語義公式成立的條件8共享密鑰？(r,t) R receivedXK 或者RP,Q。SVO邏輯語義公式成立的條件9公開加密密鑰(r,t) PK(P,K)當(dāng)且僅當(dāng)對(duì)于所有的t，若僅有(r,t) Q sees XK ，則Q=P。SVO邏輯語義公式成立的條件10公開簽名密鑰(r,t) PK(P,K)當(dāng)且僅當(dāng)對(duì)于所有的t，(r,t) Q received XK-1，則表明(r,t) P said X。SVO邏輯語義公式成立的條件11公開協(xié)商密鑰(r,t) PK(P,K)當(dāng)且僅當(dāng)對(duì)于所有的t：對(duì)于某些Q，Kpq=f

12、(K-1, PK(Q)且(r,t) goodkey(P,Kpq,Q)對(duì)于所有R，Kpr=f(K-1, PK(R)以及(r,t) goodkey(P,Kpr,R)且對(duì)于所有U，Kur=f(PK-1 (U), PK-1(R)且(r,t) goodkey(U,Kur,R)。SVO邏輯的應(yīng)用實(shí)例主體目標(biāo)相同：密鑰分配和認(rèn)證。則 不大可能會(huì)出現(xiàn)否認(rèn)性。 主體目標(biāo)不同：電子商務(wù)，為了利益需求，可能對(duì)已發(fā)生行為進(jìn)行否認(rèn)。收費(fèi)后否認(rèn)收費(fèi)或者因質(zhì)量問題而否認(rèn)發(fā)貨。解決：收集并持有一個(gè)聲稱事件或行為的不可否認(rèn)證據(jù)，并使之能有效地用于解決由于否認(rèn)事件或行為而引起的糾紛。SVO邏輯的應(yīng)用實(shí)例續(xù)1Schneider 在

13、下列文獻(xiàn) 中運(yùn)用通信順序進(jìn)程CSP對(duì)一個(gè) 不可否認(rèn)協(xié)議實(shí)例進(jìn)行了形式化的描述與分析。Schneider S., Verifying authentication protocols with CSP. Proceedings of the IEEE Computer Security Foundations Workshop X, IEEE Computer Society, 3-17 1997。用SVO也可對(duì)不可否認(rèn)性進(jìn)行分析。SVO邏輯-一個(gè)不可否認(rèn)協(xié)議實(shí)例不可否認(rèn)協(xié)議的實(shí)現(xiàn)：證據(jù)的生成證據(jù)的交換證據(jù)的驗(yàn)證糾紛的解決一是雙方進(jìn)行同時(shí)的秘密交換(麻煩，要求協(xié)議雙方具有同等計(jì)算能力不現(xiàn)實(shí))。二

14、是借助一個(gè)可信第三方(TTP)。SVO邏輯-不可否認(rèn)協(xié)議實(shí)例續(xù)兩個(gè)基本證據(jù)：NRO(Non-repudiation of Origin):發(fā)方不可否認(rèn)。NRR(Non-repudiation of Receipt):收方不可否認(rèn)。NRS:(Non-repudiation of Submission):提交不可否認(rèn),證明已提交給了TTP，由提交方提供。NRD:(Non-repudiation of Delivery):傳遞不可否認(rèn),證明TTP已交付給了意定接收者，由TTP提供。SVO邏輯-不可否認(rèn)協(xié)議實(shí)例續(xù)【Zhou和Gollman提出】ZG協(xié)議AB:fNRO, B,L,C, NROBA:fNR

15、R, A,L,C, NRRATTP: fNRS, B,L,K, NRS_KBTTP: fNRD, A,B,L,K, NRD_KATTP: fNRD, A,B,L,K, NRD_KSVO邏輯-不可否認(rèn)協(xié)議實(shí)例續(xù):ftp 操作符。NRO= SA(fNRO,B,L,C)NRR= SB(fNRR,A,L,C)NRS_K= SA(fNRS,B,L,K)NRD_K= STTP(fNRD,A,B,L,K)SVO邏輯-不可否認(rèn)協(xié)議實(shí)例分析定義3.1 不可否認(rèn)協(xié)議的公平性： 是指從協(xié)議執(zhí)行的開始到協(xié)議執(zhí)行結(jié)束的任何一個(gè)階段，通信的雙方要么能夠同時(shí)得到它們所期望的，要么任何一方都得不到有利于自己的信息，從而避免協(xié)

16、議的任一方中斷執(zhí)行的協(xié)議，或否認(rèn)其已發(fā)生的行為以達(dá)成利益不平等的可能。SVO邏輯-不可否認(rèn)協(xié)議實(shí)例分析定理3.1 一個(gè)不可否認(rèn)協(xié)議的不可否認(rèn)性是成立的，如果：協(xié)議任何一方執(zhí)行后的中止將不會(huì)破壞 通信雙方主體的地位的公平性。在協(xié)議結(jié)束時(shí)提供主體參與協(xié)議行為的證據(jù)，即證據(jù)的有效性。SVO邏輯-不可否認(rèn)協(xié)議ZG證明給出協(xié)議的前提或假設(shè)說明協(xié)議目標(biāo)運(yùn)用規(guī)則和公理進(jìn)行推證SVO邏輯-ZG證明假設(shè)給出協(xié)議的前提或假設(shè)A0:協(xié)議的運(yùn)行環(huán)境是不安全的(基本假設(shè))。A1:每個(gè)主體的公鑰是公開的。A2:每個(gè)主體的私鑰僅為其所知。A3:TTP believes SAA4:TTP believes SBA5:P be

17、lieves STTP:P 為參與協(xié)議運(yùn)行的主體A6:TTP believes (B received C)TTP believes (A said C)SVO邏輯-ZG證明假設(shè)續(xù)A7: A said (A,B,L,Ek(M) A said (A,B,L,K) A said MA8: B received (A,B,L,Ek(M) B received(A,B,L,K) B received MA9:TTP believes (A said C B received C TTP received K) TTP says K表示TTP只有在確信A已說過C，并且B已收到了C，以及TTP收到了K，才

18、將K公布到其公開目錄中。A10：TTP says XP ftp X P sees XTTP將其認(rèn)為是有效的數(shù)據(jù)放入到其公共目錄下，并可為任何主體通過ftp操作訪問。SVO邏輯-ZG證明假設(shè)續(xù)A11:P believes PK(Q,K) P received XK-1 P believes (Q said X)表示如果P收到一個(gè)簽名消息，并且P相信這個(gè)簽名密鑰是Q的，那么P相信Q說過X。A12:A beliveves fresh(Na)A13:TTP believes SVO邏輯-ZG證明協(xié)議目標(biāo)一般目標(biāo)：G1A believes (B received M)G2B believes (A sa

19、id M)仲裁目標(biāo)G3J believes (A said M)G4J believes (B received M)SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證由 消息1),得：F1:B received SA(fNRO,B,L,C)由F1,A2,P4,A11,得：(P4: PK(A,K) B received XK-1 A said X)(A11: B believes PK(A,K) B received XK-1) B believes (A said X)得F2: B believes (A said (fNRO,B,L,C)SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)由F2,P5(是

20、哪一個(gè)？)得：F3:B believes (A said C)同理，對(duì)原協(xié)議消息 2)的分析只能得到A believes (B said C)，但無法 得到A believes (B received C),原協(xié)議修改為1)AB:fNRO,B,L,C,SA(fNRO,B,L,Na,C)2)BA:fNRR,A,L,C,SA(fNR,A,L,Na+1,C)SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)對(duì)修改后的協(xié)議進(jìn)行分析得：F4:A receives SB(FNRR,A,L,Na+1,C)由F4,A2,P4,A11,A12,得：F5: A believes (B received (fNRO, B

21、,L,Na,C) A believes (B received C)由消息 3)得：F6: TTP received SA(FNRS, B,L,K)SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)由F6, A2,A3得：F7:TTP believes (A said (fNRS,B,L,K) TTP received K 根據(jù)假設(shè)A9，TTP只有確信A已說過C，并且B收到C，以及TTP收到了K，才將K公布到其公開目錄中，但在原有協(xié)議中，TTP并不能確知B是否已收到了C，因此，A可對(duì)NRR進(jìn)行簽名，并將結(jié)果發(fā)給TTP。對(duì)消息 3)修改如下：SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)3)ATTP:

22、fNRS, B,L,K,NRS_K, SA(NRR)TTP收到消息3)后由P5得：F8:TTP received SA(NRR)由F8,A3,A11,P1,得：F9:TTP believed (A said C B received C)由F8,F9,A9,A6,得：F10:TTP says KSVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)由F10,A10，消息4)得：F11: B received (fNRD, A,B,L,K,STTP(fNRO, A,B,L,K)由F11,P5,A13,得：F12:(B received K B received C) B received M由F12,P6

23、, A7,消息5)得：F13:A received (fNRD,A,B,L,K, STTP(fNRO, A,B,L,K)由F10,F12,F13,A5,A11,P5,P7,P10,得：SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)F14:A believes (TTP says K) A believes(B sees K) A believes (B received M)G1由F7,F11,A5,得：F15:B believes(TTP says K) B believes (A said K)由F3,F15,得：F16: B believes (A said M)-G2SVO邏輯-ZG證明運(yùn)用規(guī)則和公理進(jìn)行推證續(xù)協(xié)議可能出現(xiàn)的糾紛及解決Case 1 A 否認(rèn)向B發(fā)送了消息M。在這種情況下B可將M,C,K,L以及NRO,NRD_K提交給仲裁，仲裁通過以下幾步可證明A發(fā)送了消息M。檢查NRD_K是用T的私鑰對(duì)消息(fNRD,A,B