安全协议理论与方法-课件

安全协议理论与方法基于攻击结构性方法安全协议理论与方法基于攻击结构性方法攻击结构性方法---简介■从协议的初始状态开始，对合法主体和一个攻击者的所有可能的执行路径进行穷尽搜索以期找到协议可能存在的错误。下面FDR,Mur以及特殊目的的NRL分析器等工具非常有效，但存在如下问题：■主体数目的有限性(限制)。主体数目很大和数目较少发现的问题可能不同。■无法解决状态空间爆炸问题。攻击结构性方法---简介■从协议的初始状态开始，对合法主体和一般目的的验证语言

■并非专门为安全协议形式化分析而设计的。其主要思想是将安全协议视为一般的目标，在不考虑其独有的特质的前提下验证其正确性。

此类形式化分析工具往往用到状态机的概念，它提供了描述和控制应用逻辑的非常强大的方法。■有限状态机FSM应用可达性分析技术来对认证协议进行分析。■缺陷：只考虑正确性，不考虑安全性。一般目的的验证语言■并非专门为安全协议形式化分析而设计的。一般目的的验证语言续—可达性技术■使用方法：■1.对于每一次迁移，使用主体和主体之间的信道状态来描述系统的全局状态。■2.分析每一个全局状态并判断其性质，如死锁、正确性等。如果分析表明一个主体在某一已知状态下应接收到某一消息却并未接收到时，则说明协议是有问题的。可达性技术可通过对协议的说明来判断协议的正确与否，但它并不能够保证协议的秘密性不受到主动攻击。一般目的的验证语言续—可达性技术■使用方法：一般目的的验证语言—形式化■此类技术的第一部是将协议描述为验证工具所使用的形式化语言：Kemmerer认为协议的形式化目标有两个：形式化地验证安全协议满足其所说明的安全需求；发现其说明中存在的漏洞。■方法：协议系统由不同状态组成，每个状态具有不同的状态变量值，状态值的变化是由良好定义的状态转换来决定的。■实现：使用一阶谓词逻辑扩展。一般目的的验证语言—形式化■此类技术的第一部是将协议描述为验一阶谓词逻辑扩展-基本逻辑操作&: 逻辑与。→：

逻辑推断。：

成员归属。{a,B,c…}: 元素集合。{setdescription}:集合说明。: 所有。

：

存在N”: 表示变量的新值。T”:定义了给定类型T的子类型。一阶谓词逻辑扩展-基本逻辑操作&: 逻辑与。主机会话密钥表终端密钥表终端1终端2终端3终端nK=0K=1主机密码设备包含终端密钥的终端密码设备主机会话密钥表终端密钥表终端1终端2终端3终端nK=一阶谓词逻辑扩展-实例说明每个终端确保有一个永久密钥用于每次会话建立时的会话密钥的分配。终端的永久密钥和会话密钥都以密文形式存放在主机处。■终端密钥常量：永久密钥。■终端会话密钥：变量。■变换：ECPH,DCPH,RFMK和Generate_session_key一阶谓词逻辑扩展-实例说明每个终端确保有一个永久密钥用于每次一阶谓词逻辑扩展-实例说明公理：加解密操作的相互抵消性不变式：■AXIOMtTEXT■k1,k2:KEY(Encrypt(k1,Decrypt(k2,t))=Decrypt(k2,Encrypt(k1,t)))InaJo准则给出了系统的所有状态将要达成的目标的说明，应当是贯穿协议运行始终而不发生改变的性质的说明---不变式。■攻击者不能获得解密密钥的不变式：■CRITERION:kkey(kintruder_infokkey_used)一阶谓词逻辑扩展-实例说明公理：加解密操作的相互抵消性不变式一阶谓词逻辑扩展-实例说明证明的步骤：■1.初始子句描述系统初始应满足的目标。■2.通过验证系统是否满足不变式要求发现问题。■3.例如证明初始状态是满足不变式说明的，之后证明由满足的状态触发的迁移后的状态也是满足不变式的，由此递归证明所有可达状态都是满足不变式的说明，否则系统有漏洞或不完整。

