導航：安全管理網>> 培訓課件>> 綜合知識>>正文

安全協議理論與方法

			點擊數：
下載地址：點擊這里	文件大小： 277.00 KB 共60頁	文檔格式： PPT	下載點數： 13 點（VIP免費）

全屏查看

部分內容預覽 [文件共60頁]

本文件共60頁，只能預覽部分內容，查看全部內容需要下載。

注：預覽效果可能會出現部分文字亂碼（如口口口）、內容顯示不全等問題，下載是正常的。

	文件大小：277.00 KB 共60頁文件格式：PPT 下載點數：13 點（VIP會員免費）

下一篇：安全基本理論

上一篇：防汛安全培訓

文本預覽

僅提取頁面文字內容，供快速閱讀使用。

安全協議理論與方法
基于推理結構性方法
SVO邏輯
Syverson和Oracho提出，建立了用于推證合理性的理論模型。
提供獨立明確的語義基礎。
相當詳細的模型。消除理解模糊，有助于準確理解消息的真實含義和協議理想化。
通用語義，擴展性好，簡潔。
SVO邏輯的基本結構

術語集合。
 推理規則及公理。
 基于的假設。
SVO術語集合
定義T為初始術語集合, 包括互不相交的常量符號集合：主體、共享密鑰、公鑰、私鑰以及序列號等。
 n維函數表示有n個變量的函數，如加、解密函數等。
 消息語言MT：滿足下列性質的最小語言集合。
	1)	如果X?T，則X是消息。
	2)	如果X1,…,Xn是消息，F是任意一個n維函數,則F(X1,…,Xn)是消息。
	3)	如果?是公式，則?是消息。
SVO術語集合續
4. 公式語言FT：滿足下列性質的最小公式集合。
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邏輯的推理規則及公理
1. SVO邏輯遵從兩條基本推理規則

??(???) ╞ ?

╞ ? ? P believes  ?
SVO邏輯的推理規則及公理續1
SVO邏輯共有20條公理
I1 相信公理
對于任一主體P和公式?，?有：

P believes  ? ? P believes(???) ? P believes ?
P believes  ? ? P believes ( P believes ?)

SVO邏輯的推理規則及公理續2
(2) I2源關聯公理
密鑰用于推斷消息發送者的身份。
shared(P,K,Q)?R  received {XQ}K?Q said X
(PKó(Q,K))?R  received {X}K-1 ?Q said X
PKó(Q,K)表示K是主體Q的數字簽名驗證密鑰。它表明如果主體Q收到一個簽名的消息，并且Q知道簽名的驗證密鑰是K，就可以確定發送者身份。
SVO邏輯的推理規則及公理續3
I3 密鑰協商公理

(PK(P, KP) ? PK(P, Kq))  ? shared(P,KPq,Q))

Kpq= f(Kp, Kq-1) = f(Kp-1, Kq) f為密鑰協商函數，比如Diffie-Hellman密鑰交換。
SVO邏輯的推理規則及公理續4
I4 接收公理
主體對接收到的一個級聯的加密消息可用有效的密鑰解密。
P received(X1, …, Xn) ? P received Xi
P received {X}K ? P has K-1 ? P received X

SVO邏輯的推理規則及公理續5

I5 看到公理
P received X ? P sees X
P sees (X1,…,Xn)? P sees Xi
P sees X1?…?P sees Xn ? P sees (F(X1,…,Xn))
主體只要接收到一個消息就看到了這個消息，
并且看到了這個消息的每一部分。
SVO邏輯的推理規則及公理續6
I6理解公理
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))
如果一個主體理解一個消息，并看到此消息
的一個函數，那么它理解它所看到的。
F可視為加密函數，K為參數。
SVO邏輯的推理規則及公理續7
I7敘述公理
一個主體說過一個級聯消息，那么它一定說
過且看到消息的每一部分。
P said(X1,…,Xn) ? P said Xi ? P sees Xi
P says (X1,…,Xn) ? P said (X1,…,Xn) ? P says Xi

SVO邏輯的推理規則及公理續8

仲裁公理

P controls  ? ? P says ? ??
SVO邏輯的推理規則及公理續9
I9新鮮公理

如果消息的一部分是新鮮的，那么整個消息
也是新鮮的。
fresh(Xi) ?fresh(X1,…,Xn)
fresh(X1,…,Xn)?fresh(F(X1,…,Xn))
fresh(X)? P said X ? P says X
SVO邏輯的推理規則及公理續10
I10 共享密鑰的良好對稱性公理
如果K是P，Q之間的良好密鑰當且僅當K是Q，P之間的良好密鑰。

