安全协议理论与方法-课件.ppt_163文库

资源描述

1、安全协议理论与方法基于攻击结构性方法攻击结构性方法-简介从协议的初始状态开始，对合法主体和一个攻击者的所有可能的执行路径进行穷尽搜索以期找到协议可能存在的错误。下面FDR,Mur以及特殊目的的NRL分析器等工具非常有效，但存在如下问题：主体数目的有限性(限制)。主体数目很大和数目较少发现的问题可能不同。无法解决状态空间爆炸问题。一般目的的验证语言并非专门为安全协议形式化分析而设计的。其主要思想是将安全协议视为一般的目标，在不考虑其独有的特质的前提下验证其正确性。此类形式化分析工具往往用到状态机的概念，它提供了描述和控制应用逻辑的非常强大的方法。有限状态机FSM应用可达性分析技术来对认证协议进

2、行分析。缺陷：只考虑正确性，不考虑安全性。一般目的的验证语言续可达性技术使用方法：1.对于每一次迁移，使用主体和主体之间的信道状态来描述系统的全局状态。2.分析每一个全局状态并判断其性质，如死锁、正确性等。如果分析表明一个主体在某一已知状态下应接收到某一消息却并未接收到时，则说明协议是有问题的。可达性技术可通过对协议的说明来判断协议的正确与否，但它并不能够保证协议的秘密性不受到主动攻击。一般目的的验证语言形式化此类技术的第一部是将协议描述为验证工具所使用的形式化语言：Kemmerer认为协议的形式化目标有两个：1.形式化地验证安全协议满足其所说明的安全需求；2.发现其说明中存在的漏洞。方法：协

3、议系统由不同状态组成，每个状态具有不同的状态变量值，状态值的变化是由良好定义的状态转换来决定的。实现：使用一阶谓词逻辑扩展。一阶谓词逻辑扩展-基本逻辑操作&:逻辑与。：逻辑推断。：成员归属。a,B,c:元素集合。set description:集合说明。:所有。：存在N”:表示变量的新值。T”:定义了给定类型 T的子类型。主机会话密钥表终端密钥表终端1终端2终端3终端nK=0K=1主机密码设备包含终端密钥的终端密码设备一阶谓词逻辑扩展-实例说明1.每个终端确保有一个永久密钥用于每次会话建立时的会话密钥的分配。2.终端的永久密钥和会话密钥都以密文形式存放在主机处。终端密钥常量：永久密钥。终端会话

4、密钥：变量。变换：ECPH,DCPH,RFMK和Generate_session_key一阶谓词逻辑扩展-实例说明公理：加解密操作的相互抵消性不变式：AXIOM tTEXTk1,k2:KEY(Encrypt(k1,Decrypt(k2,t)=Decrypt(k2,Encrypt(k1,t)Ina Jo 准则给出了系统的所有状态将要达成的目标的说明，应当是贯穿协议运行始终而不发生改变的性质的说明-不变式。攻击者不能获得解密密钥的不变式：CRITERION:kkey(kintruder_infokkey_used)一阶谓词逻辑扩展-实例说明证明的步骤：1.初始子句描述系统初始应满足的目标。2.通过

5、验证系统是否满足不变式要求发现问题。3.例如证明初始状态是满足不变式说明的，之后证明由满足的状态触发的迁移后的状态也是满足不变式的，由此递归证明所有可达状态都是满足不变式的说明，否则系统有漏洞或不完整。Kemmerer发现前述密钥分配结构有漏洞。Mur验证系统多处理器缓存同步协议和多处理器内存模式等领域应用的协议验证工具。已验证TMN 和Kerberos V5有缺陷。1)协议形式化。2)在系统中加入一个攻击者。3)说明正确性成立的关键条件。4)确定协议规模之后运行协议。5)对协议进行反复的检测。Mur验证系统Mur描述语言:描述非确定性有限状态自动机的高级语言。说明的常量和类型变量说明转换规则