Kemmerer发现前述密钥分配结构有漏洞。一阶谓词逻辑扩展-实例说明证明的步骤：Mur验证系统■多处理器缓存同步协议和多处理器内存模式等领域应用的协议验证工具。■已验证TMN和KerberosV5有缺陷。协议形式化。在系统中加入一个攻击者。说明正确性成立的关键条件。确定协议规模之后运行协议。对协议进行反复的检测。Mur验证系统■多处理器缓存同步协议和多处理器内存模式等领Mur验证系统Mur描述语言:描述非确定性有限状态自动机的高级语言。■说明的常量和类型■变量说明■转换规则■初始状态生成规则■不变式描述Mur验证系统Mur描述语言:描述非确定性有限状态自动s2s1s0s3s4状态图例s2s1s0s3s4状态图例系统的应用例(审查)■模型的状态定义为所有全局变量取值的集合。■状态的转换由规则决定。■系统的执行由一个有限或无限的状态序列s0,s1,…,sn组成。SiSi+1：Si+1的获得可通过应用在状态si中的条件为真规则，即状态si的迁移由此种规则触发。由于一个状态允许多个行为的执行，因此Mur模型有多种执行的可能(非确定性)。例如攻击者选择重放的消息的行为是非确定性的。系统的应用例(审查)■模型的状态定义为所有全局变量取值的集合Mur验证系统2.语义和验证算法系统状态图(Q,Q0,error,)Simple-on-the-fly-Algorithm()Begin reached=unexpanded={q|qstartstate}; whileunexpandeddo removeastatefromunexpanded; foreachtransitionruletMur验证系统2.语义和验证算法Mur验证系统Mur的局限性及发展为协议运行定义所有可能的状态，并为此产生非确定有限状态自动机模型。状态可能太多，需要优化，否则时间和空间消耗太大。Mur验证系统Mur的局限性及发展CSP与安全性质■通讯顺序进程CSP是C.A.R.Hoare提出的为解决并发现象而提出的代数理论，是一个专为描述并发系统中通过消息交换进行交互的通信实体行为而设计的一种抽象语言。它将所分析的协议性质与具体的协议形式加以区别，并在CSP总体框架下对协议的性质进行分析和验证。■CSP可应用于网络安全协议的描述与分析：

将安全协议的问题规约为CSP进程是否满足其CSP说明的问题。CSP与安全性质■通讯顺序进程CSP是C.A.R.HoaCSP与安全性质■1.CSP基本术语事件(Event)进程(Process)路径(Trace)规约(Specification)CSP与安全性质■1.CSP基本术语CSP与安全性质■(1)事件(Event)所有可能的事件记为。c.i.j.m: c：信道 i:消息源 j:目的地 m:消息{m.n|mMnN},M,N消息集合。c.m：c上传送的消息是M类型的，c.mM。eventput.5：信道put上的数值5.CSP与安全性质■(1)事件(Event)CSP与安全性质■(2)进程(Process)用进程可能涉及的事件来描述进程。停止进程STOP输出进程输入进程选择进程并发进程递归进程CSP与安全性质■(2)进程(Process)CSP与安全性质■停止进程STOP

STOP进程不包括任何事件，它等价于死锁。■输出进程

c!vP:表示在信道c上输出v之后行为表现为P。■输入进程 c?x:TP(x):表示在信道c上可接收类型为T的任意输入x之后行为表现为P(x)。CSP与安全性质■停止进程STOPCSP与安全性质■选择进程PQ: 表示行为在P和Q之间做选择，结果或为P或为Q。iIPI:表示行为可为变量Pi的任何值。并发进程P|[D]|Q:

表示P和Q是并发执行的，并且它们是与同步集合D中的事件同步执行的。如果同步集合D中事件发生，则P,Q同步执行；如果发生的事件不属于D，则P,Q分别执行。如果P，Q之间没有任何同步事件，表示为P||Q。CSP与安全性质■选择进程CSP与安全性质■递归进程LIGHT=onoffLIGHT:表示进程LIGHT交替执行on和off。 COUNT(0)=upCOUNT(1) COUNT(n+1)=(upCOUNT(n+2))

(downCOUNT(n))COUNT(0)可执行任意个up和不超过up的down事件。CSP与安全性质■递归进程CSP与安全性质■(3)路径进程P定义为其可能执行的事件的序列，用路径表示(trace(P))---tr(P)。前述LIGHT进程可能的路径：<on-off-on>。空路径<>。CSP与安全性质■(3)路径CSP与安全性质■trD:表示tr中由D中事件组成的最大子序列。如果D是由一个事件组成{d}，那么 tr{d}等价于trd。■trc：表示在信道c上传输的最长消息序列。■trc：表示在c中某些信道上传输的消息集合。■(tr):表示在路径tr上出现的事件集合。

(P)：表示在进程P的某些路径上出现的事件集合。CSP与安全性质■trD:表示tr中由D中事件组成的最大CSP与安全性质■(4)规约一个进程满足一个规约S当且仅当其所有路径满足S，描述如下： P

