第十五章安全协议形式化分析ppt课件.ppt

2022/11/22,1,第十五章 安全协议的形式化分析技术,2022/11/22,2,逻辑推理及形式化语言,逻辑推理形式化语言形式化分析方法形式化分析方法应用,2022/11/22,3,逻辑推理,逻辑推理 由前提推出结论。前提和结论都是命题。 命题的真或假由命题的内容是否符合客观实际确定。演绎逻辑 当前提的“真”蕴涵结论的“真”，称前提和结论之间有可推导性关系。即前提和结论之间的推理是正确的。 研究怎样的前提和结论之间具有可推导性关系。归纳逻辑 只要求得到的结论本身是协调的，与前提是协调的。 前提的“真”并不蕴涵结论的“真”。,2022/11/22,4,逻辑推理,逻辑推理的正确性命题的内容：“真”/“假”，内容决定命题的“真”/“假”。命题的形式：即逻辑形式。由内容抽象出来。逻辑形式决定前提和结论的之间的可推导性关系。不关心前提和结论的真假，而关注前提的真是否蕴涵结论的真。,2022/11/22,5,形式化语言,形式语言使用自然语言陈述并分析命题常常引出歧义。需要构造一种符号语言形式语言，描述由命题内容抽象出来的命题逻辑形式。形式语言使用符号来构造公式由公式来精确地表示命题的逻辑形式语义和语法语义涉及符号和符号表达式的涵义(给符号某种解释)语法涉及符号表达式的形式结构，但不考虑任何对形式语言的解释。形式语言的语义和语法既有联系，又有区分。,2022/11/22,6,形式化分析方法,集合论数理逻辑图论：有限状态图网论：Petri网模型代数系统：代数系统形式化模型,2022/11/22,7,安全协议, 安全协议的基本概念安全协议特指使用密码学技术的密码协议所谓协议，就是两个或者两个以上的参与者为完成某项特定的任务而采取的一系列步骤。 协议的定义包含三层含义：1. 协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之前，后面的步骤不可能执行；在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤。2. 协议至少需要两个参与者；一个人可以执行一系列的步骤来完成一项任务，但它不构成协议。3. 通过协议必须能够完成某项任务。 安全协议使用密码学技术，协议参与者可能是可以信任的人，也可能是攻击者和完全不信任的人。密码协议包含某种密码算法。,2022/11/22,8,安全协议,网络通信中常用的密码协议按照其完成的功能分成以下四类： 密钥交换协议在参与协议的两个或者多个实体之间建立共享的秘密通道，常用于建立在一次通信中所使用的会话密钥。协议可以采用对称密码体制，也可以采用非对称密码体制，例如Diffie-Hellman密钥交换协议。认证协议认证协议中包括实体认证（身份认证）协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。认证和密钥交换协议协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。常见的有Needham-Schroeder协议、分布认证安全服务（DASS）协议、ITU-T X.509认证协议等等。电子商务协议电子商务协议中，主体利益目标往往是不一致的，电子商务协议关注的就是公平性，即协议应保证交易双方都不能通过损害对方利益而得到它不应得的利益。常见的电子商务协议有SET协议等。,2022/11/22,9,DH算法描述,Alice与ob确定两个大素数n和g，这两个整数不保密， Alice与ob 可以使用不安全信道确定这两个数Alice选择另一个大随机数x，并计算A如下： A=gx mod nAlice将发给obob选择另一个大随机数y，并计算B如下： B=gy mod nob将发给Alice计算秘密密钥K1如下： K1=Bx mod n计算秘密密钥K2如下： K2=Ay mod n,2022/11/22,10,SSL/TLS协议栈,介于应用层和传输层之间为上层提供安全性,IP,SSL ChangeCipher SpecProtocol,SSL AlertProtocol,Application Protocol,TCP,SSL RecordProtocol,SSL HandshakeProtocol,HTTP,LDAP,IMAP,2022/11/22,11,SSL/TLS概况,协议分为两层上层：TLS握手协议、TLS密码变化协议、TLS警告协议底层：TLS记录协议上层协议是用于管理SSL密钥信息的交换，下层提供基本的安全服务TLS握手协议客户和服务器之间相互认证协商加密算法和密钥它提供连接安全性，有三个特点身份认证，至少对一方实现认证，也可以是双向认证协商得到的共享密钥是安全的，中间人不能够知道协商过程是可靠的TLS记录协议建立在可靠的传输协议(如TCP)之上它提供连接安全性，有两个特点保密性，使用了对称加密算法完整性，使用HMAC算法用来封装高层的协议,2022/11/22,12,SET协议目标,信息在Internet上的安全传输，保证网上传输的数据不被黑客窃听订单信息和个人账号信息的隔离，在将包括消费者账号信息的订单送到商家时，商家只能看到订货信息，而看不到消费者的账户信息 消费者和商家的相互认证，以确定通信双方的身份，一般由第三方机构负责为在线通信双方提供信用担保要求软件遵循相同的协议和消息格式，使不同厂家开发的软件具有兼容和互操作功能，并且可以运行在不同的硬件和操作系统平台上,2022/11/22,13,Card Holder,How SET with Credit Card Works,Merchant Server,Acquiring Bank,Card Issuer Bank,8,7,6,5,4,3,2,1,9,CA,Certificate Authority,0,0,- cardholder registration,1,3,2,- purchase request,- merchant passes signed, encrypted authorization to the acquirer for check,- card validation with issuer,4,- issuer authorizes and signs transaction,5,- acquirer authorizes merchant and signs the transaction,6,- cardholder receives the goods and a receipt,7,- merchant deposit the transaction to his account,8,- merchant gets paid,9,- cardholder receives bill from card issuer,2022/11/22,14,安全协议系统模型,如果将安全协议所处环境视为一个系统，那么这个系统中，一般而言包括一些发送和接收消息的诚实的主体和一个攻击者，以及用于管理消息发送和接收的规则。,诚实主体,诚实主体,诚实主体,诚实主体,环境/攻击者,通信,通信,通信,通信,2022/11/22,15,安全协议的性质,评估一个安全协议是否安全就是检查其所欲达到的安全性质是否遭到攻击者的破坏。认证性声称者使用仅为其与验证者知道的密钥封装的一个消息声称者使用私钥对消息签名，验证者使用公钥来验证声称者通过可信第三方来证明自己。秘密性保护协议消息不被泄露给非授权拥有此消息的人，即使是攻击者观测到了消息的格式，它也无法从中得到消息的内容或提炼出有用的信息。保证协议消息秘密性的最直接的方法是对消息进行加密。安全协议中，一般不考虑具体的密码算法的执行细节，但在实际应用中这往往有可能造成协议秘密性的缺陷。,2022/11/22,16,安全协议的性质,完整性保护协议消息不被非法篡改、删除和替代。常用的方法有封装和签名SSL和IKE等协议中就涉及到保护协议消息完整性的具体实现细节不可否认性目的是通过通信主体提供参与协议交换的证据来保证其合法利益不受侵害，即协议主体必须对自己的合法行为负责，而不能也无法事后否认。协议必须具有两个特点：证据的正确性、交易的公平性。在不可否认性之中还可引申出其他一些相关性质，如适时中止性、公平性、可追究性等。,2022/11/22,17,安全协议的缺陷,安全协议的安全性安全协议是许多分布式系统安全的基础，确保这些协议的安全运行是极为重要的。安全协议有若干几个消息传递，消息之间存在着复杂的相互作用和制约；协议中使用多种不同的密码体制，目前的许多安全协议存在安全缺陷。原因有两个：协议设计者误解或者采用了不恰当的技术；协议设计者对环境要求的安全需求研究不足。对协议的安全性进行分析和研究是一个重要的课题。,2022/11/22,18,安全协议的缺陷,S.Gritzalis和D.Spinellis根据安全缺陷产生的原因和相应的攻击方法对安全缺陷进行了分类：基本协议缺陷：协议设计中没有或很少考虑防范攻击者。口令/密钥猜测缺陷：弱口令导致攻击者能够进行口令猜测攻击；或者弱密钥使攻击者能够破解该密钥。 陈旧（stale）消息缺陷：协议设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等等。,2022/11/22,19,安全协议的缺陷,并行会话缺陷协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的重要消息。内部协议缺陷协议可达性存在问题，协议的参与者中至少有一方不能够完成所有必须的动作而导致缺陷。密码系统缺陷协议中使用的密码算法的安全强度导致协议不能完全满足所要求的机密性、认证等需求而产生的缺陷。,2022/11/22,20,安全协议的逻辑形式化分析,安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存在安全缺陷。从安全协议的分析和设计角度来看，应当对协议的安全性作出认真的分析和验证。安全协议的分析方法攻击检验方法；形式化的分析方法。,2022/11/22,21,安全协议的逻辑形式化分析,攻击检验方法搜集使用目前的对协议的有效攻击方法，逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力。在分析的过程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析。这种分析方法对已知的攻击非常有效的。不能发现协议中未知的安全隐患。,2022/11/22,22,安全协议的逻辑形式化分析,形式化的分析方法采用各种形式化的语言或者模型，为安全协议建立模型，并按照给定的假设和规则，分析、验证方法证明协议的安全性。近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。形式化的分析方法是目前研究的热点，但是就其实用性来说，还有待进一步突破。安全协议的形式化分析有助于：界定安全协议的边界，即协议系统与其运行环境的界面更准确地描述安全协议的行为。更准确地定义安全协议的特性。证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。,2022/11/22,23,协议形式化分析技术(1),1）通用的形式化描述语言使用通用的、不是为分析安全协议专门设计的形式化描述语言和协议校验工具建立安全协议的模型并进行校验。主要思想是将安全协议看作一般的协议，并试图证明协议的正确性。采用的工具和模型与验证一般协议的类似，例如使用有限状态图、Petri网模型、LOTOS语言等等。方法的主要缺点是仅证明协议的正确性而不是安全性。,2022/11/22,24,协议形式化分析技术(2),2）专家系统设计专用的专家系统来制定安全协议的校验方案并进行协议检验，从而对协议的安全性作出结论。主要思想是针对所设计的协议而开发专用的专家系统，通过专家系统发现协议是否能够达到不合理的状态（比如密钥的泄露等等）。这种技术能够识别缺陷但是不能证明协议的安全性，也不能发现未知的缺陷。,2022/11/22,25,协议形式化分析技术(3),3）安全需求模型基于知识和信任逻辑，针对具体协议建立相应的形式化安全需求模型依据给定的逻辑初设和公理规则对该模型进行形式化分析推理通过推理获取的结果来推断协议能否完成预期的目标、证明协议结论的正确性。形式系统的组成（初始符号、形式规则、公理、变形规则）,2022/11/22,26,协议形式化分析技术(4),这种方法是目前为止使用最广泛的一种方法，最著名的是BAN逻辑。BAN逻辑是基于知识和信任的形式逻辑模型，进行基于知识和信任的分析。BAN逻辑假设协议的安全是完整性和新鲜度的函数，使用逻辑规则来对协议的属性进行跟踪和分析。通常，BAN逻辑只能推出给定初设的协议结果，对一般的安全性的证明依赖于给定攻击模型的初设。使用BAN逻辑分析安全协议的步骤如下：协议的理想化转化；假设所有的协议初始状态；使用逻辑规则对系统的状态作出断言；运用逻辑原理得到关于信任的断言；,2022/11/22,27,协议形式化分析技术(5),4）代数系统形式化模型基于密码学系统的代数特性开发协议的形式化模型将安全协议系统当作一个代数系统模型，表示出协议的参与者的各种状态，然后分析某种状态的可达性。Michael Merritt已经证明了代数模型可以用来分析安全协议。美国海军研究实验室（Navy Research Lab.）开发的协议分析器是这种方法中最成功的一个应用，可以用来在各种协议中寻找新的和已知的缺陷。,2022/11/22,28,安全协议分析的问题,安全协议分析的问题形式化分析方法在安全协议的应用是研究的热点。目前应用并不广泛的主要原因,是需要事先建立安全协议的安全性形式化模型。该过程比较复杂困难。目前并没有一种方法能够给出安全协议安全性的充分而且必要的理论证明。由于安全协议本身的复杂性，上述每一类方法都有不同的侧重点，或多或少地存在不足之处。使用上述方法分析安全协议的时候，应当仔细分析协议的特点、应用环境和需求，综合使用这些分析方法，以得到一个比较合理的结果。,2022/11/22,29,BAN逻辑:一种验证逻辑,由Burrows, Abadi & Needham提出，从而解决了SPA（Security Protocol Analysis)问题上迈出一大步。它是关于主体信仰以及用于从已有信仰推出新的信仰的推理规则的逻辑。这种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接收消息能否从最初的信仰逐渐发展到协议运行最终要达到的目的认证双方的最终信仰，其目的是在一个抽象层次上分析分布网络系统中认证协议的安全问题。如在协议执行结束时未能建立起关于诸如共享通信密钥、对方身份等信任时，则表明这一协议有安全缺陷。BAN逻辑包含believing、seeing、controlling和saying message语句，并以一种自然结构进行语义描述。,2022/11/22,30,BAN逻辑:一种验证逻辑,Burrows, Abadi & Needham定义一种基于信任的逻辑精确地表示这些信任找准、抓住导致信任的原因BAN通过形式化的方法回答以下问题协议在工作吗？协议能否使用？协议达到了预定的目标吗？协议比别的协议需要更多的安全假设吗？协议做了不必要的事吗？,2022/11/22,31,BAN逻辑:一种验证逻辑,BAN逻辑形式化分析方法重点放在对协议涉及的通信各方的信任以及由这些信任的进一步推演所得到的通信结果上不考虑由程序执行时所引入的错误如死锁，甚至密码系统的不正确使用问题考虑到入侵的可能性，并不试图去处理不信任的参与方的认证，也不检测加密方案及未经授权的密码体系。,2022/11/22,32,BAN逻辑:一种验证逻辑,BAN逻辑形式推理过程1. 给出协议的消息序列描述；2. 对协议进行理想化转换；【】3. 分析理想化的协议模型；4. 判断结论。,2022/11/22,33,BAN逻辑的形式体系,BAN逻辑的符号、语法、语义、规则(1)BAN形式体系建立在多种类的模型逻辑上在BAN逻辑中区分几种对象主体(principals)加密密钥(encryption keys)公式(formulas)，也称为语句(statements)。,2022/11/22,34,BAN逻辑的形式体系,BAN逻辑的符号、语法、语义、规则(2)公式或语句的连接符(conjunction)用逗号表示【例如】(X,Y)表示X和Y的结合具有结合性和交换性BAN逻辑认为消息(message)和语句(statements)是一样的。,2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑的符号、语法、语义、规则(3)BAN逻辑的符号 表示如果P为真，则Q为真。同时假定协议参与者是良好的逻辑学家，即:如果Alice相信陈述命题X和以及 ，则她也信任命题Y,2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑符号A, S 表示具体的主体；KAS 表示具体的共享对称密钥；KA, KS 表示具体的公钥；KA-1, KS-1 表示具体的私钥；NA, NA, NA, NS, NS 表示临时值(一次性随机值)； P, Q, R表示任意主体；X, Y表示任意语句；K 表示任意密钥。,2022/11/2217:40:22,BAN逻辑的形式体系,P相信X；或者P认为X为真 P曾经收到X；P看见、能读并且能重复X。P曾发送出X；但在发出X时，P相信X。P对X有控制权；P是X的权威机构并且P相信X。例如，通常相信服务器能正确产生加密密钥。初始假设中则表示主体对密钥的质量有控制权。X是新的、适时的；它经常用随机值来表示，用它来说明X是新鲜的。随机值通常包括时间戳或者一个一次性使用的数。,BAN逻辑语法、语义,2022/11/2217:40:22,BAN逻辑的形式体系,P和Q可用共享密钥K通信，如果K是好的，则意味着除了P和Q以及P或者Q所信任的主体之外的任何主体都不会发现它。K是P的公开密钥，相应的私钥K-1不会被除了P和P所信任的主体之外的主体知道。 X是只有P和Q知道的秘密，也可能P和Q信任的主体知道。只有P和Q能用X来相互说明他们彼此的身份。一个秘密的例子就是口令。,BAN逻辑语法、语义(续1),2022/11/2217:40:22,BAN逻辑的形式体系,表示X经密钥K加密后的结果表示X和Y相结合(combined)；它表明Y是一个秘密，它的出现可以证明谁发出了Y消息。符号强调突出Y扮演着能证明X起源的特殊角色。在具体执行时，X只是简单的与口令Y结合。在很多时候，Y实际上就是密钥。在BAN逻辑中，可能别的工作在这些结构中使用不同的符号。当前这些符号更详细冗长，但更容易读，因此，更适合论文中用很少的公式。 H(X)是X的单向杂凑函数（哈希Hash）值,BAN逻辑语法、语义(续2),2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑规则：消息含义（“收发”）规则,要保证这个规则是合理的，我们则必须保证P自己没有说过X；这就要将公式XK表示成XK from Q，并且要求Q不能是P,消息含义规则关心消息的解释。其中三分之二关心加密消息的解释。它们关心解释如何得到消息源的信任,2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑规则：消息（“发发”）规则,2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑规则：消息接收（“收收”）规则,2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑规则：随机数验证（“新鲜信任”）规则,2022/11/2217:40:22,BAN逻辑的形式体系,BAN逻辑规则：裁判（“信任”）规则,2022/11/2217:40:22,BAN逻辑的形式体系,类BAN逻辑规则：单向哈希函数规则,Q拥有消息X,2022/11/2217:40:22,BAN逻辑形式化分析方法,BAN逻辑形式推理证明步骤给出协议的消息序列描述对协议进行理想化转换建立协议的理想化模型；给出初始假设状态集合；给出预期目标集合；分析理想化的协议模型利用初设和逻辑公设规则对协议系统进行推理得出状态断言，以及协议所能得到的、关于信任的最终目标断言集合；最后判断结论：若，则协议可行。,2022/11/2217:40:22,BAN逻辑形式化分析方法,协议的消息序列描述协议必须首先被描述成自己的消息序列表，每条消息可典型地写成以下形式：PQ: message.这表示P发送消息给Q。消息应按照原设计意图表示成具体执行时的位串，但非正式的符号。,2022/11/2217:40:22,BAN逻辑形式化分析方法,对协议进行理想化转换理想化模型(2.1.1)由于“PQ: message”这种表达经常含糊不清，仍不适合作为形式化分析的基础。因此，需要将协议的每个步骤转换成理想化模型。协议的理想化模型中，消息是公式或语句。例如，协议步骤：Alice告诉Bob(他知道Kbs)：我是Alice, Kab是她(Alice)和他(Bob)之间的通信密钥。,2022/11/2217:40:22,BAN逻辑形式化分析方法,对协议进行理想化转换理想化模型(2.1.2)该协议步骤 可理想化为语义：从(A,Kab)到 ，该消息完成了由符号到逻辑语义的协议理想化转换（因为BAN逻辑关心语义推理）。BAN逻辑忽略明文通信，只是因为明文能被伪造。明文对认证协议的作用仅仅是提供在已被加密的消息中有哪些信息的线索。,2022/11/2217:40:22,BAN逻辑形式化分析方法,对协议进行理想化转换理想化模型(2.1.3)理想化转换后所描述的协议比传统的协议描述更清楚、详细和规范。建议在设计和描述协议时都使用理想化协议模型。为研究已发表的协议，必须依据形式化的转化规则，为每个协议表述其理想化协议模型。理想化的协议模型中不包括明文消息；理想化的消息通常形式为：,2022/11/2217:40:22,BAN逻辑形式化分析方法,对协议进行理想化转换初始假设(2.2.1)给出初始假设状态集合的形式化描述；大多情况，协议形式化分析的初始假设如下：,协议的初始必须是不变的，以保证每个协议的成功。 典型的，初始假设都是陈述两个主体之间共享什么样的密钥，哪个主体产生新鲜的随机值，哪个主体在某些特定的方式下是可信任的。 在大多数的情况下，初始假设是标准和明显的。一旦所有的初始假设被写出，验证协议就等同于对作为结论的公式做出证明。,2022/11/2217:40:22,BAN逻辑形式化分析方法,对协议进行理想化转换预期目标(2.2.2)给出预期目标集合的形式化描述；大多情况，协议形式化分析的预期目标如下：,认证协议经常是建立某些用共享会话密钥的基础，所以，我们可得到认证协议的目标这样的结论描述。 因此，如果认为A和B之间有密钥K，认证则是完成了A相信K是A与B之间的通信密钥，B相信K是A与B之间的通信密钥。 一些协议可能要求的比这更多,2022/11/2217:40:22,BAN逻辑形式化分析方法,分析理想化的协议模型利用初设和逻辑公设规则对协议系统进行推理得出状态断言，以及协议所能得到的、关于信任的最终目标断言集合；判断结论我们将通过具体的示例讲解以上两步骤,BAN逻辑形式化分析运用,【例1】THE KERBEROS PROTOCOL,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】1. Kerberos协议消息序列描述Message 1. Message 2.Message 3.Message 4.,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】2.1 Kerberos协议理想化模型Message 1. Message 2.Message 3.Message 4.,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】2.2 Kerberos协议理想化模型初始假设,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】2.3 Kerberos协议理想化模型预期目标,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】3. 分析理想化协议模型,The main steps of the proof are as follows: A receives Message 2. The annotation rules yield that,holds afterward. Since we have the hypothesis,the message-meaning rule for shared keys applies and yields the following:,One of our rules to break conjunctions (omitted here) then produces,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】3. 分析理想化协议模型(续1),2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】3. 分析理想化协议模型(续2)A passes the ticket on to B, together with another message containing a time-stamp. Initially, B can decrypt only the ticket:Logically, this result is obtained in the same way as that for Message 2, via the message-meaning, nonce-verification, and jurisdiction postulates.Knowledge of the new key allows B to decrypt the rest of Message 3. Through the message-meaning(P1.1),the nonce-verification postulates(P2.1)and M3, we deduce the following:,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例1】3. 分析理想化协议模型(续3)The fourth message simply assures A that B believes in the key and has received As last message. After new applications of the message-meaning and nonce-verification postulates to the fourth message, the final result is as follows:,If only the first three messages are used, we do not obtainThat is, the three-message protocol does not convince A of Bs existenceA observes the same messages whether B is running or not.,BAN逻辑形式化分析运用,【例2】The Otway-Rees Authentication Protocol,2022/11/22,64,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Otway-Rees Authentication Protocol协议消息序列描述,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Ottway-Rees Authentication Protocol协议理想化模型,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Ottway-Rees Authentication Protocol协议理想化模型初始假设,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Ottway-Rees Authentication Protocol协议理想化模型预期目标应该考虑：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Ottway-Rees Authentication Protocol分析理想化协议模型,P3.1,P1.1,P2.1,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Ottway-Rees Authentication Protocol分析理想化协议模型(续)同理可得：也可推导得出：但仅可证明：,因为缺少,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例2】The Ottway-Rees Authentication Protocol判断结论可推导得出：但我们仅可证明：并且，NC能够代替NA，即：NA是不必要的。,BAN逻辑形式化分析运用,【例3】The Needham-Schroeder Protocol,2022/11/2217:40:22,Protocol Analysis in BAN logics,描述协议的每一条消息(Specify messages of the protocol)理想化协议即注解协议每条消息为已接收到的断言形式(Idealize the protocol, Annotate protocol. For each message of the protocol) P Q: M, assert Q received M给出协议的初始信任假设和协议预期的信任目标(Write assumptions about initial state. And asset of Goal)使用BAN逻辑推导协议主体所能最终拥有的信任(Use the logic to derive the beliefs held by protocol principals.),2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol1）协议消息序列描述,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol2） 协议理想化模型(注意我们放弃了第一条消息，因为它是明文发送的),M2.,M3.,M4.,M5.,将消息写成“收到”形式,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol3）协议理想化模型初始的信任假设(红色命题是NS无法达到的),2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol3）协议理想化模型，协议预期的信任目标应该考虑：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由初始假设A.A1，消息M.2，消息含义公理，得结论C.1：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由初始假设A.A3，结论C.1，从随机数新鲜验证-信任公理得结论C.2：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由初始假设A.A2， A.A4，从仲裁-信任公理得结论C.3,C.4：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由初始假设A.B1，消息M.3，消息含义公理，得结论C.5：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由结论A.B5，C.5，随机数验证-信任公理，得结论C.6： NS需要不合理的的假设 ，才能继续,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由结论C.6，初始假设A.B2，A.B4 , 仲裁-信任公理，得结论C.7： 其中C.7是Bob获得的 而Alice则假设Trent能够控制KAB的新鲜性来得到,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由结论C.3，消息M.4，消息含义公理，得结论C.8：,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型由结论C.4，C.8，消息新鲜-信任公理，得结论C.9,C.10： 同理，由A.B5,可得结论,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型：判断结论由以下结论组成及关于协议的最终断言 :但我们无法得到 证毕,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型：判断结论 分析过程，可发现协议主体B关于随机数NB的新鲜信任 B believes fresh(Nb) 也就是 ，是不需要的。 协议推导得出的结论完全用不着NB.,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型：判断结论 从 Trent 对 Alice 说(saying)的消息2： , 我们能够以同样的方式证明 ，但是，Bob得到的共享密钥含义 是来自Alice的消息3，其中并没有关联上Trent的声明、以便于Bob知道密钥是新鲜的 (即消息可能是旧的,被伪造,重放) 。 由于NS协议无法令 ，因此，我们无法让Bob获得比 更多的信任了。,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder Protocol判断结论(Needham-Schroeder 已被揭露的漏洞)分析结果正确地指出，Needham-Schroeder协议存在的漏洞: Mallory (伪装者)能够记录Alice和 Bob之间交换的密钥，并在他选择的任意时间内，哄骗Bob接受第三条消息中的(旧的，可能已被破解的)密钥.无论如何，当无法回复Bob的时候， Mallory就可以阻碍掉来自Bob的第四条消息.但且Mallory 能够提供一个消耗数年CPU时间破解所得到的KAB ，之时，他就能令Bob接受并使用一个陈年的旧密钥.,2022/11/2217:40:22,BAN逻辑形式化分析运用,【例3】the Needham-Schroeder ProtocolDenning-Sacco Attack假使攻击者拥有泄露的旧会话密钥，结果会怎样呢？从第3条消息开始EA B: Kab , AKbs B EA: NbKabEA B: Nb 1 Kab其中，EA - 攻击者/入侵者/渗透者/偷听者/间谍：Eve 冒充成 Alice,2022/11/22,91,BAN逻辑的存在问题,协议的理想化过于依赖分析时的直觉，协议的理想化使得在原始协议与理想化协议之间存在一个潜在的语义鸿沟。Ban逻辑分析的正确性严重依赖于前几步，但前三步在有效达成目标上存在问题。即使对协议行为做出了准确的解释，也不能保证能够正确