6、初始状态生成规则不变式描述s2s1s0s3s4状态图例系统的应用例(审查)模型的状态定义为所有全局变量取值的集合。状态的转换由规则决定。系统的执行由一个有限或无限的状态序列s0,s1,sn组成。SiSi+1：Si+1的获得可通过应用在状态si中的条件为真规则，即状态si的迁移由此种规则触发。由于一个状态允许多个行为的执行，因此Mur模型有多种执行的可能(非确定性)。例如攻击者选择重放的消息的行为是非确定性的。Mur验证系统2.语义和验证算法系统状态图(Q,Q0,error,)Simple-on-the-fly-Algorithm()Beginreached=unexpanded=q|qstar

7、tstate;while unexpanded doremove a state from unexpanded;for each transition rule tMur验证系统3.Mur的局限性及发展为协议运行定义所有可能的状态，并为此产生非确定有限状态自动机模型。状态可能太多，需要优化，否则时间和空间消耗太大。CSP与安全性质通讯顺序进程CSP是 C.A.R.Hoare 提出的为解决并发现象而提出的代数理论，是一个专为描述并发系统中通过消息交换进行交互的通信实体行为而设计的一种抽象语言。它将所分析的协议性质与具体的协议形式加以区别，并在CSP总体框架下对协议的性质进行分析和验证。CSP

8、可应用于网络安全协议的描述与分析：将安全协议的问题规约为CSP进程是否满足其CSP说明的问题。CSP与安全性质 1.CSP基本术语(1)事件(Event)(2)进程(Process)(3)路径(Trace)(4)规约(Specification)CSP与安全性质(1)事件(Event)所有可能的事件记为。c.i.j.m:c：信道i:消息源j:目的地m:消息m.n|mM nN,M,N消息集合。c.m：c上传送的消息是M类型的，c.mM。event put.5：信道put上的数值5.CSP与安全性质(2)进程(Process)用进程可能涉及的事件来描述进程。1)停止进程STOP2)输出进程3)输入

9、进程4)选择进程5)并发进程6)递归进程CSP与安全性质停止进程STOPSTOP进程不包括任何事件，它等价于死锁。输出进程c!vP:表示在信道c上输出v之后行为表现为P。输入进程c?x:TP(x):表示在信道c上可接收类型为T的任意输入x之后行为表现为P(x)。CSP与安全性质选择进程PQ:表示行为在P和Q之间做选择，结果或为P或为Q。iIPI:表示行为可为变量Pi的任何值。5)并发进程P|D|Q:表示P和Q是并发执行的，并且它们是与同步集合D中的事件同步执行的。如果同步集合D中事件发生，则P,Q同步执行；如果发生的事件不属于D，则P,Q分别执行。如果P，Q之间没有任何同步事件，表示为P|Q。

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

11、上传输的消息集合。(tr):表示在路径tr上出现的事件集合。(P)：表示在进程P的某些路径上出现的事件集合。CSP与安全性质(4)规约一个进程满足一个规约S当且仅当其所有路径满足S，描述如下：P sat S trtrace(P).S例如:事件a必须在事件b之前发生,描述为：tr1,tr2.tr=tr1tr2tra简化：trbtra表示如果事件b在某路径tr中发生，事件a必定已发生。CSP与安全性质网络高度抽象图 in0out1in1out1inioutiCSP与安全性质 MESSAGE：表示由任一用户发送的所有消息。USER=0,1,n。in.i 类型为 USER.MESSAGE。in.i

12、.j.m:表示用户i向用户j发送消息m。out.j:类型为USER.MESSAGE。out.i.j.m：表示用户i接收用户j的消息m。CSP与安全性质用户仅需了解与网络的交互行为：1.从网络用户的角度考虑,用户不知道网络中哪些用户是可信的。用户的通信模式不与协议目标相矛盾。例如任何共享秘密不应泄漏给第三方。CSP与安全性质2.从高层角度考虑，用户被视为忠实执行其协议的节点，并能够识别协议中的漏洞。当采用这一角度时,必须注意此特定消息是不能未加考虑地出现在协议的说明中的,一个节点的响应不应依赖于只在高层看来有效的消息。本书从2)考虑,用0USER作为攻击者进程名字。CSP与安全性质(1)保密性如