sat

S

trtrace(P).S例如:事件a必须在事件b之前发生,描述为： tr1,tr2.tr=tr1<b>tr2tra<>简化：trb<>tra<>表示如果事件b在某路径tr中发生，事件a必定已发生。CSP与安全性质■(4)规约CSP与安全性质

网络高度抽象图

in0out1in1out1inioutiCSP与安全性质in0out1in1out1inioutiCSP与安全性质■MESSAGE：表示由任一用户发送的所有消息。■USER={0,1,…,n}。■in.i类型为USER.MESSAGE。■in.i.j.m:表示用户i向用户j发送消息m。■out.j:类型为USER.MESSAGE。■out.i.j.m：表示用户i接收用户j的消息m。CSP与安全性质■MESSAGE：表示由任一用户发送的所有CSP与安全性质用户仅需了解与网络的交互行为：1.从网络用户的角度考虑,用户不知道网络中哪些用户是可信的。用户的通信模式不与协议目标相矛盾。例如任何共享秘密不应泄漏给第三方。CSP与安全性质用户仅需了解与网络的交互行为：CSP与安全性质2.从高层角度考虑，用户被视为忠实执行其协议的节点，并能够识别协议中的漏洞。当采用这一角度时,必须注意此特定消息是不能未加考虑地出现在协议的说明中的,一个节点的响应不应依赖于只在高层看来有效的消息。本书从2)考虑,用0USER作为攻击者进程名字。CSP与安全性质2.从高层角度考虑，用户被视为忠实执行其协CSP与安全性质保密性如果除了意定消息接收者外任何用户都不可能从集合M中计算出任何消息，那么特定的消息集合M的保密性是成立的。换言之：如果有输入in.i.j.m,那么任何输出out.h.l.m都是发自用户j的。因此已知用户j和消息m,如果有一个输出out.j.k.m,则在此之前必有in.i.j.m的输入。因此j不能获得任何发给其他主体的消息。从一个高层的角度考虑，唯一能够获得发给其他主体的消息的用户是user0,因此保密性可描述为：user0的任何输出消息必定是在此之前已发送给user0的消息。CSP与安全性质保密性CSP与安全性质■定义4.1NET为消息集合提供保密性，当且仅当NETsatm:M. trout.0.USER.m<> trin.USER.0.m<>

用CSP进程代数表示为： m:M. NET|[in.USER.0.M]|STOP= NET|[out.0.USER.m]|STOP in.USER.0.m(此处有问题？)CSP与安全性质■定义4.1NET为消息集合提供保密性，当且CSP与安全性质

CONF(tr)=messages(trout.0.USER.M)

