密码协议安全性(形式化)分析

 

密码协议又称为安全协议。它是以协议的方式，针对当今计算机通信网络和分布式系统的背景，为保护网络通信的信息安全，以现代密码理论和技术为手段，在计算机网络通信中的综合应用。简单地说，密码协议就是使用密码技术来保障信息安全的通信协议。

密码协议安全性的含义是，如果一个密码协议使得非法用户不可能从协议中获得比协议自身所体现的更多的有用信息，则称该协议是安全的。

研究密码协议是否能达到其预定的安全目标称作协议的安全性分析。

密码协议安全性分析的步骤：

              1. 确定协议的安全目标。只有正确地刻划了安全目标，才能对安全性进行分析。反过来说，如果不能恰如其分地刻划出协议的安全目标，则对协议安全性的分析也很难得到正确的结果。另外，只有给出了明确的安全目标，才能进一步定义协议的安全性。

              2. 确定协议安全性的衡量标准。我们说一个协议是安全的或者是不安全的，必须有一个明确的判别条件，也就是要给出安全性的确切定义。

              3. 设定协议分析的出发点或基本前提。任何一种安全性都是一定基础上的安全性，因而基本前提对协议的安全性分析结果有着重要影响。比如说，我们通常所定义的协议安全性都是指“所使用的密码体制是安全的”这一基础上的协议安全性，因为密码协议离不开密码体制，从而协议的安全性也与密码体制的安全性密切相关。一个协议设计得再好，如果所使用的密码体制是不安全的，则该协议不可能是安全的。

4. 使用某种或某几种分析方法对某个具体的密码协议的安全性进行分析。迄今为止，还没有一种可靠的、切实可行的方法可以证明一个密码协议是真正安全的。但已有一些方法可以发现协议的安全漏洞，从而证明该协议是不安全的。

              密码协议安全性的基本分析方法：

              1、根据已有的成功经验和已知攻击手段，对目标协议进行穷举攻击，可称为穷举法或手工分析法；

              2、使用谓词逻辑、模态逻辑等对协议安全性形式化并进行逻辑推理，试图从逻辑上证明协议是安全的或不安全的，称为逻辑化方法；

              3、从计算的观点，将协议的安全性归约到一个数学难题，从而证明协议的安全性等价与一个公认的计算难题，称为可证安全性方法；

              4、使用规范语言和验证工具建立协议模型，用运行程序的方法来验证协议的安全性。

除了第一种方法外，其他分析方法都需要对密码协议的性质和目标进行形式化。目前，密码协议的形式化和形式化分析是研究热点。

但是，所有方法都存在局限性，没有一种万能的、通用的、切实可行的有效方法来分析密码协议的安全性。

大部分已经发表的论文不过说明自己的一套方法是可行的，可以发现已知的漏洞；或者可以证明公认的协议是安全的。但真正有用的是：设计一套方法，可以发现未知的漏洞；或者证明公认的某个安全协议是不安全的！！