13、果除了意定消息接收者外任何用户都不可能从集合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与安全性质定义4.1NET为消息集合提供保密性，当且仅当NET sat m:M.trout.0.USER.m tr i

14、n.USER.0.m用CSP进程代数表示为：m:M.NET|in.USER.0.M|STOP=NET|out.0.USER.m|STOPin.USER.0.m(此处有问题？)CSP与安全性质CONF(tr)=messages(trout.0.USER.M)messages(trin.USER.0.M)表示user0输出的消息必是发送给它的消息的子集。换言之，user0不能从不是发给它的消息M中获得任何消息。CSP与安全性质(2)认证性：消息和消息源不能被伪造。定义定义4.24.2 在进程p中事件b认证事件a，当且仅当:p sat AUTH(tr)，其中AUTH(tr)=trb tra如果只有在

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

17、述 ENEMY描述网络通信主体的描述CSP与安全性质(1)消息空间描述RAW :=USER|TEXT|NONCE|KEYMESSAGE:=RAW|KEY(MESSAGE)|MESSAGE.MESSAGEKEY :=PUBLIC|SECRETCSP与安全性质生成消息的规则A1if mS then SmA2if Sm and SS then SmA3if Smi for each miSand Sm then SmM1Sm Sk Sk(m)M2Sm1 Sm2 Sm1,m2K1E(pi:E(si:m)m?K2E(si:E(pi:m)m?CSP与安全性质(2)ENEMY描述MEDIUM(T)=tT

18、rec!tMEDIUM(Tt)trans?i?j.mMEDIUM(Tj,i,m)t T leak!tMEDIUM(T)add?i?j?mMEDIUM(Tj,i,m)kill?tMEDIUM(Tt)T是在被动媒介上传递的消息集合。CSP与安全性质INTRUDER(U)=leak?uINTRUDER(Uu)(Um),I,j add!i.j.mINTRUDER(U)(Um),I,j kill!i.j.mINTRUDER(U)将INTRUDER和MEDIUM二合一描述网络环境：MEDIUM(T)|leak,add,kill|INTRUDER(U)leak,add,killCSP与安全性质ENEMY(S

19、)=trans?i?j?mENEMY(Sm)I,jUSER,Sm rec.i.j.mENEMY(S)解释：ENEMY可读取在trans任一信道上任一用户输出的消息，并且它可以向任一用户发送它可生成的任何消息。集合S中包括ENEMY知道的所有消息，并且每当有新消息发送时，S将得到更新。CSP与安全性质ENEMY sat(INIT(trtrans)trrecINIT:ENEMY初始知识集合，其中包括用户名、公钥以及一些攻击者用到的随机数。CSP与安全性质(3)协议主体的描述修改后的NSL1)AB:E(Kb:Na,A)2)BA:E(Ka:Na,Nb,B)3)AB:E(Kb:Nb)CSP与安全性质协议

20、主体A的进程USERa描述为：USERa=iUSERtrans.A!i!E(Ki:Na,A)rec.A.i?E(Ka:Na,x,i)trans.A!i!E(Ki:x)STOPUSERb=jUSERrec.B?j?E(Kb:y,j)trans.B!j!E(Kj:y,Nb,B)rec.B.j.E(Kb:Nb)STOPCSP与安全性质(4)CSP对NSL公钥协议的形式化分析步骤：1)建立安全协议的CSP模型。2)用CSP描述安全协议的安全性质。3)验证协议的安全性质是否满足。CSP与安全性质认证性的目标：如果在进程P中R的一些事件在T的一些事件之前发生，则T认证R，其中T，R为不相交的事件集合。T

21、authenticates R=trR=trT=对于进程P：P sat T authenticates R P|R|STOP sat trT=如果P满足T认证R且RR,那么P满足T authenticates RCSP与安全性质认证性在整个网络NET满足的条件为：C1:mINIT.I(m)C2:(mS.I(m)Sm I(m)C3:mT.I(m)C4:i.(USERi|R|STOP)msat maintains I)then NET|R|STOP sat trT=CSP与安全性质断言I：表示在一轮协议中，当集合R中的消息不能出现时(包括ENEMY)，有些主体(包括ENEMY)生成的所有消息是成

