安全协议设计与分析--第3章-下.ppt

*******************************安全协议分析与设计

第三章逻辑类分析方法（下）卫剑钒*SVO逻辑针对BAN逻辑的缺陷和不足，PaulSyverson和PaulC.vanOorschot在1994年提出了SVO逻辑[SVO94]，1996年他们对SVO逻辑做了适当的修改后给出了一个新的版本[SVO96]，它的出现标志着BAN及BAN类逻辑的成熟。SVO具有十分简洁的推理规则和公理，并且具有很好的扩展能力，受到了普遍的重视和广泛的应用。*SVO的主要优点与其他逻辑分析方法相比，SVO的主要优点如下。SVO建立了一个清晰明确的语义基础，并且以此来保证在此语义基础之上的逻辑推理是可靠的，这恰恰是SVO逻辑系统合理性的理论依据。SVO具有一个更为详细的模型，很好地消除了由于逻辑表达式意义引起的模糊理解问题，可以更准确地理解协议消息的真实含义。SVO逻辑仍然保持了BAN逻辑简洁易用的特点，而且由于SVO逻辑语义的支持，对SVO逻辑的扩展变得十分方便。*SVO逻辑的认证目标G1存活确认（Far-EndOperative）：该目标是让A相信B最近发送过消息，也即认为B最近是存活的。G2身份认证（EntityAuthentication）：该目标是让A相信B最近发送了消息X，且它是对A的挑战的响应。G3安全密钥建立(SecureKeyEstablishment)：该目标是让A相信他拥有的一个用于和B通信的良好的Key。G4密钥确认(KeyConfirmation)：除了G3外，该目标还让A相信B也知道这个Key。G5密钥新鲜性(KeyFreshness)：该目标让A相信某个Key是新鲜的。G6相互确认密钥（MutualUnderstandingofSharedKey）：该目标让A相信B最近确认了B拥有了一个用于和A通信的良好的Key。*SVO逻辑的语法SVO定义了两个语言，一个是消息语言，另一个是公式语言。首先定义T为原子项（PrimitiveTerm）集合，其中包括互不相交的符号集合：主体、共享密钥、公钥、私钥、数字常量等。原子项也无法判断真假，在原子项集合的基础上，定义消息语言和公式语言。*消息语言消息语言MT是建立在T之上的满足下列性质的最小语言集合。（1）如果X∈T，则X是消息。（2）如果X1,X2,…,Xn是消息，F是任意一个n元变量函数，则F（X1,X2,…,Xn）是消息。F可以是连接函数、加密函数或者签名函数等，即如果X1,X2,…,Xn是消息，则(X1,…,Xn)、{X}K、[X]K等都是消息。在SVO逻辑中，[X]K表示签名。（3）如果φ是公式，则φ是消息。*公式语言公式语言FT是满足下列性质的最小公式集合。（1）如果P和Q是主体，K是一个密钥，则SharedKey(K,P,Q)，PKψ(P,K)和PKσ(P,K)，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是消息，则PseesX，PsaysX，PsaidX，PreceivedX和fresh（X）是公式。（4）如果φ和ψ是公式，则?φ和φ∧ψ是公式。?和∧分别代表“非”和“与”。（5）如果φ是公式，则Pbelievesφ和Pcontrolsφ是公式，其中P是主体。*和BAN在标记法上的一些不同SVO使用了BAN逻辑的一些标记方法，但有一些扩展和不同：（1）PsaysX：与“PsaidX”不同的是，它的意思是本次会话开始后P发送了X，而不是指以前会话发送了X。（2）PseesX：等价于“PhasX”，意思是“P拥有消息X”，这可能是4种情况引起的：原本X就由P所有，X被P收到，P生成了X，以及前面3种情况的组合。（3）{X}K：用密钥K对消息X加密后得到的消息，于BAN不同的是，SVO并不假设主体可以识别自己发出的消息，但是仍然假定唯有拥有正确密钥的主体能够解密这条加密的消息。（4）[X]K：用私钥K对消息X签名后得到的消息，并认为收到[X]K，就自动获得了X。（5）*：SVO使用*表示主体所收到的，但不可识别的消息。*SVO的规则SVO有两个初始规则。（1）分离规则MP(ModusPonens)：φ∧φ?ψψ（2）必要性规