安全协议-第6章-上

安全协议分析与设计

第六章（上）卫剑钒安全协议的设计在设计安全协议时，如果稍有不慎，就可能使协议存在安全隐患。有鉴于此，Abadi和Needham提出了设计认证协议的若干原则[AN96]。值得注意的是，这些原则只是非形式化的设计指导，它们既不是认证协议安全的充分条件也不是必要条件[Syve96]。一些工作致力于将形式化方法结合到协议的设计中，典型的方法有：Heintze-Tygar

方法[HT94]，Gong和Syversion

的fail-stop协议[GS95]，Buttyan&Staamann的简单逻辑[BSW98]，Canetti和Krawczyk的CK方法[CK01]等等。一些方法则通过穷举来搜索所有可能的安全协议，然后进行分析验证以得到安全协议。最后一节探讨如何设计具有防范DoS攻击能力的安全协议。2安全协议设计的基本原则这些原则最初是由MartinAbadi和RogerNeedham提出来的[AN94，AN96]，RossAnderson和RogerNeedham在文献[AN95]中又专门针对公开密钥协议提出了一系列设计原则。这些设计原则既不能保证安全，同时也不是达到安全的必要条件，但它们的确能够有效地防止一些常见的攻击。3基本原则含义明确原则原则1每条消息都能清楚地表达它的意思，对消息的解释必须完全依赖于消息的内容。形象地说，每一条消息都能用一句明明白白的语句来替代。例如，服务器S发出一条消息：{P，S，A，B，Kab}KA。这条消息可以表述为“在接收到P以后，S向A发送一个A与B之间通信的密钥K­ab”，这句话中的所有内容都必须在协议中显式地表达出来，使得消息的接收者根据协议中的信息就可以清楚地知道这条消息的含义，而不需要从上下文中推导。因为如果某个信息需要从上下文中推导，那么攻击者就可能通过在上下文中加入欺诈的信息来扰乱协议的正常运行。4基本原则声明条件原则原则2对消息适用的条件要清楚地说明，以便协议的使用者能够根据这些条件判断是否采用该协议。例如，某人希望采用公钥加密体制为基础的安全协议，他就可以选用类似NSPK这样的协议而不是NSSK协议；同样地，如果他希望第三方产生密钥，就不会选取大嘴青蛙协议。此外，保密原则也是一个基本原则，即不以明文的形式传递任何私有密钥以及其他秘密信息，这一点通常是容易做到的。5命名原则命名原则原则3如果主体的身份是一个关键消息，那么消息中应该明确标示主体的名字。这可看做是原则1的一个特例，但由于不符合这条原则带来的问题太多，故而专门列作一条原则。值得注意的是，不包含主体的名字不一定带来问题，但作为谨慎的做法，最好还是带上主体的名字。6加密原则原则4明白为什么需要加密。滥用加密会导致运算成本提高和协议冗余，而且加密并不总是意味着安全，不恰当的加密有时还会导致错误。早期的Kerberos协议[MNSS87]基于NSSK协议，但使用时间戳替换了Nonce，简化如下：7Msg1是不需要加密的，Msg2需要加密，因为Msg2中包含了S分配给A和B的通信密钥Kab。使用Kas能够让A知道这是S发出的，有一定的签名意义。但Msg2中是否需要双重加密？这种做法是从NSSK中继承来的，但双层的加密并没有给机密性和认证性带来任何附加的好处，相反，它增加了运算量。也许有人说这样可以使B在收到Msg3后得知A一定收到了Msg2，但这种解释不太寻常，也未必是协议设计者的本意（后继的Kerberos版本中去掉了这个双重加密）。8原则5先签名后加密主体对一个加密了的消息进行签名是不可靠的，因为主体可能并不知道明文是什么；而如果先签名后加密，一方面表明主体认可该消息，另一方面还保证了机密性。不满足这个原则有时会导致协议的错误，如在X.509系列协议中的单消息协议。9图中Ta是时间戳，Na是随机数（但通常并不使用），Xa和Ya是用户数据，协议的目的是保证Xa和Ya的完整性，让B得知Xa和Ya的产生者为A，并保证数据Ya的机密性。这个协议的问题在于，B事实上并不能保证主体A知道Ya的内容，[AN96]认为协议存在类似对Denning-Sacco协议的攻击，一个主体C把Msg1中A的签名去掉，然后换成C自己的签名发送给B，B会认为C认可了Ya，而事实上C并不知道Ya的内容。10这个原则仅仅是一个指导性的原则，一些不满足这个原则的协议仍然是安全的，如下图所示的ISO/IEC11770-3密钥传送协议。11时间性原则原则6设计者应该清楚地知道在使用Nonce时所要保证的性质。以Otway-Rees协议为例：12时间性原则在这个协议中，M是协议运行的会话标识符，新的会话密钥Kab由可信第三方S产生，Na和Nb不仅起到了保证新鲜性的作用，还起到了绑定主体名的作用。但是协议略显冗余，文献[AN96]中建议将其简化，使其含义更为明确13时间性原则原则7通过计数器来保证新鲜性时，需要注意对其进行秘密性保护。如果Na是Nonce的话，协议是安全的，但若Na是计数器这种可预测的量，协议就不安全了。14时间性原则攻击者C可以产生Na的下一个取值Na+1，将其发给S，然后从S那里得到一个包含系统时钟的消息，当A使用Na+1来获取时间的时候，C就可以把这个保存的消息传给A，这样A的系统时间就不准确了。协议可以修改如下：15时间性原则原则8如果采用时间戳来保证新鲜性，那么系统中的时间差异应该远小于消息的有效生存时间。系统的时间同步机制应该是系统可信计算基的一部分。比如在Kerberos协议中，系统时间比较慢的主体经常会有很多问题，它经常会把一个已经过期的证书当做有效的证书使用；同样，一个走得过快的时钟有时候也会为攻击者提供机会，如主体A（时钟过快的主体）在时间点T0发送了一个时间戳为T（T0<T）的消息，那么攻击者C就可以在时间点T附近重放这个消息而不被察觉。16时间性原则原则9对Nonce或时间戳这种新鲜性数值的加密不意味着密钥的新鲜性。NSSK协议中，对B来说，当收到Msg5后，可以肯定Kab是刚刚被使用过的密钥，但是这并不能保证Kab的新鲜性，也即不能保证Kab是刚刚被产生出来的。17识别原则原则10通常情况下每种协议都有自己的消息格式，主体收到一条消息后，应该能从消息格式中判断出该消息是属于哪个协议，属于哪次运行，以及它是第几条消息。考察NSSK协议的Msg4和Msg5：Msg4 B→A:{Nb}KabMsg5 A→B:{Nb+1}Kab