messages(trin.USER.0.M)■表示user0输出的消息必是发送给它的消息的子集。换言之，user0不能从不是发给它的消息M中获得任何消息。CSP与安全性质 CONF(tr)=messages(tCSP与安全性质认证性：消息和消息源不能被伪造。定义4.2

在进程p中事件b认证事件a，当且仅当: psatAUTH(tr)，其中 AUTH(tr)=trb<>tra<>

如果只有在事件a发生后事件b才发生，则称事件b认证事件a。 P|[a,b]|STOP=P|

[a]|STOPCSP与安全性质认证性：消息和消息源不能被伪造。CSP与安全性质(此页有问题)■对于一个包括媒介、攻击者和节点的系统，认证性可描述为：NET|[in.i.j.m]|STOP=out.j.i.mNET |[in.i.j.m]缓冲区进程COPY=in?xout!COPYCSP与安全性质(此页有问题)■对于一个包括媒介、攻击者和节CSP与安全性质■定义4.3在进程P中B认证A，当且仅当 P|[AB]|STOP=P|[A]|STOP如果B中的任何消息已出现，那么A中的一个消息必定在此之前已出现。CSP与安全性质■定义4.3在进程P中B认证A，当且仅当CSP与安全性质■3.CSP网络模型体系结构：可借助媒介彼此发送消息而进行异步通信的节点网络。由于用户不能控制媒介，因此攻击者有可能会干扰或截获网络通信。模拟：

将节点集连接到媒介上，并将每个节点视为一个独立的进程。CSP与安全性质■3.CSP网络模型CSP与安全性质■用CSP描述DY模型。该模型中,通信媒介完全受控于攻击者之下,可拦截、重放、复制以及伪造消息。S├m：表示S中消息的所有知识可生成消息m。ENEMY:不安全网络的化身(攻击者和不安全网络媒介)(USERi)trans.irec.iCSP与安全性质■用CSP描述DY模型。CSP与安全性质■整个通信网络可描述为：NET=(║|jUSERj)|[trans,rec]|ENEMYtrans和rec类型为：USER.USER.MESSAGE(trans和rec没有给出定义)trans.i.j.m:源节点i发送消息m给目的节点j。CSP与安全性质CSP与安全性质CSP描述网络

■消息空间描述

■ENEMY描述

■网络通信主体的描述CSP与安全性质CSP与安全性质■(1)消息空间描述RAW:=USER|TEXT|NONCE|KEYMESSAGE:=RAW|KEY(MESSAGE)|MESSAGE.MESSAGEKEY:=PUBLIC|SECRETCSP与安全性质■(1)消息空间描述CSP与安全性质■生成消息的规则A1ifmSthenS├mA2if

S├m

andSS’thenS’├mA3ifS├miforeachmiS’andS’├mthenS├mM1 S├mS├kS├k(m)M2 S├m1S├m2S├m1,m2K1 E(pi:E(si:m))├m???K2 E(si:E(pi:m))├m???CSP与安全性质■生成消息的规则CSP与安全性质■(2)ENEMY描述MEDIUM(T)= tTrec!tMEDIUM(T\{t})

trans?i?j.mMEDIUM(T{j,i,m})

tTleak!tMEDIUM(T)

add?i?j?mMEDIUM(T{j,i,m})

kill?tMEDIUM(T\{t})T是在被动媒介上传递的消息集合。CSP与安全性质■(2)ENEMY描述CSP与安全性质■INTRUDER(U)= leak?uINTRUDER(U{u})

(U├m),I,jadd!i.j.mINTRUDER(U)

(U├m),I,jkill!i.j.mINTRUDER(U)将INTRUDER和MEDIUM二合一描述网络环境： MEDIUM(T) |[leak,add,kill]| INTRUDER(U)\{leak,add,kill}CSP与安全性质■INTRUDER(U)=CSP与安全性质■ENEMY(S)=trans?i?j?mENEMY(S{m})

I,jUSER,S├mrec.i.j.mENEMY(S)解释：ENEMY可读取在trans任一信道上任一用户输出的消息，并且它可以向任一用户发送它可生成的任何消息。集合S中包括ENEMY知道的所有消息，并且每当有新消息发送时，S将得到更新。CSP与安全性质■ENEMY(S)=trans?i?j?mCSP与安全性质■ENEMY

sat(INIT(trtrans))├trrec■INIT:ENEMY初始知识集合，其中包括用户名、公钥以及一些攻击者用到的随机数。CSP与安全性质CSP与安全性质■(3)协议主体的描述修改后的NSLAB: E(Kb:Na,A)BA: E(Ka:Na,Nb,B)AB: E(Kb:Nb)CSP与安全性质■(3)协议主体的描述CSP与安全性质协议主体A的进程USERa描述为：■USERa=iUSERtrans.A!i!E(Ki:Na,A) rec.A.i?E(Ka:Na,x,i) trans.A!i!E(Ki:x)STOP■USERb=jUSERrec.B?j?E(Kb:y,j) trans.B!j!E(Kj:y,Nb,B) rec.B.j.E(Kb:Nb)STOPCSP与安全性质协议主体A的进程USERa描述为：CSP与安全性质■(4)CSP对NSL公钥协议的形式化分析步骤：建立安全协议的CSP模型。用CSP描述安全协议的安全性质。验证协议的安全性质是否满足。CSP与安全性质■(4)CSP对NSL公钥协议的形式化分CSP与安全性质■认证性的目标：如果在进程P中R的一些事件在T的一些事件之前发生，则T认证R，其中T，R为不相交的事件集合。TauthenticatesR=trR=<>trT=<>对于进程P：P

satTauthenticatesR P|[R]|STOPsattrT=<>■如果P满足T认证R且RR’,那么P满足TauthenticatesR’CSP与安全性质■认证性的目标：CSP与安全性质■认证性在整个网络NET满足的条件为：C1: mINIT.I(m)C2: (m’S.I(m’))S├mI(m)C3: mT.I(m)C4:i.(USERi|[R]|STOP)msatmaintainsI) thenNET|[R]|STOPsattrT=<>CSP与安全性质■认证性在整个网络NET满足的条件为：CSP与安全性质■断言I：表示在一轮协议中，当集合R中的消息不能出现时(包括ENEMY)，有些主体(包括ENEMY)生成的所有消息是成立的。C1、C2表明如果攻击者只知道满足I的消息，那么它只能生成满足I的消息。C3:对于T中的某些消息I是不成立的。C4:

对于网络用户除非他们事先收到了一个消息，否则他们决不可能输出一个不满足I的消息。CSP与安全性质■断言I：表示在一轮协议中，当集合R中的消息CSP与安全性质■maintainsI(tr)= (m(trrec):I(m))

(m(trtrans):I(m))■意义：如果在rec上收到的每一个消息满足I，那么在trans上输出的每一个消息也满足I。CSP与安全性质■maintainsI(tr)=CSP与安全性质■证明：rec.B.A.E(Kb:Nb)authenticatestrans.A.B.E(Kb:Nb),为证明NSL的这条性质，首先构造一个适合的断言I。■I(m) mUSER mTEXT mNONCEmNb mSECRETmSamSb mPUBLICCSP与安全性质■证明：rec.B.A.E(Kb:Nb)aCSP与安全性质m’:MESSAGE,k:PUBLICm=k(m’)((k=kam’NONCE.Nb.B)I(m’):m’:MESSAGE,k:SECRET.m=k(m’)((k=Sam’E(Ka:NONCE.Nb.B))I(m’))m1,m2,MESSAGE:m=m1.m2I(m1)I(m2)CSP与安全性质m’:MESSAGE,k:PUBLICCSP与安全性质■验证I是否满足所有条件。C1:根据协议的基本假设，显然I是满足C1的。C2：C2给出了生成关系与断言之间的交互性。M1:S├mS├kS├k(m).如果m’S.I(m’)■那么根据归纳假设可得I(m)和I(k)。k有两种可能：公钥或者私钥。CSP与安全性质■验证I是否满足所有条件。CSP与安全性质■如果K是公钥，那么I(m)成立，意味着I(Ki(m))成立。如果k是私钥，那么iA,并且I(m)意味着I(Si(m))成立。

C3:检查构成T的惟一消息E(Kb:Nb)。由于I(Nb):根据I的定义，有I(E(Kb:Nb))成立。C4:检查USERa和USERb是否满足C4。这等价于无论是USERa还是USERb，当trans.A.B.(E(Kb:Nb))禁止时，都不能引入任何不满足I的消息。CSP与安全性质■如果K是公钥，那么I(m)成立，意味着I(CSP与安全性质■RUSERa= USERa|[trans.A.B.E(Kb:Nb)]|STOP=

iUSERtrans.A!i!E(Ki:Na,A) rec.A.i?E(Ka:Na,x,i) STOP Ifi=bx=Nb trans.A!i!E(Ki:x)STOP ifibxNbCSP与安全性质■RUSERa=CSP与安全性质■C4表明如果进程的每一个接收消息满足I，那么它的每一个输出消息也满足I。■RUSERa的第一步是消息E(Ka:Na,A)发送给主体i，由I的定义有I(Ka:Na,A)，所以由RUSERa发送的第一条消息是满足C4的。第二步是收到消息E(Ka:Na,x,i)。由I的定义，有Na,x,iNONCE.Nb.B及I(Na,x,i)。对于第3步的第一种情况，RUSERa不再发送任何消息，故不可能违反说明；在第二种情况发送了消息E(Ki:x)。CSP与安全性质■C4表明如果进程的每一个接收消息满足I，那CSP与安全性质■(接上页)并且由于I(x)，有I(E(Ki:x))成立，故说明是满足的。同理可完成对USERb的证明。最后，可以得出：NETsat rec.B.A.E(Kb:Nb)authenticatestrans.A.B.E(Kb:Nb)，说明修改后的NS协议其认证性是满足的。CSP与安全性质■(接上页)并且由于I(x)，有I(E(KiModelChecking概述消息空间ModelChecking协议模型基于CSP的模型检测工具FDR模型检测技术与逻辑推证技术的混合使用ModelCheckingModelChecking—概述■给定一个模型M和逻辑描述的性质P，检查M╞P，即在模型M中性质P是否成立。Marrero等人通过检查在恶意攻击者存在的情况下，协议运行的所有可能的路径，可以判断协议是否满足了其安全保证。如果没有，将给出攻击者的攻击路径。■秘密性：运用模型检查器验证攻击者不可获得其不应获知的秘密。■认证性：如果事件X发生了，那么事件Y必定在此之前已发生。ModelChecking—概述■给定一个模型M和逻辑描ModelChecking—消息空间密钥：(K-1:E(K:(m)))=m主体标识：公开随机量：包含随机量的消息是新消息正文若A代表原子消息空间，则消息集合M可定义为：若m1M,且m2M,(m1,m2)M若mM,且kA,则{m}kMModelChecking—消息空间密钥：(K-1:EModelChecking—消息空间若mI,则I├m。(包含)若I├m1,且I├m2,则I├(m1,m2)。(复合)若I├(m1,m2),则I├m1,且I├m2。(投影)若I├m,且I├k,则I├E(K:m)。(加密)若I├E(K:m)且I├K-1,I├m。(解密)ModelChecking—消息空间ModelChecking协议模型■(1)主体表示为一个四元组:<N,P,I,B>Nnames:主体的名字。P:过程描述，为执行动作的序列。IM：主体知道的消息集合。M是所有可能的消息集合。I是无限的且在加解密、复合和投影操作下是封闭的。B:vars(P)I:绑定集合,vars(P)是过程P中出现的变量的集合。ModelChecking协议模型■(1)主体表示为一个ModelChecking协议模型■(2)协议的全局变量记为五元组<Л,Ci,Cr,Ss,St>■Л,参与协议的主体和攻击者进程的结果。■Ci,namesXnamesN计数器集合，用于记录主体A发起于主体B的协议轮数与B完成的对A响应的次数之差。若出现负值，则表明B已经完成了协议中对A的响应，但A并未参与协议的运行。ModelChecking协议模型■(2)协议的全局变ModelChecking协议模型■Cr,namesXnamesN计数器集合，用于记录主体A已经完成的对B响应的次数与完成的B发起的与A的协议轮数之差。若出现负值，则表明B已经完成了发起与A的一个协议，但A并未参与协议的运行。■SsM,不会泄密的消息集合。如私钥集合。■StM，协议运行时新产生的秘密消息集合，有可能被攻击者截获，例如会话密钥。ModelChecking协议模型■Cr,namesModelChecking协议模型■通信行为的执行引起的状态转换：(s,SEND,m,s’)(s,REC,m,s’)(s,A,m,s’)ModelChecking协议模型■通信行为的执行引起的ModelChecking协议模型■(1)(s,SEND,m,s’)一个主体发送消息m后，状态由s转换到s’，当且仅当：I’=Im(攻击者可截获此消息)。主体的说明由i变为i’,其中：

i=<Ni,SEND(S-msg).Pi’,Ii,Bi>

i’=<Ni,Pi’,Ii,Bi>

且Ii’=Iim。3) j

=j’(ji)ModelChecking协议模型■(1)(s,SENModelChecking协议模型■(2)(s,REC,m,s’)一个主体接收消息m后，状态由s转换到s’，当且仅当：mI’(攻击者可生成此消息)。主体的说明由i变为i’,其中：

i=<Ni,REC(R-msg).Pi’,Ii,Bi>

i’=<Ni,Pi’,Ii’,Bi’>

且Ii’=Iim。3) j

=j’(ji)ModelChecking协议模型■(2)(s,RECModelChecking协议模型■(3)(s,A,m,s’)一个主体完成用户定义的主体为消息m的行为A后,状态由s转换到s’，当且仅当：主体的说明由i变为i’,其中：

i=<Ni,A(msg).Pi’,Ii,Bi)

i’=<Ni,Pi’,Ii,Bi)

且m=(msg)。2) j

=j’(ji)。ModelChecking协议模型■(3)(s,A,m,ModelChecking协议模型■攻击者表示为=<N,,N,>■主体表示为：i=<Ni,Pi,Ii,Bi>■:绑定集合B从变量域到消息模式域增大的部分。■参与协议的双方主体为达成双向认证，必须确保在通信中攻击者不能伪装成合法主体参与协议的运行。ModelChecking协议模型■攻击者表示为=<NModelChecking协议模型■协议发起者行为

■协议响应方行为Beginit BegRespondEndinit EndRespondModelChecking协议模型■协议发起者行为 ModelChecking协议模型■Ci(A,B)=Beginit(A,B)–EndRespond(B,A)■Ci(A,B)>0:正常。■Ci(A,B)<0:表明B已经完成了协议中对A的响应，但A并未参与协议的运行，暗示有非法攻击者冒充A的身份与B对话。ModelChecking协议模型ModelChecking协议模型■Cr(A,B)=BegRespond(B,A)–EndInit(A,B)意义：为B完成的对A响应的次数与主体A已经完成的其向B发起的协议次数之差。■Cr(A,B)>0:正常。■Cr(A,B)<0:表明A已经完成了发起与B的协议，但B并未参与协议的运行，暗示有非法攻击者冒充B的身份与A对话。ModelChecking协议模型■Cr(A,B)=BeModelChecking协议模型■1)如果A发起一个与B通信的一轮协议，有：<A,Beginit(A,B).P’,IA,BA><A,P’,IA,BA>,那么 Ci(A,B)+1ifCi(A,B)isdefinedCi(A,B) otherwise■2)如果B完成了一次对A的响应，有：<B,EndRespond(B,A).P’,IB,BB><B,P’,IB,BB

>,那么 Ci(A,B)-1 ifCi(A,B)>0error otherwiseCr(A,B)=Cr(A,B)=ModelChecking协议模型■1)如果A发起一个ModelChecking协议模型■3)