22、立的。C1、C2表明如果攻击者只知道满足I的消息，那么它只能生成满足I的消息。C3:对于T中的某些消息I是不成立的。C4:对于网络用户除非他们事先收到了一个消息，否则他们决不可能输出一个不满足I的消息。CSP与安全性质maintains I(tr)=(m(trrec):I(m)(m(trtrans):I(m)意义：如果在rec上收到的每一个消息满足I，那么在trans上输出的每一个消息也满足I。CSP与安全性质证明：rec.B.A.E(Kb:Nb)authenticates trans.A.B.E(Kb:Nb),为证明NSL的这条性质，首先构造一个适合的断言I。I(m)mUSERmTEXTmN

23、ONCE mNbmSECRET mSa mSbmPUBLICCSP与安全性质m:MESSAGE,k:PUBLICm=k(m)(k=kamNONCE.Nb.B)I(m):m:MESSAGE,k:SECRET.m=k(m)(k=Sa m E(Ka:NONCE.Nb.B)I(m)m1,m2,MESSAGE:m=m1.m2I(m1)I(m2)CSP与安全性质验证I是否满足所有条件。C1:根据协议的基本假设，显然I是满足C1的。C2：C2给出了生成关系与断言之间的交互性。M1:Sm Sk Sk(m).如果mS.I(m)那么根据归纳假设可得I(m)和I(k)。k有两种可能：公钥或者私钥。CSP与安全性质如

24、果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与安全性质RUSERa=USERa|trans.A.B.E(Kb:Nb)|STOP=iUSER trans.A!i!E(Ki:Na,A)rec.A.i?E(Ka:Na,x,i)STOP If i=b x=Nbt

25、rans.A!i!E(Ki:x)STOP if ib xNbCSP与安全性质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与安全性质(接上页)并且由于I(x)，有I(E(Ki:x)成立，故说明是满足的。同理

26、可完成对USERb的证明。最后，可以得出：NET satrec.B.A.E(Kb:Nb)authenticates trans.A.B.E(Kb:Nb)，说明修改后的NS协议其认证性是满足的。Model Checking1.概述2.消息空间3.Model Checking 协议模型4.基于CSP的模型检测工具FDR5.模型检测技术与逻辑推证技术的混合使用Model Checking概述给定一个模型M和逻辑描述的性质P，检查MP，即在模型M中性质P是否成立。Marrero等人通过检查在恶意攻击者存在的情况下，协议运行的所有可能的路径，可以判断协议是否满足了其安全保证。如果没有，将给出攻击者的攻击

27、路径。秘密性：运用模型检查器验证攻击者不可获得其不应获知的秘密。认证性：如果事件X发生了，那么事件Y必定在此之前已发生。Model Checking消息空间(1)密钥：(K-1:E(K:(m)=m(2)主体标识：公开(3)随机量：包含随机量的消息是新消息(4)正文若A代表原子消息空间，则消息集合M可定义为：若m1M,且m2M,(m1,m2)M若mM,且kA,则mkMModel Checking消息空间1)若mI,则Im。(包含)2)若Im1,且Im2,则I(m1,m2)。(复合)3)若I(m1,m2),则Im1,且 Im2。(投影)4)若Im,且 Ik,则IE(K:m)。(加密)5)若IE(K

28、:m)且IK-1,Im。(解密)Model Checking协议模型(1)主体表示为一个四元组:Nnames:主体的名字。P:过程描述，为执行动作的序列。IM：主体知道的消息集合。M是所有可能的消息集合。I是无限的且在加解密、复合和投影操作下是封闭的。B:vars(P)I:绑定集合,vars(P)是过程P中出现的变量的集合。Model Checking协议模型(2)协议的全局变量记为五元组,参与协议的主体和攻击者进程的结果。Ci,names X namesN计数器集合，用于记录主体A发起于主体B的协议轮数与B完成的对A响应的次数之差。若出现负值，则表明B已经完成了协议中对A的响应，但A并未参与

29、协议的运行。Model Checking协议模型 Cr,names X namesN计数器集合，用于记录主体A已经完成的对B响应的次数与完成的B发起的与A的协议轮数之差。若出现负值，则表明B已经完成了发起与A的一个协议，但A并未参与协议的运行。SsM,不会泄密的消息集合。如私钥集合。St M，协议运行时新产生的秘密消息集合，有可能被攻击者截获，例如会话密钥。Model Checking协议模型通信行为的执行引起的状态转换：(1)(s,SEND,m,s)(2)(s,REC,m,s)(3)(s,A,m,s)Model Checking协议模型(1)(s,SEND,m,s)一个主体发送消息m后，状态

30、由s转换到s，当且仅当：1)I=Im (攻击者可截获此消息)。2)主体的说明由i变为i,其中：i=i=且Ii=Iim。3)j=j(ji)Model Checking协议模型(2)(s,REC,m,s)一个主体接收消息m后，状态由s转换到s，当且仅当：1)mI (攻击者可生成此消息)。2)主体的说明由i变为i,其中：i=i=且Ii=Iim。3)j=j(ji)Model Checking协议模型(3)(s,A,m,s)一个主体完成用户定义的主体为消息m的行为A后,状态由s转换到s，当且仅当：1)主体的说明由i变为i,其中：i=Ni,A(msg).Pi,Ii,Bi)i=Ni,Pi,Ii,Bi)且m=