shared(P,K,Q) ?shard(Q,K,P)
SVO邏輯的推理規則及公理續11
(11) I11所有公理

P  has K ?  P  sees K
SVO邏輯語義—計算模型

Pe：代表環境,可用于模擬攻擊者的任意行為 。
Si:	每個主體Pi有一個局部狀態Si。
全局狀態: n+1維局部狀態。
主體行為:發送send(X,P)、receive()和generate(X)，但只能生成集合T0中的元素
SVO邏輯語義—計算模型續1
每一個行為導致狀態的一次遷移。
r: 一輪協議r是一個由整數時間索引的全局變量的有限集合。
r(t)：協議中的t時記為r(t)。
ri(t):	對應的主體Pi的局部變量記為ri(t)。
環境狀態：全局歷史、環境有效遷移集合和用于保存發給主體P而P還未收到的消息的消息緩沖區。
SVO邏輯語義—計算模型續2
主體Pi在(r,t)收到的消息集合包括：
局部消息歷史中或t之前出現的received(X)中的X。
收到的消息的級聯。
P持有所收到的加密消息{X}K的解密密鑰，則P可得到X。
SVO邏輯語義—計算模型續3
主體Pi在協議運行當中某處可看到的消息集合包含：
主體已收到的消息集。
主體新近生成消息集。
主體初始所知的消息集。
主體通過規則和公理從已知的消息集衍生的消息集。
對于主體說過的消息集的定義比此嚴格。
SVO邏輯語義—計算模型續4
主體Pi在(r,t)發送的消息集合包括：
主體對已發送過消息的級聯。
加密密鑰為主體所持有的加密消息的非加密部分，且此部分為主體所看到。
簽名密鑰為主體所持有的簽名消息的非簽名部分，且此部分為主體所看到。
Hash消息中的非Hash部分，且此部分為主體所看到。

SVO邏輯語義—公式成立的條件

定義：?將每一個常量命題p?T映射為點集?(p),
		  即命題p為真的點。
公式?在點(r,t)為真記為： (r,t) ╞ ?。

╞ ?  意味著 ?全真。
SVO邏輯語義—公式成立的條件1
邏輯連接及其原始命題
基本邏輯關系：

(r,t) ╞ p  iff(r,t) ??(p)。
(r,t) ╞ ??? iff(r,t) ╞ ? ?(r,t)╞ ?。
(r,t) ╞ ?? iff? 在(r,t)時不成立。
SVO邏輯語義—公式成立的條件2
原始命題
接收命題
(r,t) ╞ p received X

當且僅當X屬于主體P在(r,t)時已收消息集合。

SVO邏輯語義—公式成立的條件3
看到命題和持有命題

(r,t) ╞ p sees X  當且僅當X屬于主體P在(r,t)時已看到消息集合。
(r,t) ╞ p has  X  當且僅當X屬于主體P在(r,t)時已收消息集合。

SVO邏輯語義—公式成立的條件4
3) 述說命題

(r,t)╞ p said X 當且僅當對于消息M在協議t時之前，主體P發送過消息M，且X是M的子消息。
SVO邏輯語義—公式成立的條件5
4)仲裁命題

(r,t)╞ p controls  ?， 當且僅當(r,t)╞ p says  ?且對于所有的t’>0, 有：
(r,t) ╞ ?。

SVO邏輯語義—公式成立的條件6
5)新鮮性命題

(r,t)╞ fresh(X)當且僅當對于所有主體在本輪協議前沒有說過X。
SVO邏輯語義—公式成立的條件7
四種密鑰命題：
共享密鑰
公開加密密鑰
公開簽名密鑰
公開協商密鑰
SVO邏輯語義—公式成立的條件8
共享密鑰？？

(r,t’) ╞ R  received{X}K 或者R?{P,Q}。
SVO邏輯語義—公式成立的條件9
公開加密密鑰

(r,t) ╞ PK?(P,K)當且僅當對于所有的t’，若僅有(r,t) ╞ Q  sees {X}K ，則Q=P。

SVO邏輯語義—公式成立的條件10
公開簽名密鑰

(r,t) ╞ PK?(P,K)當且僅當對于所有的t’，
(r,t) ╞ Q  received {X}K-1，則表明

(r,t) ╞  P  said  X。