如果B开始一个响应A的一轮协议，有：<A,BegRespond(B,A).P’,IA,BA><A,P’,IA,BA>,那么 Cr(A,B)+1ifCr(A,B)isdefinedCr(A,B) otherwise■4)

如果B完成了一次与A通信的发起，有：<B,Endinit(B,A).P’,IB,BB><B,P’,IB,BB

>,那么 Cr(A,B)-1 ifCr(A,B)>0 error otherwiseCr(A,B)=ModelChecking协议模型■3) 如果B开始一ModelChecking协议模型■协议路径是一条由全局状态和行为交替出现的序列，模型检测试图检查所有可能的路径。模型的一次执行对应一条有限的状态与行为交替出现的路径。■使用report-error算法记录所有出错状态。ModelChecking协议模型■协议路径是一条由全局ModelChecking协议模型ProcDFS(global-state)Push(global-state,S)While(notempty(S))do{<Л,Ci,Cr,Ss,St>=pop(S)ifCi(x,y)<0forsomexandyor Cr(x,y)<0forsomexandyor sIzforsomesSsSt thenreport-errorL=next-states(<Л,Ci,Cr,Ss,St>)ForeachlLpush(S,l)ModelChecking协议模型ProcDFS(g基于CSP的模型检测工具FDR■1)理解协议中各主体进程、目标以及可能的假设等等。■2)用形式化语言描述主体的行为、协议的安全目标，以及攻击者的初始知识库。■3)用Model–Checking工具自动检查协议是否能满足给出的安全目标。■4)如果Model-Checking工具输出攻击序列，则分析攻击的有效性。基于CSP的模型检测工具FDR■1)理解协议中各主体进程、目基于CSP的模型检测工具FDRNeedhamSchroeder公开密钥协议为A、B双方的双向认证的简化版本：AB:E(Kb:Na,A)BA:E(Ka:Na,Nb,B)AB:E(Kb:Nb)基于CSP的模型检测工具FDRNeedhamSchroe基于CSP的模型检测工具FDR■FDR验证协议时，首先要刻画主体的行为。协议发起方开始认证协议的事件为I_running,完成认证协议的事件为I_commit;协议响应方开始协议的事件为R_running,完成协议的事件为R_commit,协议主体之间的通信事件为comm。基于CSP的模型检测工具FDR■FDR验证协议时，首先要刻基于CSP的模型检测工具FDRInitiator(a,na)= User.a?bI_running.a.b Comm!Msg1.a.b.Encrypt.key(b).na.a Comm.Msg2.b.a.Encrypt.key(a).na’.Nb ifna=na’ thencomm.!Msg3.a.b.Encrypt.key(b).nb I_commit.a.bsession.a.bskip elseStop基于CSP的模型检测工具FDRInitiator(a,na)基于CSP的模型检测工具FDR■攻击者截获并试图解密消息一的进程：■其中Ki是攻击者I的公开密钥。Intercept.Msg1?a.b.Encrypt.k.n.a’Ifk=Ki

