1、形式化方法简介形式化方法简介 n形式化方法兴起于70年代末期，如今已广泛用于解决理论和实际问题，计算机安全是它一个比较成功的应用领域。n形式化分析技术是有局限性的，协议系统的运行不是独立的，而是处于某种环境之下。n安全协议的形式化分析方法是采用各种形式化的语言或者模型，为安全协议建立模型，并按照规定的假设和分析、验证方法证明协议的安全性 安全协议的形式化验证过程 非形式化的协议描述入侵者模型形式化规范说明发现漏洞分析工具安全协议的形式化验证过程 n为了对一个安全协议进行形式化的分析，首先要将协议的非形式化描述（例如RFC文档）转换为形式化的规范说明，然后结合协议的入侵者模型，将两者作为形式化分
2、析工具的输入，经过分析工具的处理，最后得到结论。n安全协议的形式化分析至少可以完成以下工作：（1）界定协议运行系统的边界；（2）更加准确描述系统的行为；（3）更准确地定义系统的特性；（4）证明系统在特定的假设前提下满足一定的特性。安全协议的形式化分析的历史安全协议的形式化分析的历史 n安全协议形式化分析的思想由Needham和Schroeder两人在1978年最先提出。n1981年，Denning和Sacco指出NS私钥协议的一个错误，人们开始关注安全协议的形式化分析。n20世纪80年代，Danny Dolev和Andrew C.Yao发表了文章“On the Security of Publ
3、ic Key Protocols”，它真正开始了使用形式化方法分析安全协议的历史，自此之后使用形式化的方法研究安全协议逐渐兴起。n安全协议的形式化分析技术领域的神秘感一直到1989年才被打破，Burrows，Abadi和Needham引入了逻辑的方法，提出了BAN逻辑的概念，并逐渐引起了人们广泛的关注。Dolev-Yao模型模型 n协议描述协议描述 在Dolev-Yao模型中，T的消息将被描述为：Ni(X,Y)M（i=1,2,t+t），其中，Ni(X,Y)表示协议主体对明文消息M所施加的加密、解密运算符号串连而成的一个序列。定义如下：N1(X,Y)=i(X,Y)，N2j(X,Y)=i(X,Y)
4、N2 j1(X,Y)，1 j tN2j+1(X,Y)=i+1(X,Y)N2i(X,Y)，1 i t 1其中，i(X,Y)与i(X,Y)分别表示协议发起者与响应者对接收到的消息所执行的加密、解密运算组成的一个序列。定义如下：i(X,Y)EX,EY,DX*i(X,Y)EX,EY,DX*其中，EX为加密运算符；DX为解密运算符。他们满足以下两个条件：EX DX=DX EX=1；已知EX(M)与主体X的公钥不会泄露有关M的任何信息。Dolev-Yao入侵入侵模型模型n我们假设入侵者为Z，并且定义他可以执行的操作序列为：(1(Z)2 3)*其中，E表示所有主体A的公钥EA组成的集合，并且有1(Z)=E
5、DZ，2=i(A,B)|对于所有A B与i 2，3=i(A,B)|对于所有A B与i 1。n对于某个Ni(X,Y)，如果存在某个，使得下式成立：其中，表示一个空序列。那么我们称协议T是不安全的；否则称T是安全的。(,)iN X YDolev-Yao实例实例 n简单级连协议ST为例 11(,)(,)ABNABM11(,)(,)ABABM()ABBEDEM()AEM(1)A向B发送消息：(A,EB(M),B)；(2)B向A发送消息：(B,EA(M),A)。n利用Dolev-Yao模型给出上述协议的形式化描述如下：(1)N1(A,B)M=(A,B)M=EB(M)，其中i(A,B)=EB(2)N2(A
6、,B)M=其中i(A,B)=EA DB Dolev-Yao实例实例那么入侵者Z将对协议ST展开如下攻击：(1)Z截获在步骤(1)中A向B发送的消息：(A,EB(M),B)；(2)Z将消息(1)中的发送者名称A改为Z，然后将改动后的消息发送给B：(Z,EB(M),B)；(3)B按照协议要求回复Z消息：(B,EZ(M),Z)；(4)Z收到来自B的消息：EZ(M)；(5)Z使用自己的私钥解密消息EZ(M)以获得明文消息：M。于是，在Dolev-Yao模型中就会检查到存在，使得1111(,)(,)(,)(,)ZZZBZZBBN A BDZ B N A BD E D N A BD E D E这也就验证了
7、ST是不安全的。安全协议的形式化分析的分类安全协议的形式化分析的分类 n定理证明方法定理证明方法 n模拟检测方法模拟检测方法n互模拟等价互模拟等价 定理证明方法定理证明方法 n定理证明方法简单说就是数学方法，这种方法考虑协议的所有行为，并且验证这些行为满足一集正确条件。n定理证明有以下特点：n（1）用一集代数或者逻辑公式定义系统的行为，构成系统的行为集；用一集公理和系统的行为集一起，作为推理的基础公式集。n（2）所期望的系统行为和性质，描述成为一组公式，称为定理。n（3）从基础公式出发，进行定理证明过程，以达到所期望的结果。定理证明方法定理证明方法 n定理证明由公理、假设以及推理规则组成。这个
8、系统通常有两个刻画，一个可靠性或者相容性；另一个完备性。n一般可以用这种方法证明协议的正确性，难以用于发现协议的缺陷。而且，基于定理证明的方法在自动化方面无法与模型检测方法比拟n定理证明的过程中有些部分是可以自动化的，这样的自动化证明系统称为定理证明器。定理证明器与模型检测系统不同，通常需要人的帮助。常见的定理证明器有：Isabelle，HOL，Paradox，ACL2，PVS等等。模拟检测方法模拟检测方法 n模型检测考虑的是协议的有限多种行为，检测他们满足一些正确条件。n模型检测有以下特点：n（1）关于协议操作行为的有限状态系统，被刻画为有限状态迁移系统。这个系统的状态通过与环境的交互，满足
9、一定条件就迁移到另一个状态。这些条件被标记到迁移的边上，这个系统称为标记迁移系统（Labelled Transitive System，LTS）。n（2）在每一个状态上，有某些性质被满足，这些性质描述为一个（古典逻辑，或者时态等逻辑）公式。n（3）与定理证明一样，系统要满足的性质也被刻画为逻辑公式。n（4）用自动机械的手段检测上述的性质是否在系统的每个轨迹上都被满足，这里的轨迹是指系统的一个可能迁移路径。模拟检测方法模拟检测方法n模型检测的方法完全是自动化的，是这个方法的优点。同时，这个方法的另一个缺点在于，尽管人们已经探索了20余年，但是状态爆炸问题还是没有得到解决方法，因而对于复杂的系统，
10、难以用模型检测的方法分析。更为实质性的一点是，常用的协议是不可判定的。这就决定了没有一个算法系统能够搜索协议所有可能的行为。n总之，这个方法注定是一个不完全的方法，其优点在于可能直观的发现协议的漏洞，然而如果没有发现协议存在漏洞，将不保证协议的正确性。它更适合于去它更适合于去发现协议的攻击，而并非去证明协议的正确性。发现协议的攻击，而并非去证明协议的正确性。互模拟等价互模拟等价 n理论计算机科学中互模拟是状态迁移系统间的等价关系。互模拟等价的系统间有相同的行为方式。直观上，如果两个系统的迁移动作是相互对应的则它们是互模拟的。在这种意义下，互模拟系统是观察者不可区分的。基于逻辑推理的方法和模型基
11、于逻辑推理的方法和模型 n这个方法属于定理证明范畴，它遵循定理证明的一般规律。BAN逻辑的构成逻辑的构成 nBAN逻辑系统所做的假设如下：n（1）密文块不能被篡改，也不能用几个小的密文块组成一个新的大密文块。n（2）一个消息中的两个密文块被看作是分两次分别到达的。n（3）总假设加密系统是完善的，即只有掌握密钥的主体才能理解密文消息，因为不知道密钥的主体不能解密得到明文，攻击者无法从密文推断出密钥。n（4）密文含有足够的冗余信息，使解密者可以判断他是否应用了正确的密钥。n（5）BAN逻辑还假设参与协议的主体是诚实的 BAN逻辑的构成逻辑的构成n作为一种多类型模态逻辑，BAN逻辑包含3种处理对象：
12、主体、密钥和公式。公式也称为语句或命题。协议的每个消息表达为该逻辑的一个公式。n假设P、Q、R、代表一般意义上的主体nA、B、C代表具体的认证主体nS代表可行第三方nIDA代表主体A的身份标识nKab、Kas、Kbs代表具体认证主体的共享密钥，Ka、Kb、Kc代表具体认证主体的公开密钥，Ka1、K b1、Kc1代表具体认证主体，K代表一般意义上的加密密钥nNa、Nb、Nc代表具体的观点（如随机数）nX、Y是一般意义上的消息。BAN逻辑的基本公式及其语义 nP|=X P相信X；P相信X为真。nPX P看见X；P曾经收到过包含X的消息并且读到了X。nP|X P曾经说过X；P曾经发送过包含X的消息。
13、nP|X P可以裁定X；信任P对于X的真值的判定。n#(X)X是新鲜的；X在当前协议运行前没有被发现过。nP Q P 和Q分享一个好的密钥K。意思是，密钥K对于P、Q以及他们信任的主体来说仍然具有保密性。n P P具有密钥K，相应的私钥是K1，这个私钥只有P以及他信任的人知道。nP Q P和Q分享秘密X，这个秘密只有P、Q以及他们信任 的人知道。nXK 用K加密X后的消息。nY X与消息Y结合。KKXnBAN的推导规则直观的反映了逻辑公式构造的语义，我们把“逻辑公式X1、X2、Xn成立则Y成立”记为：nBAN的19条推理规则 12.nXXXY，理想化协议理想化协议 n在常见的协议中，每个协议步
14、的一般写法是：P Q:message，表示主体P发给主体Q消息，这种使用非形式化符号的表达通常是模糊的，不适合作为形式化分析的基础。所以有必要把协议的每一步转化成一种理想的形式。n例如：nA B:A,KabKbs应该告诉B（它知道密钥Kbs）Kab是它和A进行通信的密钥，这一步应该理想化为：A B:A BKbsn理想化后的协议比传统的描述具有更清楚和更完备的规范，因此在生成和描述协议时应该使用理想化的形式。abK 其它安全协议分析法其它安全协议分析法 n 归纳证明方法归纳证明方法n 串空间模型串空间模型n CSP方法方法 n 模型检测与定理证明的混合方法模型检测与定理证明的混合方法 n 互模拟
15、等价模型下的系统互模拟等价模型下的系统SPI演算演算n 计算方法计算方法 归纳证明方法归纳证明方法 n归纳证明方法是数学中最常用的方法之一。应用归纳证明协议的安全性可以不必一一考虑协议无限多种可能的行为，从而建立协议正确性的结论。n安全协议分析的一个特点就是要考虑攻击者的能力。在归纳分析中，Paulson定义了三种运算：parts，analz和synth。简单说来，parts(M)是消息集合M的所有消息的构成部分的集合。analz(M)是集合M中消息用（攻击者）可得到的密钥解密能够得到的消息的集合。而synth刻画的是消息的伪造。后两种运算实际上攻击者能力的刻画。这些运算都是归纳定义的，而协议
16、推理中起着主要作用。串空间模型串空间模型 n1997年，Fabrega、Herzag和Guttman建立了串空间（strand space）模型，将安全协议的形式化分析技术推向了一个新的高度。n串空间模型用于证明安全协议的正确性，可以分析安全协议中存在安全缺陷。应用串空间模型是，为集中精力分析安全协议本身的安全性，总是假设使用的密码系统是完善的。串空间模型串空间模型 n串空间是由协议主体，包括诚实主体和攻击者所组成的串集合。n丛是串空间模型中的重要概念，它表示一个完整的安全协议交换的串空间的子集，由一些合法的或不合法的串共同组成，其中一个串的发送消息对应于另一个串的接收消息（两个消息是相同的）。n串是一个主体发送、接收消息的线性序列。丛可以表示为图结构，表示一些串之间的通信。n在串空间模型中，通过证明串空间中发送包含某个数据项的消息的串是唯一的，说明数据项的新鲜性。CSP方法nCSP协议模型 ReceiveReceiveSenderSendReceiveA（Initiator）B（Responder）Instruder S（Server）Send
