1.2 NSL协议
    NSL((Needham-Schroeder-Lowe)协议是由G. Lowe针对NSPK(Needham Schroeder Public Key)协议的改进方案。NSPK协议的安全目标是实现2个主体之间的相互认证，为了分配主体通信密钥协议引入了双方都信任的可信第三方服务器。假设A是发起者,B是响应者,S是认证服务器，用于为通信双方之间分配密钥。
    Ka表示A的公钥，Kb表示B的公钥，Na表示A产生的随机数，Nb表示B产生的随机数。为了简化分析，协议消息中去除了服务器分配双方公钥的内容。NSPK协议简化表现形式为:
    (1)A→B: {Na, A }Kb
    (2)B→A:{Na, Nb}Ka
    (3)A→B:{Nb}Kb
    1996年G. Lowe用CSP(通信顺序进程)方法和模型校验技术对NSPK协议进行形式化分析，指出由于消息2中没有B的标识符，攻击者可以假冒B的身份发送消息。即存在攻击者I冒充B向A重发消息{Na, Nb}Ka ，I可以冒充B通过认证。G. Lowe提出了NSPK的改进协议NSL协议，主要是在消息2中增加了B的标识，协议具体形式为：
    (1)A→B: {Na, A }Kb
    (2)B→A:{Na, Nb, B}Ka
    (3)A→B:{Nb}Kb
    由于在消息2中加入了B的标识符，即使I重发消息2，A可以轻易识别出B的标识发现I的真实身份。从NSL协议设计出来到现在，在协议安全分析中经常被用来作为一个设计正确的协议加以引用。
    1.3同态攻击
    同态用于表示两个代数结构（例如群、环、或者向量空间）之间的保持结构不变的映射。考虑两个有单一二元运算的集合X和Y，同态就是映射 使得： 
    例如，考虑带加法运算的自然数。保持加法不变的函数有如下性质：f(a + b) = f(a) + f(b)。如f(x) = 8x就是这样的一个同态，因为f(a + b) = 8(a + b) = 8a + 8b = f(a) + f(b)。
    考虑ECB模式的同态结构，具有：
    C=Ek(m1m2m3…mn)= Ek(m1), Ek(m2), Ek(m3),…, Ek(mn)
    NSL协议是在基于Dolev-Yao模型的基础上设计的，当工作模式具备同态结构时可以利用这种特性进行攻击。下面引入攻击者I，具备Dolev-Yao模型攻击者所有能力，并且在A和B的通信中扮演中间人的角色。
    I发起和A与B的两个会话：
    (1)A→I: {Na, A }Ki
    (2)I(A)→B:{Na, A}Kb
    (3)B→I(A):{ Na,Nb, B }Ka
    (4)I→A: {Na, Nb, I }Ka
    (5)A→I:{Nb}Ki
    (6)I(A)→B:{Nb}Kb
    (1)、(4)、(5)属于A和I的会话回合，本回合I没有冒充其他对象，这里称为回合一。(2)、(3)、(6)属于I和B的会话回合，本回合I冒充了A，这里称为回合二。
    在(5)中攻击者I获得了Nb，接着在(6)中就可以冒充A向B发送验证信息的Nb值。上面攻击的重点在于获得B的随机数Nb。
    由于ECB的同态结构，消息(3) B→I(A):{ Na,Nb, B }Ka等同为：
    B→I(A):{ Na,Nb }Ka, { B }Ka
    同样的，消息(4) I→A:{ Na,Nb, I }Ka等同为：
    I→A:{ Na,Nb }Ka, { I }Ka
    这样，消息(4)可以用消息(3)分解的信息{ Na,Nb }Ka和{ I }Ka一起合成，接着在消息(5)中A会把Nb告诉I。
    2 NSL协议改进方法
   2.1 基于哈希函数的改进方法
    在安全协议中，由于高层协议抽象很少考虑同态、可交换性、无界性等的特性，可能导致协议被攻击。在ECB结构中，密文具有特性：
    C=Ek(m1m2m3…mn)= Ek(m1), Ek(m2), Ek(m3),…, Ek(mn)
     即m1m2m3…mn加密中没有任何关系，要破坏上面的等式，可以把C=Ek(m1m2m3…mn)改变为：
    C=Ek(m1 ,f(m1,m2) , f(m1,m2, m3)…f(m1m2m3…mn))
    这样对于mi来说，要加密的消息不仅和当前明文块有关系，还和以前的信息有关。尽管攻击者I可以得到：
    C=Ek(m1), Ek(f(m1,m2)),…Ek (f(m1m2m3…mn))
    使用哈希函数，攻击者无法提取出m2m3…mn的内容，保护了后续内容的秘密性。为了避免对NSL协议的攻击，本文提出了破坏同态结构的改进方法。改进后的协议为：
    (1)A→B: {Na, A }Kb
    (2)B→A:{Na, Nb, h(Nb, B)}Ka
    (3)A→B:{Nb}Kb
    改进后的协议增加了一个哈希函数h(Nb, B),把主体的ID和生成的随机数绑定在一起。攻击者I在并行会话攻击中，获得消息(2)后使用ECB的同态特性把消息分解重新为：
    B→I(A):{ Na,Nb }Ka, { h(Nb, B) }Ka
    接着，攻击者想生成新的消息：
    I→A:{ Na,Nb }Ka, {h(Nb, I)}Ka
     其中，攻击者I可以获得{ Na,Nb }Ka，但是无法生成{h(Nb, I)}Ka，因为此时I还不知道的Nb数值。
    3安全协议形式化验证
    3.1 增强的BAN逻辑分析
    BAN逻辑是一种基于信仰的安全协议形式化分析方法，是在Dolev-Yao模型基础上的高层协议抽象。它通过认证协议运行过程中消息的接收和发送最初的信仰，发展到协议运行要达到的目的主体的最终信仰。为了考虑密码算法的同态特性，增加了一条推理规则来扩充攻击者的攻击能力。
    BAN逻辑基本推理规则有：

    1. 消息含义规则

(责任编辑：)