SVO邏輯語義—公式成立的條件11
公開協商密鑰
(r,t) ╞ PKó(P,K)當且僅當對于所有的t’：
對于某些Q，Kpq=f(K-1, PKó(Q))且(r,t’) ╞goodkey(P,Kpq,Q)
對于所有R，Kpr=f(K-1, PKó(R))以及(r,t’) ╞?goodkey(P,Kpr,R)

且對于所有U，Kur=f(PKó-1 (U), PKó-1(R))且(r,t’) ╞?goodkey(U,Kur,R)。
SVO邏輯的應用實例
主體目標相同：密鑰分配和認證。則 不大可能會出現否認性。
 主體目標不同：電子商務，為了利益需求，可能對已發生行為進行否認。收費后否認收費或者因質量問題而否認發貨。
解決：收集并持有一個聲稱事件或行為的不可否認證據，并使之能有效地用于解決由于否認事件或行為而引起的糾紛。
SVO邏輯的應用實例續1
Schneider 在下列文獻 中運用通信順序進程CSP對一個 不可否認協議實例進行了形式化的描述與分析。
Schneider S., Verifying authentication protocols with CSP. Proceedings of the IEEE Computer Security Foundations Workshop X, IEEE Computer Society, 3-17 1997。
用SVO也可對不可否認性進行分析。
SVO邏輯-一個不可否認協議實例
不可否認協議的實現：
證據的生成
證據的交換
證據的驗證
糾紛的解決
一是雙方進行同時的秘密交換(麻煩，要求協議雙方具有同等計算能力不現實)。
二是借助一個可信第三方(TTP)。
SVO邏輯-不可否認協議實例續
兩個基本證據：
NRO(Non-repudiation of Origin):發方不可否認。
NRR(Non-repudiation of Receipt):收方不可否認。
NRS:(Non-repudiation of Submission):
提交不可否認,證明已提交給了TTP，由提交方提供。
NRD:(Non-repudiation of Delivery):
傳遞不可否認,證明TTP已交付給了意定接收者，由TTP提供。

SVO邏輯-不可否認協議實例續
【Zhou和Gollman提出】ZG協議
A?B:	fNRO, B,L,C, NRO
B?A:	fNRR, A,L,C, NRR
A?TTP: fNRS, B,L,K, NRS_K
B?TTP: fNRD, A,B,L,K, NRD_K
A?TTP: fNRD, A,B,L,K, NRD_K

SVO邏輯-不可否認協議實例續
?: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邏輯-不可否認協議實例分析
定義3.1  不可否認協議的公平性：
    是指從協議執行的開始到協議執行結束的任何一個階段，通信的雙方要么能夠同時得到它們所期望的，要么任何一方都得不到有利于自己的信息，從而避免協議的任一方中斷執行的協議，或否認其已發生的行為以達成利益不平等的可能。
SVO邏輯-不可否認協議實例分析
定理3.1  一個不可否認協議的不可否認性是成立的，如果：
協議任何一方執行后的中止將不會破壞 通信雙方主體的地位的公平性。
在協議結束時提供主體參與協議行為的證據，即證據的有效性。
SVO邏輯-不可否認協議ZG證明

給出協議的前提或假設
說明協議目標
運用規則和公理進行推證
SVO邏輯-ZG證明假設
給出協議的前提或假設
A0:	協議的運行環境是不安全的(基本假設)。
A1:	每個主體的公鑰是公開的。
A2:	每個主體的私鑰僅為其所知。
A3:	TTP believes SA
A4:	TTP believes SB
A5:	P believes STTP:P 為參與協議運行的主體
A6:	TTP believes (B received C)?TTP believes (A said C)

SVO邏輯-ZG證明假設續
A7: A said (A,B,L,Ek(M)) ? A said (A,B,L,K) ? A said M
A8: B received (A,B,L,Ek(M)) ? B received(A,B,L,K) ? B received M
A9:	TTP believes (A said C ? B received C ? TTP received K) ? TTP  says K
表示TTP只有在確信A已說過C，并且B已收到了C，以及TTP收到了K，才將K公布到其公開目錄中。
A10：TTP  says X?P ftp X? P sees X
	TTP將其認為是有效的數據放入到其公共目錄下，并可為任何主體通過ftp操作訪問。
SVO邏輯-ZG證明假設續
A11:	P  believes PKó(Q,K) ? P received {X}K-1? P believes (Q  said X)
表示如果P收到一個簽名消息，并且P相信這個簽名密鑰是Q的，那么P相信Q說過X。
A12:	A  beliveves fresh(Na)
A13:	TTP  believes ???

