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

安全协议理论与方法安全协议安全协议理论与方法安全协议2.1 安全协议概述各种攻击黑客利用安全协议本身的缺陷进行攻击重设计面向具体应用基于经验和软件测试来保证安全性 对现有协议改进和优化2.1 安全协议概述各种攻击安全协议的概念定义：协议是两个或两个以上的参与者采取一系列步骤以完成某项特定的任务。安全协议是密码体制基础上的一种高互通协议。协议至少需要两个参与者。在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤。通过执行协议必须能够完成某项任务，或达成某种共识。安全协议的概念定义：协议是两个或两个以上的参与者采取一系列步安全协议常见类型密钥交换协议：用于完成会话密钥的建立。认证协议：实体、身份、数据源(目)、消息。用来防止篡改、假冒、否认等攻击。认证和密钥交换协议：IKE、DASS、Kerberos等。电子商务协议：由于协议双方利益矛盾，因此需要保证公平，如SET。安全协议常见类型安全协议系统模型环境定义系统环境：消息的发送和接收者、攻击者(恶意网络环境)、管理消息发送和接收的规则。恶意网络环境：攻击者攻击者操作：截取、重放、篡改、级联、分离、加密和解密。被动攻击者：知道信息。主动攻击者：操纵信息。安全协议系统模型环境定义系统环境：消息的发送和接收者、攻安全协议系统模型安全协议系统模型攻击行为攻击行为转发消息到其意定接收者处。延迟消息的送达。将消息篡改后转发。将消息与以前接收的消息合并。改变部分或全部消息的去处。重放消息。安全协议系统模型攻击行为安全协议系统模型安全协议系统模型-示意图示意图诚实主体诚实主体诚实主体诚实主体环境/攻击者安全协议系统模型-示意图诚实主体诚实主体诚实主体诚实主体环安全协议的性质及实现安全协议的性质及实现目标：保证下面安全性质在协议执行完毕时能够得 以实现。认证性-关键性质 机密性 完整性 不可否认性安全协议的性质及实现目标：保证下面安全性质在协议执行完毕时能认证性实现认证性实现通过共享秘密实现，例如：加密的密钥。声称者使用仅为其与验证者知道的密钥封装消息，如果验证者能够成功地解密消息或验证封装是正确的，则证毕。声称者使用私钥对消息签名，验证者使用声称者的公钥验证签名，如正确，证毕。声称者通过可信第三方来证明自己。用途：对抗假冒攻击，确保身份，从而获取对某人或某事的信任。认证性实现通过共享秘密实现，例如：加密的密钥。秘密性实现秘密性实现目的：保护协议消息不被泄漏非授权拥有此消息的人，即使是攻击者观测到了消息的格式，它也无法从中得到消息的内容或提炼出有用的消息。实现方法之一：对消息明文加密。秘密性实现目的：保护协议消息不被泄漏非授权拥有此消息的人，完整性实现完整性实现应用：保护协议消息不被非法篡改、删除和替代。常用方法：封装和签名。即用加密的方法或者Hash函数产生一个明文的摘要附在传送的消息上，作为验证消息完整性的依据，称为完整性校验值(ICV)。关键问题：通信双方必须事先达成有关算法的选择等诸项的共识。完整性实现应用：保护协议消息不被非法篡改、删除和替代。不可否认性实现目的：通过通信主体提供对方参与协议交换的证据来保证其合法利益不受侵害。收集证据，以便事后能够向可信仲裁证明对方主体的确发送或接收了消息。证据实现：签名消息的形式。协议特点：证据的正确性，交易的公平性。次要性质：适时中止性、可追究性等。不可否认性实现目的：通过通信主体提供对方参与协议交换的证据协议设计准则缺陷来源:设计不规范和具体执行时产生。消息独立完整性原则消息前提准确原则主体身份标识原则加密目的原则原则签名原则随机数的使用原则时戳的使用原则编码原则协议设计准则缺陷来源:设计不规范和具体执行时产生。消息独立完整性原则一条消息的解释应完全由其内容来决定，而不必借助于上下文来推断。发送者标识接收者标识：消息 AB:m m应包含A，B的标识，否则易造成攻击。消息独立完整性原则消息前提准确原则与消息的执行相关的先决前提条件应当明确指出，并且其正确性与合理性能够得到验证，由此可判断出此消息是否应当接收。解释:每条消息所基于的假设是否能够成立?消息前提准确原则主体身份标识原则主体标识重要时在消息中明确附上主体名称显式：主体的名字以明文形式出现。隐式：采用加密或签名技术，需要从消息格式中推知消息所属主体的身份。主体身份标识原则主体标识重要时在消息中明确附上主体名称加密目的原则加密可实现多种安全目的：秘密性、完整性、认证性在协议中使用加密算法时，要事先确定什么目的并能够保证某种安全性的实现。加密目的原则加密可实现多种安全目的：签名原则主体对加密消息签名时，并不表明主体知道加密消息的内容。如果主体对一个消息签名后再加密，则表明主体知道消息的内容。同时使用加密与签名时，应该先签名后加密。签名原则主体对加密消息签名时，并不表明主体知道加密消息的内随机数的使用原则作用：在协议中使用随机数时，应明确其所起的作用和属性，它的目的是提供消息的新鲜性。关键问题：随机数的真正随机性。随机数的使用原则时戳的使用原则原则：使用时戳时，要考虑各个机器的时钟与当地标准时间的差异，这种差异不能影响到协议执行有效性。时戳的使用主要依赖于时钟的同步。时戳的使用原则编码原则明确指出具体的编码格式编码是与协议的安全性相关。编码原则安全协议缺陷分类 基本协议缺陷 口令/密钥猜测缺陷 陈旧消息缺陷 并行会话缺陷 内部协议缺陷 密码系统缺陷安全协议缺陷分类 基本协议缺陷基本协议缺陷设计时没有考虑或很少考虑攻击者攻击而引发的协议缺陷。实例：对消息先加密后签名就有漏洞，因为签名者并不一定知道被加密的消息内容，而且签名者的公钥是公开的。使攻击者通过用他自己的签名替换原有的签名来伪装成发送者。基本协议缺陷口令/密钥猜测缺陷可检测的口令在线猜测攻击：不成功的登录能被检测并被认证服务器记录(以便限定次数)。不可检测的口令在线猜测攻击：攻击者从认证服务器的响应中逐渐推导出正确的口令。可离线的口令猜测攻击：攻击者使用认证协议消息复件，猜测口令并离线验证。改进的措施：认证服务器只响应新鲜的请求。认证服务器只响应可验证的真实性。口令/密钥猜测缺陷可检测的口令在线猜测攻击：不成功的登录能其他几种缺陷陈旧消息缺陷：在协议设计中没有对消息的新鲜性充分考虑。从而存在消息重放攻击。并行会话缺陷：攻击者通过交换一定的协议消息获得重要的消息。内部协议缺陷：协议的参与者中至少有一方不能够完成所有必需的动作而导致缺陷。密码系统缺陷：协议中使用的密码算法的安全强度有问题，导致协议不能满足所要求的机密性、认证等需求而产生的缺陷。其他几种缺陷陈旧消息缺陷：在协议设计中没有对消息的新鲜性充消息重放攻击及对策消息重放攻击对策序列号机制时戳机制挑战-应答机制消息重放攻击及对策消息重放攻击消息重放攻击攻击者利用其消息再生能力生成诚实用户所期望的消息格式并重放，从而达到破坏协议安全性质的目的。类别：本协议的轮内攻击和轮外攻击。轮内攻击消息重放攻击攻击者利用其消息再生能力生成诚实用户所期望的消影响消息去向的攻击偏转攻击：将消息返还给发方-反射攻击非协议的双方-第三方攻击直接攻击-意定的接收方，但被延迟影响消息去向的攻击偏转攻击：诚实主体收到的重放消息类型本轮内的消息重放无重叠轮外消息的重放有重叠轮外消息的重放延迟的消息诚实主体收到的重放消息类型对策-序列号(挑战-应答)序列号机制接收方通过比较消息中的序列号以判断消息是新产生的还是重放的。问题:开销增大,适用系统中成员较少的情况。挑战-应答机制-消息的时间变量参数由接收方在该消息传递前明确地向消息发送方说明。问题：系统开销增加.对策-序列号(挑战-应答)序列号机制接收方通过比较消对策-时戳机制消息的新旧是由消息上盖的时戳决定的，只有当消息上的时戳与当前本地时间的差值在一定范围内，接收方才接收这个消息。问题：需要全局时钟，但仍难以同步。1)如果验证者弄错了当前的时间，那么旧消息就能被很容易地重放。2)如果合法声称者弄错当前时间,有可能被利用在合理的时间点接收验证者重放产生的认证请求。3)如果双方的时钟都有较大的偏差，则双方都会被攻击者利用。对策-时戳机制消息的新旧是由消息上盖的时戳决定的，只有安全协议及其受到攻击的实例A,B,:表示参与协议的主体。Kij:主体i，j共享的会话密钥。Ki：主体i的公钥，Ki-1：主体i的私钥。Ri：主体i生成的随机数，Ni：主体i生成的序列号。Ti：主体i生成的时戳。m1|m2:表示消息 的级联 E(k:m):表示用密钥K对消息m加密。Text1,Text2,:为消息常量。fKab(X):表示用Kab加密的Hash函数。Z:表示攻击者。安全协议及其受到攻击的实例A,B,:表示参与协议的主体无可信第三方参与的对称密钥协议ISO one-pass 单方对称密钥认证协议 1)AB:Text2,E(Kab:Ta|Na,B,Text1)ISO two-pass 单方对称密钥认证协议 1)BA:Rb,Text12)AB:Text3,E(Kab:Rb,B,Text2)无可信第三方参与的对称密钥协议ISO one-pass 无可信第三方参与的对称密钥协议ISO two-pass 双方对称密钥认证协议 1)AB:Text2,E(Kab:Ta|Na,B,Text1)2)BA:Text4,E(Kab:Tb|Nb,A,Text3)ISO three-pass 双方对称密钥认证协议1)BA:Rb,Text12)AB:Text3,E(Kab:Ra,Rb,B,Text2)3)BA:Text5,E(Kab:Rb,Ra,Text4)无可信第三方参与的对称密钥协议ISO two-pass 无可信第三方参与的对称密钥协议使用单向函数1)BA:B,Rb2)AB:A,E(Kab:f(Rb),Ra,A,K)3)BA:B,E(K:f(Ra)使用f(Rb)和f(Ra)单向函数验证消息的正确性。无可信第三方参与的对称密钥协议使用单向函数无可信第三方参与的对称密钥协议 RFC 协议1)AB:A,E(Kab:Na)2)BA:E(Kab:Na+1,Nb)3)AB:E(Kab:Nb+1)4)BA:E(Kab:Kab,Nb)有缺陷，例如第4步易被 E(Kab:Na+1,Nb)重放替代，并且A不能觉察。无可信第三方参与的对称密钥协议 RFC 协议RFC协议的修改 将前述协议的2)3)4)修改为：1)AB:A,Na2)BA:E(Kab:Na,Kab)3)AB:A,E(Kab:Na)4)BA:Nb问题:仍有缺陷，因为存在多重会话攻击。RFC协议的修改 将前述协议的2)3)4)修改为：多重会话攻击1)AZ(B):A,Na1)Z(B)A:B,Na (Z假冒B向A发连接)2)AZ(B):E(Kab:Na,Kab)(A应答Z的请求)2)Z(B)A:E(Kab:Na,Kab)(Z重放A应答Z的消息给A)3)AZ(B):A,E(Kab:Na)(A回应Z)3)Z(B)A:A,E(Kab:Na)4)Z(B)A:Ni4)AZ(B):Na多重会话攻击AZ(B):A,Na多重会话攻击分列表示1)AZ(B):A,Na 1)Z(B)A:B,Na 2)AZ(B):E(Kab:Na,Kab)2)Z(B)A:E(Kab:Na,Kab)3)AZ(B):A,E(Kab:Na)3)Z(B)A:A,E(Kab:Na)4)Z(B)A:Ni 4)AZ(B):Na多重会话攻击分列表示AZ(B):A,Na有可信第三方参与的对称密钥协议1.Needham-Schroeder私钥协议1)AS:A,B,Na2)SA:E(Kas:Na,B,Kab,E(Kbs:Kab,A)3)AB:E(Kbs:Kab,A)4)BA:E(Kab:Nb)5)AB:E(Kab:Nb-1)问题:消息3新鲜性无法保证,可用类似旧消息重放。若使用流密码则消息4和5差别很小,易被攻击。有可信第三方参与的对称密钥协议1.Needham-Schr缺陷分析若在给定的时间内E(Kbs:Kab,A)中的旧密钥Kab被解密，则该协议存在如下的问题：由于消息3)中没有新鲜性标记，因此攻击者重放一个以前A发给B的报文。Z(A)B:E(Kbs:Kab,A)B以为A发来的新消息。由于此处的Kab已被解密,因此所有用Kab加密的消息都不保密。缺陷分析若在给定的时间内E(Kbs:Kab,A)中的旧密钥NS-无需获得会话密钥的攻击针对Needham-Schroeder协议的另类攻击1)AS:A,B,Na2)SA:E(Kas:Na,B,Kab,E(Kbs:Kab,A)3)AB(Z):E(Kbs:Kab,A)4)Z(B)A:Nz /与E(Kab:Nb)格式相同5)AB(Z):E(Kab:(E(Kab:Nz)-1)-1)此时，A认为主体B已经知道了会话密钥Kab,但B实际上并没有参与协议的执行过程。NS-无需获得会话密钥的攻击针对Needham-Schro1.修订的Needham Schroeder协议1)AB:A2)BA:E(Kbs:A,Nb)3)AS:A,B,Na,E(Kbs:A,Nb)4)SA:E(Kas:Na,B,Kab,E(Kbs:Kab,Nb,A)5)AB:E(Kbs:Kab,Nb,A)6)BA:E(Kab:Nb)7)AB:E(Kab:Nb-1)该协议见Boyd90,任有漏洞。1.修订的Needham Schroeder协议AB2.Denning Sacco 协议针对前述协议缺点,提出采用时戳方法来解决上述NS协议中出现的新鲜性问题。1)AS:A,B2)SA:Certa,Certb3)AB:Certa,Certb,E(Kb:E(Ka-1:Kab,T)消息3的双重加密用于保证消息的秘密性和认证性,但当B收到此消息时,并不能确定这条消息是发给它的。2.Denning Sacco 协议针对前述协议缺点,提Denning Sacco 协议的攻击用户Z通过协议正常执行得到A发的消息3):3)AZ:Certa,Certz,E(Kz:E(Ka-1:Kaz,T)之后,Z将外层密文解密,利用前两条消息从S处得到主体B的公钥Kb,此后,Z可伪装成A,进行下面消息的传递:3)AB:Certa,Certb,E(Kb:E(Ka-1:Kai,T)使B误认为与A的会话密钥为Kai，原因在于消息3)中没有显式或隐式地给出B身份标识。Denning Sacco 协议的攻击用户Z通过协议正常执3.Otway-Rees有漏洞的协议1)AB:M,A,B,E(Kas:Na,M,A,B)2)BS:M,A,B,E(Kas:Na,M,A,B),E(Kbs:Nb,M,A,B)3)SB:M,E(Kas:Na,Kab),E(Kbs:Nb,Kab)4)BA:M,E(Kas:Na,Kab)M是协议轮标识符,消息2)中S解密检查两个消息中的M,A,B是否一致,如果一致,S就生成新密钥Kab发给B。3.Otway-Rees有漏洞的协议1)AB:M,A,B3.Otway-Rees协议攻击例1)AZ(B):M,A,B,E(Kas:Na,M,A,B)4)Z(B)A:M,E(Kas:Na,M,A,B)主体A会误将M,A,B视为新密钥，它是典型的类型缺陷例子。另种攻击:等待消息2)的发送,之后将适当的部分重放给A和B,之后监视A、B间的会话。3.Otway-Rees协议攻击例1)AZ(B):M,A5.大嘴青蛙协议1)AS:A,E(Kas:Ta,B,Kab)2)SB:E(Kbs:Ts,A,Kab)攻击1:在有效时间窗口内重放消息1),由于S将产生附有一个更新的时戳的一个新的消息2)而造成重认证。攻击2:将会话记录下来,之后不断将S当作一个中转站直到它试图造成A、B之间的重认证。5.大嘴青蛙协议AS:A,E(Kas:Ta,B,K大嘴青蛙协议攻击例1)AS:A,E(Kas:Ta,B,Kab)2)SB:E(Kbs:Ts,A,Kab)1)Z(B)S:B,E(Kbs:Ts,A,Kab)2)SZ(A):E(Kas:Ts,B,Kab)1)Z(A)S:A,E(Kas:Ts,B,Kab)2)SZ(B):E(Kbs:Ts,A,Kab)此时,Z能够重放A、B之间的消息1)AZ(S):A,E(Kas:Ts,B,Kab)2)Z(S)B:E(Kbs:Ts,A,Kab)大嘴青蛙协议攻击例AS:A,E(Kas:Ta,B,K6.Yahalom 协议1)AB:A,Na2)BS:B,E(Kbs:A,Na,Nb)3)SA:E(Kas:B,Kab,Na,Nb),E(Kbs:A,Kab)4)AB:E(Kbs:A,Kab),E(Kab:Nb)6.Yahalom 协议Yahalom协议攻击例1)Z(A)B:A,Na2)BZ(S):B,E(Kbs:A,Na,Nb)3)SA:E(Kas:B,Kab,Na,Nb),E(Kbs:A,Kab)4)Z(A)B:E(Kbs:A,Na,Nb),E(Na,Nb:Nb)B会将Na,Nb当作Kab，因此造成协议执行的缺陷。Yahalom协议攻击例Z(A)B:A,NaNeedham-Schroeder签名协议1)AS:A,E(Kas:CS)/CS为Message的摘要2)SA:B,E(Kss:A,CS)3)AB:Message,E(Kss:A,CS)4)BS:B,E(Kss:A,CS)5)SB:E(Kbs:A,CS)主体A通过发送消息给B并保证消息的原发性和完整性。Needham-Schroeder签名协议AS:A,E(Kerberos V51)CA:U,G,L1,N12)AC:U,Tcg,E(Ku:G,Kcg,Tstart,Texpire,N1)3)CG:S,L2,N2,Tcg,Acg4)GC:U,Tcs,E(Kcg:S,Kcs,Tstart,Texpire,N2)5)CS:Tcs,Acs6)SC:E(Kcs:T)其中Acs=E(Kcs:C,T)Kerberos V5CA:U,G,L1,N1其他协议 Carlson SKI协议 ISO四向认证协议 ISO五向认证协议 Woo&Lam 认证协议 Woo&Lam 相互认证协议 Neuman Stubblebine协议其他协议 Carlson SKI协议 无可信第三方参与的公钥协议1.ISO one-pass 单方公钥认证协议AB:CertA,Ta|Na,B,Text2,E(Ka-1:Ta|Na,B,Text1)2.ISO two-pass 单方公钥认证协议1)BA:Rb,Text12)AB:CertA,Ra,Rb,B,Text3,E(Ka-1:Ra,Rb,B,Text2)无可信第三方参与的公钥协议1.ISO one-pas 无可信第三方参与的公钥协议3.ISO two-pass双方公钥认证协议AB:CertA,Ta|Na,B,Text2,E(Ka-1:Ta|Na,B,Text1)BA:CertB,Tb|Nb,A,Text4,E(Kb-1:Tb|Nb,A,Text3)4.ISO three-pass 双方公钥认证协议1)BA:Rb,Text12)AB:CertA,Ra,Rb,B,Text3,E(Ka-1:Ra,Rb,B,Text2)3)BA:CertB,Rb,Ra,A,Text5,E(Ka-1:Rb,Ra,A,Text4)无可信第三方参与的公钥协议3.ISO two-pasDiffie-Hellman协议1)AB:X=Gxmod N2)BA:Y=Gymod N G,N是通信主体A、B的共识。协议执行完成后，双方计算得到新的密钥K=GXY mod N，它提供密钥交换的方法，但不提供认证，需要与认证协议结合使用。Diffie-Hellman协议AB:X=Gxmod station-to-station协议1)AB:A,B,ax2)BA:B,A,ay,E(K:(ayax)3)AB:A,B,E(K:(axay)它是建立在Diffie-Hellman密钥交换基础上的双向认证协议。station-to-station协议station-to-station协议的攻击1)AZ(B):A,B,ax 1)ZB:Z,B,ax 2)BZ:B,Z,ay,E(K:(ayax)2)Z(B)A:B,A,ay,E(K:(ayax)3)AZ(B):A,B,E(K:(axay)3)ZB:Z,B,E(K:(axay)station-to-station协议的攻击AZ(B):station-to-station协议攻击解释A发送指数aX 试图开始一轮与B的协议,此消息被Z截获。Z发起另一轮协议重放此消息。B回应指数aY以及加密的指数积,Z将此消息转发给A。A收到此消息确认是在与其通信，而实际上是与通信，根本不知道的存在，攻击的危害在于持有错误的信仰。修改：1)AB:A,B,ax2)BA:B,A,ay,E(K:(，ayax)3)AB:A,B,E(K:(，axay)station-to-station协议攻击解释A发送指数有可信第三方参与的公钥协议 Needham-Schroeder公钥协议1)AS:A,B2)SA:E(Ks-1:Kb,B)3)AB:E(Kb:Na,A)4)BS:B,A5)SB:E(Ks-1:Ka,A)6)BA:E(Ka:Na,Nb)7)AB:E(Kb:Nb)有可信第三方参与的公钥协议 Needham-SchroedLowe发现的对此协议的攻击3)AZ:E(Kz:Na,A)/Z冒充A3)Z(A)B:E(Kb:Na,A)6)ZA:E(Ka:Na,Nb)7)AZ:E(Kz:Nb)7)Z(A)B:E(Kb:Nb)危害:AB没有直接通信,而B以为是与A通信。Lowe的修改 6)BA:E(Ka:Na,Nb,B)Lowe发现的对此协议的攻击AZ:EDenning Sacco密钥分配协议1)AS:A,B2)SA:Certa,Certb3)AB:Certa,Certb,E(Kb:E(Ka-1:Kab,Ta)协议的目的在于安全地将由A生成的会话密钥Kab传递给B,S为A,B提供证书。Certa=E(Ks-1:A,Ka,T)是由S签发的A的证书。Denning Sacco密钥分配协议AS:A,BDenning Sacco密钥分配协议攻击如果B不诚实，它在获得A的证书后,可以冒充A给C发信息，使得C以为A与其共享密钥Kab,将会导致危险发生。1)BS:B,C2)SB:Certb,Certc3)B(A)C:Certa,Certc,E(Kc:E(Ka-1:Kab,T)Denning Sacco密钥分配协议攻击如果B不诚实，它其他协议SPLICE/AS 认证协议Denning Sacco密钥分配协议SRA three-pass协议Gong双方认证协议加密的密钥交换协议其他协议SPLICE/AS 认证协议安全协议的形式化分析目前的技术主要用于对密钥正确的认证安全协议的形式化分析有助于减轻协议设计者的部分工作量：.界定安全协议的边界,即协议系统与其运行环境的界面。更准确地描述安全协议的行为。更准确地定义安全协议的特性。证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。安全协议的形式化分析目前的技术主要用于对密钥正确的认证安全协议形式化分析的历史与现状最早提出对安全协议形式化分析思想的是Needham和SchroederNESC78。NESC78 R.M.Needham and M.D.Schroeder，Using encryption for authentications of large networks of computers.Communications of the ACM,21(12),993-999,1978真正在此领域做出工作的为Dolev和YaoDOYA83。DOYA83 D.Dolev.And A.Yao.On the security of public key protocols.IEEE Transactions on Information Theory.29(2):198-208,Mar 19831989年,Burrows,Abadi和Needham提出了BAN逻辑。安全协议形式化分析的历史与现状最早提出对安全协议形式化分析安全协议形式化分析的历史与现状以BAN逻辑代表的基于推理结构性方法。推广应用如GNY逻辑，基于攻击结构性方法。研究热点，大量一般目的的形式化方法被用于这一领域。基于证明结构性方法。安全协议形式化分析的历史与现状以BAN逻辑代表的基于推理结有关问题open-ended协议:协议使用的数据结构固定。只有协议并行执行的数目和攻击者为创建一个消息而执行的操作数不受限制。拒绝服务:指攻击者开始一个协议之后就放弃，造成合法的协议请求不能接受。匿名通信:防止“旁观者”了解信息来源和去向。高逼真度:可合成性:同意环境下,多个协议同时执行。一个协议的消息是否会破坏其他协议的安全目标。有关问题open-ended协议:协议使用的数据结构固定。活跃研究团体美国空军研究实验室:Meadows代表。英国London学院:Schneider代表。英国Oxford学院:Roscoe代表。美国Carnegie Mellon学院:Milen代表。AT&T实验室:Stubblebine代表。活跃研究团体美国空军研究实验室:Meadows代表。相关问题-局限性对安全协议的分析或推证往往是基于环境某些假设之上的，只有当假设成立时，证明才成立。一旦某种假设不成立，一切的证明无效。一些关键性的假设，只要攻击者违反了他们，仍可成功入侵系统。安全特性对不同的要求侧重点不一样，甚至矛盾。例如匿名性和可追究性是冲突的。相关问题-局限性对安全协议的分析或推证往往是基于环境某形式化法进一步解决的问题扩展现有的形式化分析工具的能力,不仅能证明是不安全的,还能证明是安全的。为现有形式化语言构造完善的数学描述,并进行严谨的理论证明,形成统一的形式语言描述,以描述可利用的必要信息,并使之能应用于一些新的应用协议的分析中。将形式化方法应用于协议说明与设计阶段，从而可以极小的代价尽可能早地发现错误。形式化法进一步解决的问题扩展现有的形式化分析工具的能力,不