31、(msg)。2)j=j(ji)。Model Checking协议模型攻击者表示为=主体表示为：i=:绑定集合B从变量域到消息模式域增大的部分。参与协议的双方主体为达成双向认证，必须确保在通信中攻击者不能伪装成合法主体参与协议的运行。Model Checking协议模型协议发起者行为协议发起者行为协议响应方行为协议响应方行为BeginitBeginitBegRespondBegRespondEndinitEndinit EndRespond EndRespondModel Checking协议模型 Ci(A,B)=Beginit(A,B)EndRespond(B,A)Ci(A,B)0:正常。C

32、i(A,B)0:正常。Cr(A,B)0:表明A已经完成了发起与B的协议，但B并未参与协议的运行，暗示有非法攻击者冒充B的身份与A对话。Model Checking协议模型1)如果A发起一个与B通信的一轮协议，有：,那么Ci(A,B)+1 if Ci(A,B)is defined Ci(A,B)otherwise2)如果B完成了一次对A的响应，有：,那么Ci(A,B)-1 if Ci(A,B)0 errorotherwiseCr(A,B)=Cr(A,B)=Model Checking协议模型 3)如果B开始一个响应A的一轮协议，有：,那么Cr(A,B)+1 if Cr(A,B)is define

33、d Cr(A,B)otherwise 4)如果B完成了一次与A通信的发起，有：,那么Cr(A,B)-1 if Cr(A,B)0 errorotherwiseCr(A,B)=Model Checking协议模型协议路径是一条由全局状态和行为交替出现的序列，模型检测试图检查所有可能的路径。模型的一次执行对应一条有限的状态与行为交替出现的路径。使用report-error算法记录所有出错状态。Model Checking协议模型Proc DFS(global-state)Push(global-state,S)While(not empty(S)do =pop(S)if Ci(x,y)0 for s

34、ome x and y orCr(x,y)0 for some x and y orsIz for some sSs Stthen report-errorL=next-states()For each lL push(S,l)基于CSP的模型检测工具FDR1)理解协议中各主体进程、目标以及可能的假设等等。2)用形式化语言描述主体的行为、协议的安全目标，以及攻击者的初始知识库。3)用ModelChecking工具自动检查协议是否能满足给出的安全目标。4)如果Model-Checking工具输出攻击序列，则分析攻击的有效性。基于CSP的模型检测工具FDRNeedham Schroeder公开密钥