Msg5中把Nb加上1，其目的是防止攻击者对Msg4的重放，事实上，只要能够表达这种意义的消息都被认为是可行的，区分这两条消息的方法有很多，比如写成如下的形式：Msg4 B→A:{NSSK，“Message4”，Nb}KabMsg5 A→B:{NSSK，“Message5”，Nb}Kab18信任原则原则11协议的设计者应该知道他所设计的协议是基于怎样的信任关系，为什么要基于这种信任，以及有没有把握保证这种信任的存在。比如在Kerberos协议中，服务器及其时间源应该被信任，如果服务器发出错误的时间戳，则整个系统的安全性都不能得到保证。再如大嘴青蛙协议，协议由A产生会话密钥Kab，这种信任关系是否能被接受？主体A是否能保证产生的密钥具有保密性、不可重复性和不可预测性？这需要协议设计者审慎地加以考虑。19安全协议的设计方法研究fail-stop协议CK模型20fail-stop协议Gong&Syverson在文献[GS95]中提出了fail-stop协议的概念，其含义为：当遭遇任何干扰协议正常执行的主动功击时，协议将立即停止。它可以使协议设计更加容易，并对协议分析方法的要求大为降低。[GS95]认为，一个分布式的系统可视为一些空间上分离的进程的集合，它们通过交换消息来进行通信；协议是对所交换的消息的格式与相应时间的一个说明；安全协议使用密码体制，如加密算法和解密算法，来保证消息的完整性、秘密性、消息源发点、消息目的地、消息顺序以及消息意义；消息是被一步一步（step）执行的。21fail-stop协议定义6.1