SVO邏輯-ZG證明協議目標
一般目標：
	G1	A  believes (B  received M)
	G2	B  believes (A said M)

仲裁目標
	G3	J  believes  (A  said M)
	G4	J  believes  (B  received M)
SVO邏輯-ZG證明運用規則和公理進行推證
由 消息1),得：
F1:		B received SA(fNRO,B,L,C)
由F1,A2,P4,A11,得：
(P4:   PKó(A,K) ? B received {X}K-1? A  said X)
(A11: B believes PKó(A,K) ? B received {X}K-1)? B believes (A said X))
得F2:   B  believes (A said (fNRO,B,L,C))
SVO邏輯-ZG證明運用規則和公理進行推證續
由F2,P5(是哪一個？)得：
F3:	B  believes (A  said C)
同理，對原協議消息 2)的分析只能得到
		A  believes (B  said C)，但無法 得到
		A  believes (B  received C),原協議修改為
1’)	A?B:fNRO,B,L,C,SA(fNRO,B,L,Na,C)
2’)	B?A:fNRR,A,L,C,SA(fNR,A,L,Na+1,C)

SVO邏輯-ZG證明運用規則和公理進行推證續
對修改后的協議進行分析得：
F4:		A  receives  SB(FNRR,A,L,Na+1,C)
由F4,A2,P4,A11,A12,得：
F5:    	A  believes (B  received (fNRO, B,L,Na,C)) ?
		A   believes (B  received C)
由消息 3)得：
F6:	  TTP  received SA(FNRS, B,L,K)	
SVO邏輯-ZG證明運用規則和公理進行推證續
由F6, A2,A3得：
F7:	TTP  believes (A said (fNRS,B,L,K)) ? TTP received K

根據假設A9，TTP只有確信A已說過C，并且B收到C，以及TTP收到了K，才將K公布到其公開目錄中，但在原有協議中，TTP并不能確知B是否已收到了C，因此，A可對NRR進行簽名，并將結果發給TTP。對消息 3)修改如下：
SVO邏輯-ZG證明運用規則和公理進行推證續
3’)	A?TTP: 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 K
SVO邏輯-ZG證明運用規則和公理進行推證續
由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, 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證明運用規則和公理進行推證續
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)--G2
SVO邏輯-ZG證明運用規則和公理進行推證續
協議可能出現的糾紛及解決
Case 1  	A 否認向B發送了消息M。在這種情況下B可將M,C,K,L以及NRO,NRD_K提交給仲裁，仲裁通過以下幾步可證明A發送了消息M。
檢查NRD_K是用T的私鑰對消息(fNRD,A,B,L,K)的簽名。
	J received STTP(fNRD, A,B,L,K)	? J believes (TTP says K)
						? J believes (A said K)

SVO邏輯-ZG證明運用規則和公理進行推證續
2)	檢查NRO是用A的私鑰對消息(fNRO,B,L,Na,C)的簽名。
J  received SA(fNRO, B,L,Na,C)? J believes (A said C)
如果檢查M=D(K,C),則：
	J  believes  (A said M)
得證G3。
SVO邏輯-ZG證明運用規則和公理進行推證續
Case  2  B否認收到了消息M。在這種情況下A將M,C,K,L以及NRR,NRD_K提交給仲裁，仲裁通過以下幾步可證明B接收到了消息M。

檢查NRD_K是用T的私鑰對消息(fNRD,A,B,L,K)的簽名。
	J received STTP(fNRD, A,B,L,K)	?J believes (TTP says K)
					   	?J believes(B received  K)

SVO邏輯-ZG證明運用規則和公理進行推證續

2)	檢查NRR是用B的私鑰對消息(fNRO,A,L,Na+1,C)的簽名。
J  received SB(fNRO, A,L,Na+1,C)? J believes (B received  C)
如果檢查M=D(K,C),則：
	J  believes  (B received  M)
得證G4。

SVO邏輯-ZG證明運用規則和公理進行推證續
修改后的協議為：
A?B:	fNRO, B,L,C, SA(fNRO,B,L,Na,C)
B?A:	fNRR, A,L,C, SB(fNRR,A,L,Na+1,C)
A?TTP: fNRS, B,L,K, NRS_K,SA(NRR)
B?TTP: fNRD, A,B,L,K, NRD_K
A?TTP: fNRD, A,B,L,K, NRD_K

網友評論 more

綜合知識最新內容

02-11