《{安全生产管理}安全协议理论与办法》由会员分享，可在线阅读，更多相关《{安全生产管理}安全协议理论与办法（59页珍藏版）》请在金锄头文库上搜索。
1、安全协议理论与方法,基于推理结构性方法,SVO逻辑,Syverson和Oracho提出，建立了用于推证合理性的理论模型。 提供独立明确的语义基础。 相当详细的模型。消除理解模糊，有助于准确理解消息的真实含义和协议理想化。 通用语义，扩展性好，简洁。,SVO逻辑的基本结构,术语集合。 推理规则及公理。 基于的假设。,SVO术语集合,定义T为初始术语集合, 包括互不相交的常量符号集合：主体、共享密钥、公钥、私钥以及序列号等。 n维函数表示有n个变量的函数，如加、解密函数等。 消息语言MT：满足下列性质的最小语言集合。 1)如果XT，则X是消息。 2)如果X1,Xn是消息，F是任意一个n维函数,则F
2、(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
3、逻辑的推理规则及公理续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 XQKQ said X (PK(Q,K)R received XK-1 Q said X PK(Q,K)表示K是主体Q的数字签名验证密钥。它表明如果主体Q收到一个签名的消息，并且Q知道签名的验证密钥是K，就可以确定发送者身份
4、。,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 XK P has K-1 P received X,SVO逻辑的推理规则及公理续5,I5 看到公理 P received X P sees X P se
5、es (X1,Xn) P sees Xi P sees X1P 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
6、叙述公理 一个主体说过一个级联消息，那么它一定说 过且看到消息的每一部分。 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
7、共享密钥的良好对称性公理 如果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是一个由整数时间索引的全局变量的有限
8、集合。 r(t)：协议中的t时记为r(t)。 ri(t):对应的主体Pi的局部变量记为ri(t)。 环境状态：全局历史、环境有效迁移集合和用于保存发给主体P而P还未收到的消息的消息缓冲区。,SVO逻辑语义计算模型续2,主体Pi在(r,t)收到的消息集合包括： 局部消息历史中或t之前出现的received(X)中的X。 收到的消息的级联。 P持有所收到的加密消息XK的解密密钥，则P可得到X。,SVO逻辑语义计算模型续3,主体Pi在协议运行当中某处可看到的消息集合包含： 主体已收到的消息集。 主体新近生成消息集。 主体初始所知的消息集。 主体通过规则和公理从已知的消息集衍生的消息集。 对于主体说过
9、的消息集的定义比此严格。,SVO逻辑语义计算模型续4,主体Pi在(r,t)发送的消息集合包括： 主体对已发送过消息的级联。 加密密钥为主体所持有的加密消息的非加密部分，且此部分为主体所看到。 签名密钥为主体所持有的签名消息的非签名部分，且此部分为主体所看到。 Hash消息中的非Hash部分，且此部分为主体所看到。,SVO逻辑语义公式成立的条件,定义：将每一个常量命题pT映射为点集(p), 即命题p为真的点。 公式在点(r,t)为真记为： (r,t) 。 意味着 全真。,SVO逻辑语义公式成立的条件1,逻辑连接及其原始命题 基本逻辑关系： (r,t) p iff(r,t) (p)。 (r,t)
10、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逻辑语义公式
11、成立的条件5,4)仲裁命题 (r,t) p controls ， 当且仅当(r,t) p says 且对于所有的t0, 有： (r,t) 。,SVO逻辑语义公式成立的条件6,5)新鲜性命题 (r,t) fresh(X)当且仅当对于所有主体在本轮协议前没有说过X。,SVO逻辑语义公式成立的条件7,四种密钥命题： 共享密钥 公开加密密钥 公开签名密钥 公开协商密钥,SVO逻辑语义公式成立的条件8,共享密钥？ (r,t) R receivedXK 或者RP,Q。,SVO逻辑语义公式成立的条件9,公开加密密钥 (r,t) PK(P,K)当且仅当对于所有的t，若仅有(r,t) Q sees XK ，则Q
12、=P。,SVO逻辑语义公式成立的条件10,公开签名密钥 (r,t) PK(P,K)当且仅当对于所有的t， (r,t) Q received XK-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逻辑的应用
13、实例,主体目标相同：密钥分配和认证。则 不大可能会出现否认性。 主体目标不同：电子商务，为了利益需求，可能对已发生行为进行否认。收费后否认收费或者因质量问题而否认发货。 解决：收集并持有一个声称事件或行为的不可否认证据，并使之能有效地用于解决由于否认事件或行为而引起的纠纷。,SVO逻辑的应用实例续1,Schneider 在下列文献 中运用通信顺序进程CSP对一个 不可否认协议实例进行了形式化的描述与分析。 Schneider S., Verifying authentication protocols with CSP. Proceedings of the IEEE Computer Sec
14、urity 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
15、-repudiation of Submission): 提交不可否认,证明已提交给了TTP，由提交方提供。 NRD:(Non-repudiation of Delivery): 传递不可否认,证明TTP已交付给了意定接收者，由TTP提供。,SVO逻辑-不可否认协议实例续,【Zhou和Gollman提出】ZG协议 AB:fNRO, B,L,C, NRO BA:fNRR, A,L,C, NRR ATTP: fNRS, B,L,K, NRS_K BTTP: fNRD, A,B,L,K, NRD_K ATTP: fNRD, A,B,L,K, NRD_K,SVO逻辑-不可否认协议实例续,:ftp 操作
16、符。 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:每个主体的私钥仅为其所知。