fail-stop协议：如果某个协议能够做到这一点，即若攻击者对协议中某条消息的发送进行了干扰（如伪造、篡改、重放、插入、截断等），则协议后继的消息不再发送，那么这个协议是fail-stop协议。为方便起见，有时也称fial-stop协议中某条消息是fial-stop的。定义6.1是非形式化的，这是为了能够更直观地对fail-stop概念进行描述22断言6.1主动攻击不会导致fail-stop协议在运行时秘密泄露。由于主动攻击可导致一个fail-stop协议的停止，因此一个主动攻击者并不能获得比被动攻击者更多的信息。23抵御被动攻击的分析一个fail-stop协议是否可以抵御被动攻击？证明分为3个阶段：阶段1验证协议的fail-stop性质，即判断该协议是否是一个fail-stop协议；阶段2验证秘密假设，分析一个被动攻击者是否可以得到协议中的秘密；阶段3在阶段2的基础上，应用BAN类逻辑分析协议。24阶段1．验证fail-stop性质阶段1．验证fail-stop性质验证一个协议是否为fail-stop协议，最直接的办法是验证协议与一个fail-stop协议规范是一致的。可能会有很多种fail-stop协议规范，这里先给出一种简单的fail-stop协议规范，这类协议使用对称密码体制。断言6.2如果满足下述条件，则一个协议是fail-stop的。（1）每个消息含有一个消息头，内含发送者标识、接收者标识、协议标识及协议版本号、消息序号以及一个新鲜性标识。（2）每个消息都是被加密的，加密密钥是发送者和接收者之间的共享密钥。（3）一个诚实主体按照协议运行，并忽略所有非预期的消息。（4）当一个期望的消息在规定的时间内没有到达，主体停止运行。25阶段2．秘密性假设的验证阶段2．秘密性假设的验证由于主动攻击将停止一个fail-stop协议，攻击者如果想尽可能多地收集消息，最好还是不加干扰地等协议运行完毕，也即最好做一个被动攻击者。验证一个协议执行是否会泄露秘密，只需确定被动攻击者能否通过处理消息而获得特定的数据项（简称项）。给定攻击者已拥有的项，有如下的拥有规则。（1）拥有一个项，则拥有项中的所有子项。（2）拥有一个项的所有子项，则拥有该项。（3）拥有一个项，则拥有该项的函数运算结果，前提是该函数对于攻击者是可计算的（如拥有x则拥有Hash(x)）。（4）拥有一个项和一个加密密钥，则拥有该项的加密形式，即一个加密项。（5）拥有一个加密项和对应的解密密钥，则拥有解密后的项。26阶段3．应用BAN类逻辑阶段3．应用BAN类逻辑BAN类逻辑在对协议进行分析时，需要一些前提假设，如要求一个主体能判断一个消息是不是自己发的，而满足断言6.2中定义的fail-stop协议能自动满足这个假设。此外，对于fail-stop协议，逻辑中关于新鲜性验证和可识别性验证（如GNY逻辑）的公理或规则都可以被简化或去掉。BAN类逻辑有一个共同的关键假设：所有秘密在协议执行中是保密的。因此，需要用阶段2来验证秘密性假设。27有些协议在前部分传送一个会话密钥，后部分用这个密钥来握手。协议的前两条消息是服务器S给A和B分发会话密钥k，后两个消息中，A和B使用该密钥进行握手。在这个协议中，后两条消息中使用的k是前两条消息中的内容，在不能判定k的安全性的情况下，无法认定整个协议是否是fail-stop的。可以先对第1条和第2条消息组成的部分进行分析，当这个部分通过3个阶段的验证后，就可以得知k是安全的，然后再对整个协议进行3个阶段的分析。28分析Nessett协议Nessett协议这个协议不是fail-stop的，因为一个攻击者窃听到Msg1后，可以把Msg1转发给诚实主体C，C得到这个消息后，不能判断这个消息是不是被转发来的还是确实是A发给自己的，而继续执行协议。为了使这个协议能够fail-stop，可以在Msg1中添加B的身份，使Msg1成为{B，Na,Kab}Ka−1，这样，协议就是fail-stop的了。一个隐含的假设是：没有其他协议的消息片段和修改后的Msg1有同样的形式，如果这个隐含假设不满足的话，可以在Msg1中添加协议标识和协议版本号来区分。29下面开始第2阶段的分析，这个阶段要对秘密保持的假设进行验证。协议中，Kab是一个需要保持秘密的量，对它的秘密性不作验证就无法分析Msg2。依据阶段2里提到的5条拥有规则，可以很容易得出：拥有{B，Na,Kab}Ka−1并且拥有Ka，则拥有{B，Na,Kab};拥有{B，Na,Kab}则拥有Kab。从推理可知，攻击者能够拥有Kab，修改Msg1后的Nesset协议不能通过阶段2的验证，协议无法继续后继的BAN类逻辑分析。30分析大嘴青蛙协议这个协议存在攻击，是S不能分辨重放的消息。主要的原因在于消息的区别能力，只要第2条消息能在格式上比第1条消息能有1比特的差异，这个协议就是fail-stop的。在将该协议修改为fail-stop协议后，可以对其进行第2阶段的分析，这是容易验证的，只要Kas和Kbs保持秘密，就可以保证协议的秘密不被泄露。BAN逻辑分析的结果表明修改后的该协议是安全的。31CK模型Canetti和Krawczyk在文献[BCK98]的基础上，采用复杂性理论对密钥交换协议做了安全特性的定义[CK01]，提出了一种模块化设计密钥交换协议的理论和方法，这里对其进行简要的介绍。CK模型将安全协议模型化为n个主体上运行的多个进程，每个主体可以同时运行协议的多个会话。攻击者控制整个通信并试图通过与协议的交互来获得秘密，并可以有如下的行为：激活（activate）主体运行协议；攻破（corrupt）主体；主体内部状态泄漏（reveal）；进行会话输出查询（query）。32AM/UM模型攻击者能力模型分为AM模型和UM模型，AM模型可被视为理想环境，在AM模型下攻击者只能通过传递另一个主体发送的消息来使主体激活；攻击者可以选择不传递消息，但一旦传递，就只能传送一次，并且忠实地传送到消息预定目的地；攻击者可以伪装网络地址，但不能篡改消息和重放消息。UM模型可被视为真实环境，UM下攻击者除了具备AM中的能力外，还可以主动激活主体与另外一个主体的会话，并可以任意篡改和重放消息。激活的含义是指使一个主体主动地发起协议运行，如对于NSPK协议，攻击者在需要的时候，可以使主体A发起对攻击者自己的协议运行。33SK安全定义6.2满足以下条件的认证协议被称为SK安全：（1）如果两个未被攻破的主体完成一次匹配的会话后，它们都接受相同的会话密钥。（