35、协议为A、B双方的双向认证的简化版本：1)AB:E(Kb:Na,A)2)BA:E(Ka:Na,Nb,B)3)AB:E(Kb:Nb)基于CSP的模型检测工具FDR FDR验证协议时，首先要刻画主体的行为。协议发起方开始认证协议的事件为I_running,完成认证协议的事件为I_commit;协议响应方开始协议的事件为R_running,完成协议的事件为R_commit,协议主体之间的通信事件为comm。基于CSP的模型检测工具FDRInitiator(a,na)=User.a?b I_running.a.bComm!Msg1.a.b.Encrypt.key(b).na.aComm.Msg2.b.

36、a.Encrypt.key(a).na.Nbif na=nathen comm.!Msg3.a.b.Encrypt.key(b).nbI_commit.a.bsession.a.bskipelse Stop基于CSP的模型检测工具FDR攻击者截获并试图解密消息一的进程：其中Ki 是攻击者I的公开密钥。Intercept.Msg1?a.b.Encrypt.k.n.aIf k=Ki then I(m1s,m2s,m3s,nsn)else I(m1sEncrypt.k.n.a,m2s,m3s,ns)基于CSP的模型检测工具FDR攻击者重放以前截获的消息(1)进程:fake.Msg1?a.b?m:m1

37、sI(m1s,m2s,m3s,ns)攻击者用得到的随机数n生成冒充消息(1)的消息：fake.Msg1?a.b!Encrypt?k?n:ns?aI(m1s,m2s,m3s,ns)基于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的模型检测工具FDRa.1)AT:A,T,Na,AkTb.1)T(A)B:A,B,Na,AKb

38、b.2)BT(A):B,A,Na,NbKaa.2)TA:T,A,Na,NbKaa.3)AT:A,T,NbkTb.3)T(A)B:A,B,NbKbBAN逻辑不能考虑主体同时参与过个协议进程的情况。模型检测与逻辑推证技术混合使用方法一方法一：首先运用逻辑推证工具对协议进行分析，如果发现了协议的漏洞以及导致此漏洞的关键性假设，则运用模型检测工具有针对地为关键性假设构造可能的现实攻击路径。协议关键性假设可能涉及的内容有：关于主体行为的假设关于重要消息的假设模型检测与逻辑推证技术混合使用方法一Case1:如果协议主体P的行为是可信的，则用攻击者不诚实主体身份取代主体P的地位与其他诚实主体依协议进行额外的

39、会话，用模型检测工具分析此会话并找出可能的攻击路径。Case2：如果对方通信主体的行为是可信的，则用攻击者不诚实主体身份取代对方主体的地位与主体P依协议规则进行额外的会话，用模型检测工具分析此会话并找出可能的攻击路径。模型检测与逻辑推证技术混合使用方法一Case 3：如果协议主体相信某一重要消息，则用模型检测技术检测攻击者是否能够再生成此消息，或将此消息说明为一个不安全状态，运用模型检测工具检查此状态是否可达。模型检测与逻辑推证技术混合使用方法二方法二：首先运用模型检测工具对协议进行分析，如果发现协议是不安全的，则使用逻辑推证工具去判断协议的哪一个假设是导致协议遭受现实攻击的原因。模型检测与逻

40、辑推证技术混合使用方法二1）先用逻辑推证工具将找到的攻击路径说明为一个协议，其中攻击者作为参与协议运行的主体。2）说明此协议应满足的安全目标，如秘密性，认证性等。3）根据推理规则和公理以及协议欲达成的目标对协议中的主体增加相应的假设条件，使得构造的协议是安全的。4）分析所提出的额外的假设，并由此发现导致协议错误的关键性假设。模型检测与逻辑推证技术混合使用方法二协议11)AB:Mka2)BA:Mkakb3)AB:Mkb协议21)AS:A,Ta,B,Kabkas2)SB:Ts,A,Kabkbs模型检测工具对协议的分析对协议1的分析诚实主体：A 和 B。攻击者：Z攻击者知识集合：KS协议应满足的安全

