导航：安全管理网>> 培训课件>> 综合知识>>正文

安全协议理论与方法

		点击数：	更新时间： 2021年08月02日
下载地址：点击这里	文件大小： 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

综合知识最新内容

04-18