thenI(m1s,m2s,m3s,ns{n})else I(m1s{Encrypt.k.n.a’},m2s,m3s,ns)基于CSP的模型检测工具FDR■攻击者截获并试图解密消息一的基于CSP的模型检测工具FDR■攻击者重放以前截获的消息(1)进程:fake.Msg1?a.b?m:m1sI(m1s,m2s,m3s,ns)■攻击者用得到的随机数n生成冒充消息(1)的消息：fake.Msg1?a.b!Encrypt?k?n:ns?a’ I(m1s,m2s,m3s,ns)基于CSP的模型检测工具FDR■攻击者重放以前截获的消息(1基于CSP的模型检测工具FDR进程刻画双向认证协议要满足的性质：■I_running必须在R_commit之前发生。■R_running必须在I_commit之前发生。■AR0=R_running.A.BI_commit.A.BAR0■AI0=I_running.A.BR_commit.A.BAI0运行FDR发现攻击：基于CSP的模型检测工具FDR进程刻画双向认证协议要满足的性基于CSP的模型检测工具FDRa.1)AT:A,T,{Na,A}kTb.1)T(A)B:A,B,{Na,A}Kbb.2)BT(A):B,A,{Na,Nb}Kaa.2)TA:T,A,{Na,Nb}Kaa.3)AT:A,T,{Nb}kTb.3)T(A)B:A,B,{Nb}KbBAN逻辑不能考虑主体同时参与过个协议进程的情况。基于CSP的模型检测工具FDRa.1)AT:A,T,模型检测与逻辑推证技术混合使用—方法一方法一：■首先运用逻辑推证工具对协议进行分析，如果发现了协议的漏洞以及导致此漏洞的关键性假设，则运用模型检测工具有针对地为关键性假设构造可能的现实攻击路径。协议关键性假设可能涉及的内容有：■关于主体行为的假设■关于重要消息的假设模型检测与逻辑推证技术混合使用—方法一方法一：模型检测与逻辑推证技术混合使用—方法一Case1:如果协议主体P的行为是可信的，则用攻击者不诚实主体身份取代主体P的地位与其他诚实主体依协议进行额外的会话，用模型检测工具分析此会话并找出可能的攻击路径。Case2：如果对方通信主体的行为是可信的，则用攻击者不诚实主体身份取代对方主体的地位与主体P依协议规则进行额外的会话，用模型检测工具分析此会话并找出可能的攻击路径。模型检测与逻辑推证技术混合使用—方法一Case1:如果协议主模型检测与逻辑推证技术混合使用—方法一Case