41、性为：秘密性 MKS模型检测工具对协议的分析经自动检测工具发现协议1违反了秘密性：1)AZ(B):MKa2)Z(B)A:MKa3)AZ(B):M 认证性：模型检测工具未能发现协议1可能的认证缺陷。模型检测工具对协议的分析对协议2的分析认证性：对于协议一轮的运行，认证的性质是成立的。但如果A、B皆发起多个会话，认证性将不成立。攻击为：1)AS:A,Ta,B,Kabkas2)SB:Ts,A,Kabkbs1)Z(B)S:B,Ts,A,Kabkbs2)SZ(A):Ts,B,Kabkas模型检测工具对协议的分析1”)Z(A)S:A,Ts,B,Kabkas2”)SZ(B):Ts”,A,Kabkbs1”中的

42、Ts有问题，本应为Ta。秘密性：kabKS在协议认证性被破坏后，存在一个攻击破坏协议的秘密性，描述为：1)AZ(S):A,Ts,B,Kab2)Z(S)B:Ts”,A,Kabkbs逻辑推证工具对协议的分析协议1不能提供认证的缺陷。协议1的安全目标是：A，B双方都相信对方已拥有了M。由于没有任何签名和预共享的秘密，所以协议的目标是不能达到的。如果基于以下两个假设,通过逻辑推证其秘密性是成立的。Believes(A,maysee(B,M)Believes(B,maysee(A,M)但实际上，通过前面的证明可知协议1的秘密性是不成立的。原因为认证的缺乏和双层加密造成的。而一般的逻辑推证工具的推理规则

43、不能判断由双层加密造成的秘密性缺陷。逻辑推证工具对协议的分析协议2是一个密钥交换协议，其信仰目标是：G1:believes(A,goodkey(A,Kab,B)G2:believes(B,goodkey(A,Kab,B)G3:believes(A,believes(B,goodkey(A,Kab,B)G4:believes(B,believes(A,goodkey(A,Kab,B)逻辑推证工具对协议的分析协议的基本假设为：A1:believes(A,goodkey(A,kas,S)A2:believes(B,goodkey(B,kas,S)A3:believes(A,fresh(Ta)A4:b

44、elieves(S,fresh(Ts)A1:believes(S,controls(A,Kab)逻辑推证工具对协议的分析推证过程略。由假设A1,A2以及可信服务器的权限,可证明协议的G1,G2 是满足的。但由于协议没有认证体系,S无法判断接收到的消息的确发自A以及B的确为消息的意定接收者，同理对于A,B也无法判断S的可信性，因此G3,G4是不满足的。即A、B不能得到有关对方主体相信Kab是良好的共享密钥的信仰。混合分析技术对协议的分析ML:分析协议11.运用模型检测工具对协议进行分析,若不安全,则：2.使用逻辑推证工具去判断协议的哪一个假设是导致协议遭受现实攻击的原因。LM:分析协议21.运用

45、逻辑推证工具对协议进行分析，发现协议有漏洞以及导致此漏洞的关键性假设，则2.运用模型检测工具有针对地为关键性假设构造可能的攻击路径。混合分析技术ML对协议1的分析首先用逻辑推证工具发现协议1不能提供认证的缺陷。协议1的安全目标是：A,B双方都相信对方已拥有了M。将Z取代B，将攻击模型化为3条消息的协议。1)AZ:Mka2)ZA:Mka3)AZ:M混合分析技术ML对协议1的分析下面假设对于协议满足其安全目标是必须的：Believes(Z,maysee(A,M)Believes(A,maysee(Z,M)由于该协议没有认证功能，因此并不能肯定M是被意定的主体接收的信仰。所以很有可能M为攻击者获取，因此混合分析技术LM对协议2的分析为达到安全目标就必须修改协议或者允许服务器S使用不正确的推理规则，以及为满足安全性质，需要增加额外的假设Believes(S,fresh(Ta)让攻击者Z扮演S的角色，通过模型检测工具进行自动检测可得到一个前述的对协议秘密性的攻击。结论：认证性的缺乏将导致对消息的不恰当的解释以及不恰当的假设可引发Z对协议秘密性的攻击。混合分析技术分析对照表协议协议2协议协议1 模型检测模型检测逻辑推证逻辑推证混合分析混合分析ML LM认证性秘密性表示发现了漏洞问题未发现

展开阅读全文