《安全协议分析与设计 普通高等教育十一五 国家级规划教材 教学课件 ppt 作者 卫剑钒 陈钟 安全协议-第3章-下》由会员分享，可在线阅读，更多相关《安全协议分析与设计 普通高等教育十一五 国家级规划教材 教学课件 ppt 作者 卫剑钒 陈钟 安全协议-第3章-下（30页珍藏版）》请在金锄头文库上搜索。
1、安全协议分析与设计 第三章（下）,卫剑钒,2,SVO逻辑,针对BAN 逻辑的缺陷和不足，Paul Syverson和Paul C. van Oorschot在1994年提出了SVO逻辑SVO94，1996年他们对SVO逻辑做了适当的修改后给出了一个新的版本SVO96，它的出现标志着BAN 及BAN 类逻辑的成熟。 SVO 具有十分简洁的推理规则和公理，并且具有很好的扩展能力，受到了普遍的重视和广泛的应用。,3,SVO的主要优点,与其他逻辑分析方法相比，SVO的主要优点如下。 SVO建立了一个清晰明确的语义基础，并且以此来保证在此语义基础之上的逻辑推理是可靠的，这恰恰是SVO逻辑系统合理性的理论
2、依据。 SVO具有一个更为详细的模型，很好地消除了由于逻辑表达式意义引起的模糊理解问题，可以更准确地理解协议消息的真实含义。 SVO逻辑仍然保持了BAN逻辑简洁易用的特点，而且由于SVO逻辑语义的支持，对SVO逻辑的扩展变得十分方便。,4,SVO逻辑的认证目标,G1存活确认（Far-End Operative）：该目标是让A相信B最近发送过消息，也即认为B最近是存活的。 G2身份认证（Entity Authentication）：该目标是让A相信B最近发送了消息X，且它是对A的挑战的响应。 G3安全密钥建立 (Secure Key Establishment) ：该目标是让A相信他拥有的一个用
3、于和B通信的良好的Key。 G4密钥确认 (Key Confirmation) ：除了G3外，该目标还让A相信B也知道这个Key。 G5密钥新鲜性 (Key Freshness)：该目标让A相信某个Key是新鲜的。 G6相互确认密钥（Mutual Understanding of Shared Key）：该目标让A相信B最近确认了B拥有了一个用于和A通信的良好的Key。,5,SVO逻辑的语法,SVO定义了两个语言，一个是消息语言，另一个是公式语言。 首先定义T为原子项（Primitive Term）集合，其中包括互不相交的符号集合：主体、共享密钥、公钥、私钥、数字常量等。原子项也无法判断真假，
4、在原子项集合的基础上，定义消息语言和公式语言。,6,消息语言,消息语言MT是建立在T之上的满足下列性质的最小语言集合。 （1）如果XT，则X是消息。 （2）如果X1, X2, Xn是消息，F是任意一个n元变量函数，则 F（X1, X2, Xn）是消息。F可以是连接函数、加密函数或者签名函数等，即如果X1, X2, Xn是消息，则(X1 , Xn)、XK、XK等都是消息。在SVO逻辑中，XK表示签名。 （3）如果是公式，则是消息。,7,公式语言,公式语言FT是满足下列性质的最小公式集合。 （1）如果P和Q是主体，K是一个密钥，则SharedKey(K, P,Q)，PK(P,K)和 PK(P,K)
5、，PK(P,K)是公式。它们分别表示“K是P与Q的良好共享密钥”、“K是P的加密公钥”、“K是P的签名验证公钥”和“K是P的协商公钥”，并且公钥所对应的私钥是良好的。 （2）如果X和Y是消息，K是密钥，则SV(X,K,Y)是公式。SV(X,K,Y)表示签名验证。 （3）如果P是主体，X是消息，则P sees X，P says X，P said X，P received X和 fresh（X）是公式。 （4）如果和是公式，则和是公式。和分别代表“非”和“与”。 （5）如果是公式，则P believes 和 P controls 是公式，其中P是主体。,8,和BAN在标记法上的一些不同,SVO使用
6、了BAN逻辑的一些标记方法，但有一些扩展和不同： （1）P says X：与“P said X”不同的是，它的意思是本次会话开始后P发送了X，而不是指以前会话发送了X。 （2）P sees X：等价于“P has X”，意思是“P拥有消息X”，这可能是4种情况引起的：原本X就由P所有，X被P收到，P生成了X，以及前面3种情况的组合。 （3）XK：用密钥K对消息X加密后得到的消息，于BAN不同的是，SVO并不假设主体可以识别自己发出的消息，但是仍然假定唯有拥有正确密钥的主体能够解密这条加密的消息。 （4）XK：用私钥K对消息X签名后得到的消息，并认为收到XK，就自动获得了X。 （5）*：SVO使
7、用*表示主体所收到的，但不可识别的消息。,9,SVO的规则,SVO有两个初始规则。 （1）分离规则MP(Modus Ponens)： （2）必要性规则Nec(Necessitation)： P believes 表示“与”，表示“蕴含”，表示是一个定理，表示推理，也即“若则”关系。 规则1表明，可将公式和蕴含替换成公式。 规则2表明，如果是一个定理，则P believes 也是一个定理。,10,SVO公理,SVO公理有20条，其中有些是普通的公理，有些则是公理模板（axiom schemata）,即含有一些公式变量的公理。 对于任意的主体P及Q、任意和公式及，有下面这些公理。,11,相信公理（
8、Believing）,12,源关联公理（Source Association）,在Ax3中，XQ指消息X来自Q，Q sees K可以理解为Q has K。 Ax4中，PK(Q,K)表示K是Q的签名验证公钥，SV(X,K,Y)表示使用K可以验证X是否为消息Y的签名，如果收到X，且签名验证通过，则可推理出Q说过Y。,13,密钥协商公理（Key agreement）,Ax5中PK(P, Kp)表示Kp是P的协商公钥，还隐含表达了对应私钥的秘密性。F0(Kp, Kq)表示协商密钥生成函数（如DH算法），F0使用第1个参数所表示的公钥，使用第2个参数所对应的私钥。 Ax6中，为逻辑恒等，F1/F2符号表
9、示在公式中替换F1为F2，该公理表达了密钥协商的对称性。,14,接收公理（Receiving）,以上公理表明，主体接收到一个消息，也同时接收了该消息中的连接项；如果主体拥有解密密钥，可以获得被加密前的消息；主体能够从签名中得到被签名的消息。,15,看见公理（Seeing）,Ax10表明一个主体能看见所有它接收到的。Ax11表明主体可以看见连接消息项中的一部分。 Ax12中的F是主体P可计算的函数（如加密函数、解密函数及散列函数等等），这样，P sees XK P sees K1 P sees X 只是Ax12的一个特例，而不再作为一个单独的公理出现。 看见（see）和接收（receive）是不
10、一样的，凡是主体接收的，它一定看见，另外，主体还看见（可理解为生成或拥有）它自己生成的公式。,16,理解公理（Comprehending）,其中F是函数，且F或F1是P可以计算的。 理解公理指的是主体可以运用F或F1，对F(X)进行检验，如X为P产生的Nonce, F为对X的加密或者Hash，P可以对XK解密或者对X进行Hash，并检验是否为X或是否为H(X)。若检验成功，则P相信P拥有F(X)，这意味着P能识别它。 对于不能识别的项，SVO记之为“*”。注意，Ax13的反向形式，即P believes ( P sees X )P believes ( P sees F(X) )是一个定理，可
11、由Ax1和Ax12推导得出。,17,说过公理（Saying）,18,仲裁公理（Jurisdiction）,Ax16. P controls P says Ax16表明P对有仲裁权。,19,新鲜性公理（Freshness）,在Ax18中，F的计算必须依赖(X1,Xn)中新鲜元素的值。 例如：在X1、X2、X3中，只有X2是新鲜的，根据Ax17，则级联（X1,X2,X3）是新鲜的，但F(X1,X2,X3) = ( X1+(0 *X2) +X3 )不是新鲜的，因为F的计算并不依赖于X2的值。,20,Nonce验证公理（Nonce-Verification）,Ax19. fresh (X) P sai
12、d X P says X 如果X是新鲜的，且主体说过X，就意味着主体最近说过，也即在当前时期内（current epoch）说过。,21,共享密钥对称公理（Symmetric goodness of shared keys）,Ax20. SharedKey( K, P, Q ) SharedKey ( K, Q, P ) Ax20表明共享密钥具有对称性。,22,SVO目标的形式化,G1存活确认A believes B says X G2身份认证A believes B says F( X, Na ) G3安全密钥建立A believes SharedKey( K-, A, B ) G4 密钥确
13、认A believes SharedKey( K+, A, B ) G5 密钥新鲜性 A believes fresh( K ) G6 相互确认密钥 A believe B says SharedKey( K, B, A ),23,用SVO逻辑分析安全协议,以NSSK协议为例：,24,协议的初始假设,25,主体接收到消息的假设,26,对收到消息进行可理解性分析,27,主体对消息的解释,28,用SVO的推理规则和公理进行推导,29,用SVO的推理规则和公理进行推导,对B来说，B由（9）和（10）可以推导出S曾经说过Kab是良好的和新鲜的，但不能继续推导得出S是否在本次运行中说过。,30,Wei Jianfan,Thank You !,