3：如果协议主体相信某一重要消息，则用模型检测技术检测攻击者是否能够再生成此消息，或将此消息说明为一个不安全状态，运用模型检测工具检查此状态是否可达。模型检测与逻辑推证技术混合使用—方法一模型检测与逻辑推证技术混合使用—方法二方法二：■首先运用模型检测工具对协议进行分析，如果发现协议是不安全的，则使用逻辑推证工具去判断协议的哪一个假设是导致协议遭受现实攻击的原因。模型检测与逻辑推证技术混合使用—方法二方法二：模型检测与逻辑推证技术混合使用—方法二■1）先用逻辑推证工具将找到的攻击路径说明为一个协议，其中攻击者作为参与协议运行的主体。■2）说明此协议应满足的安全目标，如秘密性，认证性等。■3）根据推理规则和公理以及协议欲达成的目标对协议中的主体增加相应的假设条件，使得构造的协议是安全的。■4）分析所提出的额外的假设，并由此发现导致协议错误的关键性假设。模型检测与逻辑推证技术混合使用—方法二■1）先用逻辑推证工具模型检测与逻辑推证技术混合使用—方法二■协议1AB: {M}kaBA: {{M}ka}kbAB: {M}kb■协议2AS: A,{Ta,B,Kab}kasSB: {Ts,A,Kab}kbs模型检测与逻辑推证技术混合使用—方法二■协议1模型检测工具对协议的分析■对协议1的分析诚实主体： A和B。攻击者： Z攻击者知识集合： KS协议应满足的安全性为：秘密性MKS模型检测工具对协议的分析■对协议1的分析模型检测工具对协议的分析■经自动检测工具发现协议1违反了秘密性：AZ(B): {M}KaZ(B)A: {M}KaAZ(B): M■认证性：模型检测工具未能发现协议1可能的认证缺陷。模型检测工具对协议的分析■经自动检测工具发现协议1违反了秘密模型检测工具对协议的分析■对协议2的分析认证性：对于协议一轮的运行，认证的性质是成立的。但如果A、B皆发起多个会话，认证性将不成立。攻击为：AS: A,{Ta,B,Kab}kasSB: {Ts,A,Kab}kbs1’) Z(B)S:B,{Ts,A,Kab}kbs2’) SZ(A): {Ts,B,Kab}kas模型检测工具对协议的分析■对协议2的分析模型检测工具对协议的分析1”) Z(A)S:A,{Ts’,B,Kab}kas2”) SZ(B): {Ts”,A,Kab}kbs1”中的Ts’有问题，本应为Ta。■秘密性：kabKS■在协议认证性被破坏后，存在一个攻击破坏协议的秘密性，描述为：AZ(S):A,{