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

《第十五章安全协议形式化分析ppt课件》由会员分享，可在线阅读，更多相关《第十五章安全协议形式化分析ppt课件（133页珍藏版）》请在金锄头文库上搜索。

1、经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用 第十五章 安全协议的形式化分析技术2024/8/312024/8/311 1经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用逻辑推理及形式化语言逻辑推理形式化语言形式化分析方法形式化分析方法应用2024/8/312024/8/312 2经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用逻辑推理逻辑推理 由

2、前提推出结论。前提和结论都是命题。 命题的真或假由命题的内容是否符合客观实际确定。演绎逻辑 当前提的“真”蕴涵结论的“真”，称前提和结论之间有可推导性关系。即前提和结论之间的推理是正确的。 研究怎样的前提和结论之间具有可推导性关系。归纳逻辑 只要求得到的结论本身是协调的，与前提是协调的。 前提的“真”并不蕴涵结论的“真”。2024/8/312024/8/313 3经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用逻辑推理逻辑推理的正确性命题的内容：“真”/“假”，内容决定命题的“真”/“假”。命题的形式：即逻辑形式

3、。由内容抽象出来。逻辑形式决定前提和结论的之间的可推导性关系。不关心前提和结论的真假，而关注前提的真是否蕴涵结论的真。2024/8/312024/8/314 4经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用形式化语言形式语言使用自然语言陈述并分析命题常常引出歧义。需要构造一种符号语言形式语言，描述由命题内容抽象出来的命题逻辑形式。形式语言使用符号来构造公式由公式来精确地表示命题的逻辑形式语义和语法语义涉及符号和符号表达式的涵义(给符号某种解释)语法涉及符号表达式的形式结构，但不考虑任何对形式语言的解释。形式语言

4、的语义和语法既有联系，又有区分。2024/8/312024/8/315 5经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用形式化分析方法集合论数理逻辑图论：有限状态图网论：Petri网模型代数系统：代数系统形式化模型2024/8/312024/8/316 6经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议 安全协议的基本概念安全协议特指使用密码学技术的密码协议所谓协议，就是两个或者两个以上的参与者为完成某项特定的任务而采取的

5、一系列步骤。 协议的定义包含三层含义：1. 协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之前，后面的步骤不可能执行；在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤。2. 协议至少需要两个参与者；一个人可以执行一系列的步骤来完成一项任务，但它不构成协议。3. 通过协议必须能够完成某项任务。 安全协议使用密码学技术，协议参与者可能是可以信任的人，也可能是攻击者和完全不信任的人。密码协议包含某种密码算法。2024/8/312024/8/317 7经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的

6、费用安全协议网络通信中常用的密码协议按照其完成的功能分成以下四类： 密钥交换协议在参与协议的两个或者多个实体之间建立共享的秘密通道，常用于建立在一次通信中所使用的会话密钥。协议可以采用对称密码体制，也可以采用非对称密码体制，例如Diffie-Hellman密钥交换协议。认证协议认证协议中包括实体认证（身份认证）协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。认证和密钥交换协议协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。常见的有Needham-Schroeder协议、分布认证安全服务（DASS）协议、ITU-T X.509认证协议等等

7、。电子商务协议电子商务协议中，主体利益目标往往是不一致的，电子商务协议关注的就是公平性，即协议应保证交易双方都不能通过损害对方利益而得到它不应得的利益。常见的电子商务协议有SET协议等。2024/8/312024/8/318 8经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用DH算法描述1.Alice与ob确定两个大素数n和g，这两个整数不保密， Alice与ob 可以使用不安全信道确定这两个数2.Alice选择另一个大随机数x，并计算A如下： A=gx mod n3.Alice将发给ob4.ob选择另一个大随机

8、数y，并计算B如下： B=gy mod n5.ob将发给Alice6.计算秘密密钥K1如下： K1=Bx mod n7.计算秘密密钥K2如下： K2=Ay mod n2024/8/312024/8/319 9经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SSL/TLS协议栈介于应用层和传输层之间为上层提供安全性IPSSL ChangeCipher SpecProtocolSSL AlertProtocolApplication ProtocolTCPSSL RecordProtocolSSL Handshake

9、ProtocolHTTPLDAPIMAP2024/8/312024/8/311010经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SSL/TLS概况协议分为两层上层：TLS握手协议、TLS密码变化协议、TLS警告协议底层：TLS记录协议上层协议是用于管理SSL密钥信息的交换，下层提供基本的安全服务TLS握手协议客户和服务器之间相互认证协商加密算法和密钥它提供连接安全性，有三个特点身份认证，至少对一方实现认证，也可以是双向认证协商得到的共享密钥是安全的，中间人不能够知道协商过程是可靠的TLS记录协议建立在可靠的传

10、输协议(如TCP)之上它提供连接安全性，有两个特点保密性，使用了对称加密算法完整性，使用HMAC算法用来封装高层的协议2024/8/312024/8/311111经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SET协议目标信信息息在在InternetInternet上上的的安安全全传传输输，保保证证网网上上传传输输的的数据不被黑客窃听数据不被黑客窃听订订单单信信息息和和个个人人账账号号信信息息的的隔隔离离，在在将将包包括括消消费费者者账账号号信信息息的的订订单单送送到到商商家家时时，商商家家只只能能看看到到订订

11、货信息，而看不到消费者的账户信息货信息，而看不到消费者的账户信息 消消费费者者和和商商家家的的相相互互认认证证，以以确确定定通通信信双双方方的的身身份份，一一般般由由第第三三方方机机构构负负责责为为在在线线通通信信双双方方提提供供信用担保信用担保要要求求软软件件遵遵循循相相同同的的协协议议和和消消息息格格式式，使使不不同同厂厂家家开开发发的的软软件件具具有有兼兼容容和和互互操操作作功功能能，并并且且可可以以运行在不同的硬件和操作系统平台上运行在不同的硬件和操作系统平台上2024/8/312024/8/311212经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加

12、赔偿的金额为消费者购买商品的价款或接受服务的费用Card HolderHow SET with Credit Card WorksMerchant ServerAcquiring BankCard Issuer Bank876543219CACertificate Authority00- cardholder registration132- purchase request- merchant passes signed, encrypted authorization to the acquirer for check- card validation with issuer4- iss

13、uer authorizes and signs transaction5- acquirer authorizes merchant and signs the transaction6- cardholder receives the goods and a receipt7- merchant deposit the transaction to his account8- merchant gets paid9- cardholder receives bill from card issuer2024/8/312024/8/311313经营者提供商品或者服务有欺诈行为的，应当按照消费

14、者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议系统模型如果将安全协议所处环境视为一个系统，那么这个系统中，一般而言包括一些发送和接收消息的诚实的主体和一个攻击者，以及用于管理消息发送和接收的规则。诚实主体诚实主体诚实主体诚实主体环境/攻击者通信通信通信通信2024/8/312024/8/311414经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的性质 评估一个安全协议是否安全就是检查其所欲达到的安全性质是否遭到攻击者的破坏。认证性声称者使用仅为其与验证者知道的

15、密钥封装的一个消息声称者使用私钥对消息签名，验证者使用公钥来验证声称者通过可信第三方来证明自己。秘密性保护协议消息不被泄露给非授权拥有此消息的人，即使是攻击者观测到了消息的格式，它也无法从中得到消息的内容或提炼出有用的信息。保证协议消息秘密性的最直接的方法是对消息进行加密。安全协议中，一般不考虑具体的密码算法的执行细节，但在实际应用中这往往有可能造成协议秘密性的缺陷。2024/8/312024/8/311515经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的性质完整性保护协议消息不被非法篡改、删除和替代

16、。常用的方法有封装和签名SSL和IKE等协议中就涉及到保护协议消息完整性的具体实现细节不可否认性目的是通过通信主体提供参与协议交换的证据来保证其合法利益不受侵害，即协议主体必须对自己的合法行为负责，而不能也无法事后否认。协议必须具有两个特点：证据的正确性、交易的公平性。在不可否认性之中还可引申出其他一些相关性质，如适时中止性、公平性、可追究性等。2024/8/312024/8/311616经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的缺陷安全协议的安全性安全协议是许多分布式系统安全的基础，确保这些协议

17、的安全运行是极为重要的。安全协议有若干几个消息传递，消息之间存在着复杂的相互作用和制约；协议中使用多种不同的密码体制，目前的许多安全协议存在安全缺陷。原因有两个：协议设计者误解或者采用了不恰当的技术；协议设计者对环境要求的安全需求研究不足。对协议的安全性进行分析和研究是一个重要的课题。2024/8/312024/8/311717经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的缺陷S.Gritzalis和D.Spinellis根据安全缺陷产生的原因和相应的攻击方法对安全缺陷进行了分类：基本协议缺陷：协议设

18、计中没有或很少考虑防范攻击者。口令/密钥猜测缺陷：弱口令导致攻击者能够进行口令猜测攻击；或者弱密钥使攻击者能够破解该密钥。 陈旧（stale）消息缺陷：协议设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等等。2024/8/312024/8/311818经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的缺陷并行会话缺陷协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的重要消息。内部协议缺陷协议可达性存在问题，协议的参与者中至

19、少有一方不能够完成所有必须的动作而导致缺陷。密码系统缺陷协议中使用的密码算法的安全强度导致协议不能完全满足所要求的机密性、认证等需求而产生的缺陷。2024/8/312024/8/311919经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的逻辑形式化分析安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存在安全缺陷。从安全协议的分析和设计角度来看，应当对协议的安全性作出认真的分析和验证。安全协议的分析方法攻击检验方法；形式化的分析方法。2024/8/312024/8/312020经营

20、者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的逻辑形式化分析攻击检验方法搜集使用目前的对协议的有效攻击方法，逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力。在分析的过程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析。这种分析方法对已知的攻击非常有效的。不能发现协议中未知的安全隐患。2024/8/312024/8/312121经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议的逻辑形式化分析形

21、式化的分析方法采用各种形式化的语言或者模型，为安全协议建立模型，并按照给定的假设和规则，分析、验证方法证明协议的安全性。近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。形式化的分析方法是目前研究的热点，但是就其实用性来说，还有待进一步突破。安全协议的形式化分析有助于：界定安全协议的边界，即协议系统与其运行环境的界面更准确地描述安全协议的行为。更准确地定义安全协议的特性。证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。2024/8/312024/8/312222经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失

22、，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议形式化分析技术(1)1）通用的形式化描述语言使用通用的、不是为分析安全协议专门设计的形式化描述语言和协议校验工具建立安全协议的模型并进行校验。主要思想是将安全协议看作一般的协议，并试图证明协议的正确性。采用的工具和模型与验证一般协议的类似，例如使用有限状态图、Petri网模型、LOTOS语言等等。方法的主要缺点是仅证明协议的正确性而不是安全性。2024/8/312024/8/312323经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议形式化分析技术(2

23、)2）专家系统设计专用的专家系统来制定安全协议的校验方案并进行协议检验，从而对协议的安全性作出结论。主要思想是针对所设计的协议而开发专用的专家系统，通过专家系统发现协议是否能够达到不合理的状态（比如密钥的泄露等等）。这种技术能够识别缺陷但是不能证明协议的安全性，也不能发现未知的缺陷。2024/8/312024/8/312424经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议形式化分析技术(3)(3)3）安全需求模型基于知识和信任逻辑，针对具体协议建立相应的形式化安全需求模型依据给定的逻辑初设和公理规则对该模型

24、进行形式化分析推理通过推理获取的结果来推断协议能否完成预期的目标、证明协议结论的正确性。形式系统的组成（初始符号、形式规则、公理、变形规则）2024/8/312024/8/312525经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议形式化分析技术(4)(4)这种方法是目前为止使用最广泛的一种方法，最著名的是BAN逻辑。BAN逻辑是基于知识和信任的形式逻辑模型，进行基于知识和信任的分析。BAN逻辑假设协议的安全是完整性和新鲜度的函数，使用逻辑规则来对协议的属性进行跟踪和分析。通常，BAN逻辑只能推出给定初设的协

25、议结果，对一般的安全性的证明依赖于给定攻击模型的初设。使用BAN逻辑分析安全协议的步骤如下：协议的理想化转化；假设所有的协议初始状态；使用逻辑规则对系统的状态作出断言；运用逻辑原理得到关于信任的断言；2024/8/312024/8/312626经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议形式化分析技术(5)4）代数系统形式化模型基于密码学系统的代数特性开发协议的形式化模型将安全协议系统当作一个代数系统模型，表示出协议的参与者的各种状态，然后分析某种状态的可达性。Michael Merritt已经证明了代数

26、模型可以用来分析安全协议。美国海军研究实验室（Navy Research Lab.）开发的协议分析器是这种方法中最成功的一个应用，可以用来在各种协议中寻找新的和已知的缺陷。2024/8/312024/8/312727经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用安全协议分析的问题安全协议分析的问题形式化分析方法在安全协议的应用是研究的热点。目前应用并不广泛的主要原因,是需要事先建立安全协议的安全性形式化模型。该过程比较复杂困难。目前并没有一种方法能够给出安全协议安全性的充分而且必要的理论证明。由于安全协议本身的

27、复杂性，上述每一类方法都有不同的侧重点，或多或少地存在不足之处。使用上述方法分析安全协议的时候，应当仔细分析协议的特点、应用环境和需求，综合使用这些分析方法，以得到一个比较合理的结果。2024/8/312024/8/312828经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑:一种验证逻辑由Burrows, Abadi & Needham提出，从而解决了SPA（Security Protocol Analysis)问题上迈出一大步。它是关于主体信仰以及用于从已有信仰推出新的信仰的推理规则的逻辑。这种逻辑

28、通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接收消息能否从最初的信仰逐渐发展到协议运行最终要达到的目的认证双方的最终信仰，其目的是在一个抽象层次上分析分布网络系统中认证协议的安全问题。如在协议执行结束时未能建立起关于诸如共享通信密钥、对方身份等信任时，则表明这一协议有安全缺陷。BAN逻辑包含believing、seeing、controlling和saying message语句，并以一种自然结构进行语义描述。2024/8/312024/8/312929经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服

29、务的费用BAN逻辑:一种验证逻辑Burrows, Abadi & Needham定义一种基于信任的逻辑精确地表示这些信任找准、抓住导致信任的原因BAN通过形式化的方法回答以下问题协议在工作吗？协议能否使用？协议达到了预定的目标吗？协议比别的协议需要更多的安全假设吗？协议做了不必要的事吗？2024/8/312024/8/313030经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑:一种验证逻辑BAN逻辑形式化分析方法重点放在对协议涉及的通信各方的信任以及由这些信任的进一步推演所得到的通信结果上不考虑由程序

30、执行时所引入的错误如死锁，甚至密码系统的不正确使用问题考虑到入侵的可能性，并不试图去处理不信任的参与方的认证，也不检测加密方案及未经授权的密码体系。2024/8/312024/8/313131经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑:一种验证逻辑BAN逻辑形式推理过程1. 给出协议的消息序列描述；2. 对协议进行理想化转换；【】3. 分析理想化的协议模型；4. 判断结论。2024/8/312024/8/313232经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加

31、赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系BAN逻辑的符号、语法、语义、规则(1)BAN形式体系建立在多种类的模型逻辑上在BAN逻辑中区分几种对象主体(principals)加密密钥(encryption keys)公式(formulas)，也称为语句(statements)。2024/8/312024/8/313333经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系BAN逻辑的符号、语法、语义、规则(2)公式或语句的连接符(conjunction)用逗号表示【例如】

32、(X,Y)表示X和Y的结合具有结合性和交换性BAN逻辑认为消息(message)和语句(statements)是一样的。2024/8/312024/8/313434VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑的符号、语法、语义、规则逻辑的符号、语法、语义、规则(3)(3)n nBANBAN逻辑的符号逻辑的符号 表示如果表示如果P P为真，则为真，则QQ为真。为真。n n同时假定协议参

33、与者是良好的逻辑学家，即同时假定协议参与者是良好的逻辑学家，即: :如果如果AliceAlice相信陈述命题相信陈述命题X X和以及和以及 ，则，则她她也信任命题也信任命题Y Y2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑符号逻辑符号A A, , S S 表示具体的主体；表示具体的主体；K KASAS 表示具体的共享对称密钥；表示具体的共享对称密钥

34、；K KA A, , K KS S 表示具体的公钥；表示具体的公钥；K KA A-1-1, , K KS S-1-1 表示具体的私钥；表示具体的私钥；N NA A, , NNA A, , NNA A, , N NS S, , NNS S 表示临时值表示临时值( (一次性随机值一次性随机值) )； P P, , QQ, , R R表示任意主体；表示任意主体；X X, , Y Y表示任意语句；表示任意语句；K K 表示任意密钥。表示任意密钥。2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为

35、的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 P P相信相信X X；或者；或者P P认为认为X X为真为真 P P曾经收到曾经收到X X；P P看见、能读并且能重复看见、能读并且能重复X X。P P曾发送出曾发送出X X；但在发出；但在发出X X时，时，P P相信相信X X。P P对对X X有控制权；有控制权；P P是是X X的权威机构并且的权威机构并且P P相信相信X X。例如，通常相信服务器能正确产生加密密钥。例如，通常相信服务器能正确产生加密密钥。初始假设中则表示主体对密钥的质量有控制权。初始假设中则表示主体对密钥

36、的质量有控制权。X X是新的、适时的；它经常用随机值来表示，用它来说明是新的、适时的；它经常用随机值来表示，用它来说明X X是新鲜的。随机值通常包括时间戳或者一个一次性使是新鲜的。随机值通常包括时间戳或者一个一次性使用的数。用的数。BANBAN逻辑语法、语义逻辑语法、语义2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 P P和和QQ可用共享密钥可用共享密钥K K通信，

37、如果通信，如果K K是好的，则意味着除是好的，则意味着除了了P P和和QQ以及以及P P或者或者QQ所信任的主体之外的任何主体所信任的主体之外的任何主体都不会发现它。都不会发现它。K K是是P P的公开密钥，相应的私钥的公开密钥，相应的私钥K K-1-1不会被除了不会被除了P P和和P P所信所信任的主体之外的主体知道。任的主体之外的主体知道。 X X是只有是只有P P和和QQ知道的秘密，也可能知道的秘密，也可能P P和和QQ信任的主体知信任的主体知道。只有道。只有P P和和QQ能用能用X X来相互说明他们彼此的身份。来相互说明他们彼此的身份。一个秘密的例子就是口令一个秘密的例子就是口令。BA

38、NBAN逻辑语法、语义逻辑语法、语义( (续续1)1)2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 表示表示X X经密钥经密钥K K加密后的结果加密后的结果表示表示X X和和Y Y相结合相结合(combined)(combined)；n n它表明它表明Y Y是一个秘密，它的出现可以证明谁发出了是一个秘密，它的出现可以证明谁发出了Y Y消息。消息。n n符号强调突出符

39、号强调突出Y Y扮演着能证明扮演着能证明X X起源的特殊角色。在起源的特殊角色。在具体执行时，具体执行时，X X只是简单的与口令只是简单的与口令Y Y结合。在很多时结合。在很多时候，候，Y Y实际上就是密钥。实际上就是密钥。n n在在BANBAN逻辑中，可能别的工作在这些结构中使用不逻辑中，可能别的工作在这些结构中使用不同的符号。当前这些符号更详细冗长，但更容易读，同的符号。当前这些符号更详细冗长，但更容易读，因此，更适合论文中用很少的公式。因此，更适合论文中用很少的公式。 H(X)H(X)是是X X的单向杂凑函数（哈希的单向杂凑函数（哈希HashHash）值）值BANBAN逻辑语法、语义逻辑

40、语法、语义( (续续2)2)2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑规则：逻辑规则：消息含义（消息含义（消息含义（消息含义（“ “收收收收发发发发” ”）规则）规则）规则）规则 要保证这个规则要保证这个规则是合理的，我们则必是合理的，我们则必须保证须保证P P自己没有说过自己没有说过X X；这就要将公式；这就要将公式XXK K表示成表示成XXK

41、 K from Q from Q，并且要求并且要求QQ不能是不能是P P 消息含义规则消息含义规则消息含义规则消息含义规则关心消关心消息的解释。其中三分息的解释。其中三分之二关心加密消息的之二关心加密消息的解释。它们关心解释解释。它们关心解释如何得到消息源的信如何得到消息源的信任任 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑规则：逻辑规则：消息（

42、消息（消息（消息（“ “发发发发发发发发” ”）规则）规则）规则）规则2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑规则：逻辑规则：消息接收（消息接收（消息接收（消息接收（“ “收收收收收收收收” ”）规则）规则）规则）规则2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经

43、营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑规则：逻辑规则：随机数验证（随机数验证（随机数验证（随机数验证（“ “新鲜新鲜新鲜新鲜信任信任信任信任” ”）规则）规则）规则）规则2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 BANBAN逻辑规则：裁

44、判（逻辑规则：裁判（“ “信任信任” ”）规则）规则 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的形式体系 类类BANBAN逻辑规则：逻辑规则：单向哈希函数规则单向哈希函数规则单向哈希函数规则单向哈希函数规则Q拥有消息X2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行

45、为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法BANBAN逻辑形式推理证明步骤逻辑形式推理证明步骤1.1.给出协议的消息序列描述给出协议的消息序列描述2.2.对协议进行理想化转换对协议进行理想化转换建立协议的理想化模型；建立协议的理想化模型；给出初始假设状态集合给出初始假设状态集合 ；给出预期目标集合给出预期目标集合 ；3.3.分析理想化的协议模型分析理想化的协议模型利用初设和逻辑公设规则对协议系统进行推理利用初设和逻辑公设规则对协议系统进行推理得出状态断言，以及协议所能得到的、关于信任的最终目标得出状态断言，以及协

46、议所能得到的、关于信任的最终目标断言集合断言集合 ；4.4.最后判断结论：若最后判断结论：若 ，则协议可行。，则协议可行。2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法1.协议的消息序列描述n n协议必须首先被描述成自己的消息序列表，协议必须首先被描述成自己的消息序列表，每条消息可典型地写成以下形式：每条消息可典型地写成以下形式：P PQQ: : messagem

47、essage. .这表示这表示P P发送消息给发送消息给QQ。n n消息应按照原设计意图表示成具体执行时的消息应按照原设计意图表示成具体执行时的位串，但非正式的符号。位串，但非正式的符号。2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法2.对协议进行理想化转换对协议进行理想化转换理想化模型理想化模型(2.1.1)(2.1.1)n n由于由于“ “P PQQ: : m

48、essagemessage” ”这种表达经常含糊不清，仍不这种表达经常含糊不清，仍不适合作为形式化分析的基础。因此，需要将协议的每个适合作为形式化分析的基础。因此，需要将协议的每个步骤转换成理想化模型。步骤转换成理想化模型。n n协议的理想化模型中，消息是公式或语句。协议的理想化模型中，消息是公式或语句。例如，协议步骤：例如，协议步骤：AliceAlice告诉告诉Bob(Bob(他知道他知道K Kbsbs) )：我是我是Alice, Alice, K Kabab是她是她(Alice)(Alice)和和他他(Bob)(Bob)之间的通信密钥。之间的通信密钥。2024/8/312024/8/31V

49、R0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法2.对协议进行理想化转换对协议进行理想化转换理想化模型理想化模型(2.1.2)(2.1.2)n n该协议步骤该协议步骤 可理想化为语义：可理想化为语义：n n从从( (A,A,K Kabab) )到到 ，该消息完成了由符号到逻辑语义的，该消息完成了由符号到逻辑语义的协议理想化转换（因为协议理想化转换（因为BANBAN逻辑关心语义推理）。逻辑关心语义推理）。

50、n nBANBAN逻辑忽略明文通信，只是因为明文能被伪造。逻辑忽略明文通信，只是因为明文能被伪造。n n明文对认证协议的作用仅仅是提供在已被加密的消息中明文对认证协议的作用仅仅是提供在已被加密的消息中有哪些信息的线索。有哪些信息的线索。2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法2.对协议进行理想化转换对协议进行理想化转换理想化模型理想化模型(2.1.3)(2.

51、1.3)n n理想化转换后所描述的协议比传统的协议描述更清楚、理想化转换后所描述的协议比传统的协议描述更清楚、详细和规范。建议在设计和描述协议时都使用理想化协详细和规范。建议在设计和描述协议时都使用理想化协议模型。议模型。n n为研究已发表的协议，必须依据形式化的转化规则，为为研究已发表的协议，必须依据形式化的转化规则，为每个协议表述其理想化协议模型。每个协议表述其理想化协议模型。n n理想化的协议模型中不包括明文理想化的协议模型中不包括明文消息；理想化的消息通消息；理想化的消息通常形式为：常形式为： VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经

52、营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法2.对协议进行理想化转换对协议进行理想化转换初始假设初始假设(2.2.1)(2.2.1)n n给出初始假设状态集合给出初始假设状态集合 的形式化描述；的形式化描述；大多情况，协议形式化分析的初始假设如下：大多情况，协议形式化分析的初始假设如下： 协议的初始必须是不变的，以保证协议的初始必须是不变的，以保证每个协议的成功。每个协议的成功。 典型的，初始假设都是陈述两个主典型的，初始假设都是陈述两个主体之间共享什么样的密钥，哪个主体产体之间共享什么

53、样的密钥，哪个主体产生新鲜的随机值，哪个主体在某些特定生新鲜的随机值，哪个主体在某些特定的方式下是可信任的。的方式下是可信任的。 在大多数的情况下，初始假设是标在大多数的情况下，初始假设是标准和明显的。一旦所有的初始假设被写准和明显的。一旦所有的初始假设被写出，验证协议就等同于对作为结论的公出，验证协议就等同于对作为结论的公式做出证明。式做出证明。 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法2.

54、对协议进行理想化转换对协议进行理想化转换预期目标预期目标(2.2.2)(2.2.2)n n给出预期目标集合给出预期目标集合 的形式化描述；的形式化描述；大多情况，协议形式化分析的预期目标如下：大多情况，协议形式化分析的预期目标如下： 认证协议经常是建立某些用认证协议经常是建立某些用共享会话密钥的基础，所以，我们共享会话密钥的基础，所以，我们可得到认证协议的目标这样的结论可得到认证协议的目标这样的结论描述。描述。 因此，如果认为因此，如果认为A A和和B B之间有之间有密钥密钥K K，认证则是完成了，认证则是完成了A A相信相信K K是是A A与与B B之间的通信密钥，之间的通信密钥，B B相信

55、相信K K是是A A与与B B之间的通信密钥。之间的通信密钥。 一些协议可能要求的比这更多一些协议可能要求的比这更多 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法3.分析理想化的协议模型n n利用初设和逻辑公设规则对协议系统进行推利用初设和逻辑公设规则对协议系统进行推理理n n得出状态断言，以及协议所能得到的、关于得出状态断言，以及协议所能得到的、关于信任的最终目标断言集合信任的最终目标断言集合

56、；4.判断结论我们将通过具体的示例讲解以上两步骤2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例1】THE KERBEROS PROTOCOLVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】1.

57、Kerberos1. Kerberos协议协议消息序列描述消息序列描述Message Message 1. 1. MessageMessage 2. 2.MessageMessage 3. 3.Message Message 4. 4. S SA AB BMessage 1Message 1Message 2Message 2Message 3Message 3Message 4Message 4The Kerberos ProtocolThe Kerberos ProtocolVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺

58、诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】2.1 Kerberos2.1 Kerberos协议协议理想化模型理想化模型Message Message 1. 1. MessageMessage 2. 2.MessageMessage 3. 3.Message Message 4. 4. VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务

59、的费用BAN逻辑形式化分析运用【例例1 1】2.2 Kerberos2.2 Kerberos协议理想化模型协议理想化模型初始假设初始假设 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】2.3 Kerberos2.3 Kerberos协议理想化模型协议理想化模型预期目标预期目标 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服

60、务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】3. 3. 分析理想化协议模型分析理想化协议模型The main steps of the proof are as follows: A receives Message 2. The annotation rules yield thatThe main steps of the proof are as follows: A receives Message 2. The annotation rules yield thatholds af

61、terward. Since we have the hypothesisholds afterward. Since we have the hypothesisthe message-meaning rule for shared keys applies and yields the following:the message-meaning rule for shared keys applies and yields the following:One of our rules to break conjunctions (omitted here) then producesOne

62、 of our rules to break conjunctions (omitted here) then producesVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】3. 3. 分析理想化协议模型分析理想化协议模型( (续续1)1)Moreover, we have the following hypothesis(Moreover, we have the following

63、 hypothesis(假假设设): ):The nonce-verification rule applies and yields:The nonce-verification rule applies and yields:Again, we break a conjunction, to obtain the following:Again, we break a conjunction, to obtain the following:Then, we instantiate Then, we instantiate K K to to K Kabab i in the hypoth

64、esis:n the hypothesis:deriving the more concrete:deriving the more concrete:Finally, the jurisdiction rule p3.1 applies, and yields the following:Finally, the jurisdiction rule p3.1 applies, and yields the following:This concludes the analysis of Message 2.This concludes the analysis of Message 2.VR

65、0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】3. 3. 分析理想化协议模型分析理想化协议模型( (续续2)2) A passes the ticket on to B, together with another message A passes the ticket on to B, together with another message containing a time-sta

66、mp. Initially, B can decrypt only the ticket:containing a time-stamp. Initially, B can decrypt only the ticket:Logically, this result is obtained in the same way as that for Logically, this result is obtained in the same way as that for Message 2, via the message-meaning, nonce-verification, and Mes

67、sage 2, via the message-meaning, nonce-verification, and jurisdiction postulates.jurisdiction postulates. Knowledge of the new key allows B to decrypt the rest of Message Knowledge of the new key allows B to decrypt the rest of Message 3. Through the message-meaning(P1.1),the nonce-verification 3. T

68、hrough the message-meaning(P1.1),the nonce-verification postulates(P2.1)and M3, we deduce the following:postulates(P2.1)and M3, we deduce the following:VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例1 1】3. 3. 分析理想化协议模型分析理想

69、化协议模型( (续续3)3) The fourth message simply assures A that B believes in the key and The fourth message simply assures A that B believes in the key and has received As last message. After new applications of the has received As last message. After new applications of the message-meaning and nonce-verif

70、ication postulates to the fourth message-meaning and nonce-verification postulates to the fourth message, the final result is as follows:message, the final result is as follows:If only the first three messages are used, we do not obtainIf only the first three messages are used, we do not obtainThat

71、is, the three-message protocol does not convince That is, the three-message protocol does not convince A A of of B Bs s existenceexistenceA A observes the same messages whether observes the same messages whether B B is running or not. is running or not.VR0304-DOC0-学习讨论：形式化分析方法经营者提供商品或者服务有欺诈行为的，应当按照消

72、费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例2】The Otway-Rees Authentication ProtocolThe Otway-Rees Authentication Protocol经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用ABNc,A,B,Ka(Na,Nc,A,B)KDCM1M2M3M4M5Ka(Na,Nc,A,B)Kb(Nb,Nc,A,B)Nc,Ka(Na,Kab),Kb(Nb,Kab)Ka(Na,Kab)Kab202

73、4/8/312024/8/316464VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例2】The Otway-Rees Authentication ProtocolThe Otway-Rees Authentication Protocol协议协议消息序列描述消息序列描述1. 1. 2. 2. 3. 3. 4. 4. 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分

74、析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例2】The Ottway-Rees Authentication ProtocolThe Ottway-Rees Authentication Protocol协议协议理想化模型理想化模型1. 1. 2. 2. 3. 3. 4. 4. 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为

75、的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例2】The Ottway-Rees Authentication ProtocolThe Ottway-Rees Authentication Protocol协议理想化模型协议理想化模型初始假设初始假设 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形

76、式化分析运用【例2】The Ottway-Rees Authentication ProtocolThe Ottway-Rees Authentication Protocol协议理想化模型协议理想化模型预期目标预期目标 应该考虑：应该考虑：2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例2】The Ottway-Rees Authentication Prot

77、ocolThe Ottway-Rees Authentication Protocol分析理想化协议模型P3.1P3.1P1.1P1.1P2.1P2.12024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例2 2】The Ottway-Rees Authentication ProtocolThe Ottway-Rees Authentication Protoco

78、l分析分析理想化协议模型理想化协议模型( (续续) )同理可得：同理可得：也可推导得出：也可推导得出：但仅可证明：但仅可证明：因为缺少因为缺少VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例2】The Ottway-Rees Authentication ProtocolThe Ottway-Rees Authentication Protocol判断结论可推导得出：可推导得出：但我们仅可证明：但

79、我们仅可证明：并且，并且，N NC C能够代替能够代替N NA A，即：，即：N NA A是不必要的。是不必要的。2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】The Needham-Schroeder ProtocolVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金

80、额为消费者购买商品的价款或接受服务的费用Protocol Analysis in BAN logics1.1.描述协议的每一条消息描述协议的每一条消息(Specify messages of the protocol)(Specify messages of the protocol)2.2.理想化协议理想化协议即即注解协议每条消息为注解协议每条消息为已接收到已接收到的断言形式的断言形式(Idealize the protocol, Annotate protocol. For each (Idealize the protocol, Annotate protocol. For each m

81、essage of the protocol)message of the protocol) P P Q: M Q: M, assert , assert Q Q receivedreceived M M3.3.给出协议的初始信任假设和协议预期的信任目标给出协议的初始信任假设和协议预期的信任目标(Write assumptions about initial state. And asset of Goal)(Write assumptions about initial state. And asset of Goal)4.4.使用使用BANBAN逻辑推导协议主体所能最终拥有的信任逻辑推导

82、协议主体所能最终拥有的信任(Use the logic to derive the beliefs held by protocol (Use the logic to derive the beliefs held by protocol principals.)principals.)2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham

83、-Schroeder Protocol1 1）协议）协议消息序列描述消息序列描述4. 4. 1. 1. 2. 2. 3. 3. 5. 5. 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol2 2） 协议协议理想化模型理想化模型( (注意我们放弃了第一条消息，因为它是明文发送的注意我们放弃了第一条消息

84、，因为它是明文发送的) )M2. M2. M3.M3. M4.M4. M5.M5. 将消息写成将消息写成“ “收到收到” ”形式形式2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol3 3）协议理想化模型）协议理想化模型初始的初始的信任信任假设假设(红色命题红色命题是是NSNS无法达到的无法达到的)

85、)1.1. 2.2. 3.3. 4.4. 5.5. 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol3 3）协议理想化模型，）协议理想化模型，协议预期的协议预期的信任信任目标目标 应该考虑：应该考虑：2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大

86、学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由初始假设由初始假设A.A1A.A1，消息，消息M.2M.2，消息含义公理，得结论，消息含义公理，得结论C.1C.1：2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增

87、加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由初始假设由初始假设A.A3A.A3，结论，结论C.1C.1，从随机数新鲜验证，从随机数新鲜验证- -信任公信任公理得结论理得结论C.2C.2：2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或

88、接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由初始假设由初始假设A.A2A.A2， A.A4A.A4，从仲裁，从仲裁- -信任公理得结论信任公理得结论C.3,C.4C.3,C.4：2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needha

89、m-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由初始假设由初始假设A.B1A.B1，消息，消息M.3M.3，消息含义公理，得结论，消息含义公理，得结论C.5C.5： 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例3 3】the Needham-Schroeder Protocolthe Needham-Schroe

90、der Protocol4 4）分析理想化的协议模型分析理想化的协议模型由结论由结论 A.B5A.B5 ，C.5C.5，随机数验证，随机数验证- -信任公理，得结论信任公理，得结论C.6C.6： NSNS需要不合理的的假设需要不合理的的假设 ，才能继续，才能继续 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例3 3】the Needham-Schroeder

91、 Protocolthe Needham-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由结论由结论 C.6C.6 ，初始假设，初始假设A.B2A.B2， A.B4A.B4 , , 仲裁仲裁- -信任公理，得结论信任公理，得结论 C.7C.7 ： 其中其中 C.7C.7 是是BobBob获得的获得的 而而AliceAlice则假设则假设TrentTrent能够控制能够控制K KABAB的新鲜性来得到的新鲜性来得到2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者

92、服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由结论由结论C.3C.3，消息，消息M.4M.4，消息含义公理，得结论，消息含义公理，得结论C.8C.8： 2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价

93、款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4 4）分析理想化的协议模型）分析理想化的协议模型由结论由结论C.4C.4，C.8C.8，消息新鲜，消息新鲜- -信任公理，得结论信任公理，得结论C.9,C.10C.9,C.10： 同理，由同理，由 A.B5A.B5, ,可得结论可得结论2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的

94、费用BAN逻辑形式化分析运用【例例3 3】the Needham-Schroeder Protocolthe Needham-Schroeder Protocol4 4）分析理想化的协议模型：判断结论）分析理想化的协议模型：判断结论由以下结论组成及关于协议的最终断言由以下结论组成及关于协议的最终断言 : :但我们无法得到但我们无法得到 证毕2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用B

95、AN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4）分析理想化的协议模型：判断结论 分析过程，可发现协议主体分析过程，可发现协议主体B B关于随机数关于随机数N NB B的新鲜信任的新鲜信任 B B believes fresh( believes fresh(N Nb b) ) 也就是也就是 ，是不需要的。，是不需要的。 协议推导得出的结论完全用不着协议推导得出的结论完全用不着N NB B. .2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为

96、的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needham-Schroeder Protocol4 4）分析理想化的协议模型：判断结论）分析理想化的协议模型：判断结论 从从 Trent Trent 对对 Alice Alice 说说(saying)(saying)的消息的消息2 2： , , 我们能够我们能够以同样的方式证明以同样的方式证明 ，但是，但是，BobBob得到的共享密钥含义得到的共享密钥含义 是来自是来自AliceAlice的消息的消息3 3，其中并没有关联上，其中并没有关联上TrentT

97、rent的声明、以的声明、以便于便于BobBob知道密钥是新鲜的知道密钥是新鲜的 ( (即消息可能是旧的即消息可能是旧的, ,被伪造被伪造, ,重放重放) ) 。 由于由于NSNS协议无法令协议无法令 ，因此，我们无法让，因此，我们无法让BobBob获得获得比比 更多的信任了。更多的信任了。2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例3】the Needha

98、m-Schroeder Protocol判断结论(Needham-Schroeder Needham-Schroeder 已被揭露的漏洞已被揭露的漏洞已被揭露的漏洞已被揭露的漏洞)分析结果正确地指出，分析结果正确地指出，Needham-SchroederNeedham-Schroeder协议存在的漏洞协议存在的漏洞: : Mallory (Mallory (伪装者伪装者) )能够记录能够记录AliceAlice和和 BobBob之间交换的密钥，并在他选之间交换的密钥，并在他选择的任意时间内，哄骗择的任意时间内，哄骗BobBob接受第三条消息中的接受第三条消息中的( (旧的，可能已被破旧的，可能

99、已被破解的解的) )密钥密钥. .无论如何，当无法回复无论如何，当无法回复BobBob的时候，的时候， MalloryMallory就可以阻碍掉来自就可以阻碍掉来自BobBob的第四条消息的第四条消息. .但且但且Mallory Mallory 能够能够提供一个消耗数年提供一个消耗数年CPUCPU时间破解所得到的时间破解所得到的K KAB AB ，之时，之时，他就能令他就能令BobBob接受并使用一个陈年的旧密钥接受并使用一个陈年的旧密钥. .2024/8/312024/8/31VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺

100、诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析运用【例例3 3】the Needham-Schroeder Protocolthe Needham-Schroeder ProtocolppDenning-Sacco AttackDenning-Sacco Attackn n假使攻击者拥有泄露的旧会话密钥，结果会怎样呢？从第假使攻击者拥有泄露的旧会话密钥，结果会怎样呢？从第3 3条消息条消息开始开始3.3.E EA A B: Kab B: Kab , A, AKbs Kbs 4.4.B B E EA A: Nb: Nb

101、KabKab5.5.E EA A B: Nb B: Nb 1 1 KabKabn n其中，其中，E EA A - - 攻击者攻击者/ /入侵者入侵者/ /渗透者渗透者/ /偷听者偷听者/ /间谍：间谍：Eve Eve 冒充成冒充成 AliceAlice2024/8/312024/8/31经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的存在问题协议的理想化过于依赖分析时的直觉，协议的理想化使得在原始协议与理想化协议之间存在一个潜在的语义鸿沟。Ban逻辑分析的正确性严重依赖于前几步，但前三步在有效达成目标

102、上存在问题。即使对协议行为做出了准确的解释，也不能保证能够正确理解协议设计者的真正意图，因而虽然对主体行为的理解不存在任何歧义，但仍可能存在对同一协议有两种理想化的结果。BAN不够完备，即BAN逻辑不能查出协议的所有问题，只能证伪。2024/8/312024/8/319191经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的缺陷BAN逻辑系统没有为协议理想化过程提供标准的转换格式，这就使得对同一个协议由于分析者的不同理解而得到不同的理想化版本。不合理的假设认为参与协议运行的主体都是诚实的。实际上许多合理

103、协议并不满足主体诚实性假设，且诚实概念也缺乏良好规范的定义初始状态假设难以确定，而假设对分析结论的正确得出至关重要。没有形式化规则来确定假设，从而无法确认和自动验证假设的正确性和有效性。2024/8/312024/8/319292经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑的设计准则 BAN逻辑为认证协议的设计提供了可参考的准则。认证主体用会话密钥加密另一个认证主体所知的明文信息，来表示已获得了会话密钥。协议中会话密钥的使用必须以新鲜性为保证，以防密钥重放。认证协议中，在传送包含关键的敏感信息的消息

104、中，尽可能以显式表现出参与协议的各个主体，使接收的主体能清晰地意识到其它主体的存在。在协议中可信服务器的信仰很重要，因此区分服务器作用的强弱是十分必要的。2024/8/312024/8/319393经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO逻辑1994年Syverson和Orschot提出了SVO逻辑，它的出现标志着BAN及BAN类逻辑的成熟。1996年，他们又在SVO逻辑的公理，以及语义上有进行了更准确的定义。SVO逻辑吸收了BAN类逻辑系统的优点，同时又具有十分简洁的推理规则和公理。它为逻辑系统建

105、立了用于推证合理性的理论模型。在形式化语义方面，它具有极好的扩展能力。2024/8/312024/8/319494经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO逻辑的基本结构 定义T为初始术语集合，包括互不相交的常量符号集合：主体、共享密钥、公钥、私钥以及序列号等。基于此，n维函数表示有n个变量的函数，如加、解密函数等。SVO逻辑将语言划分为集合T上的消息语言MT和公式语言FT。消息语言MT 是满足下列性质的最小语言集合：1.如果XT，则X是消息。2.如果X1，Xn是消息，F是任意一个n维函数，则F(X1

106、，Xn)是消息。3.如果是公式，则是消息。 2024/8/312024/8/319595经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO逻辑的基本结构公式语言FT是满足下列性质的最小公式集合：1.如果P是原始命题，则P是公式。2.如果，是公式，则和是公式。3.P believes 和P controls 是公式，其中P是主体，是公式。4.P sees X，P says X，P said X，P received X和fresh(X)是公式，其中P是主体，X是消息。5. Shared(P，K，Q)，PK(P，

107、K)，PK(P，K) ，PK(P，K)和P has K是公式，其中P是主体，K是密钥。（其中PK(P，K)指公开密钥，K是主体P的公钥，而K1指相应的私钥。PK(P，K)，PK(P，K) ，PK(P，K)分别表示用于加密，签名和密钥协商的公开密钥。）SV(X, K, Y) 是公式，其中X，Y是消息，K是密钥。（SV(X, K, Y)指签名验证，即X为签名后得到消息，K为签名验证密钥，Y为被签名的消息。）2024/8/312024/8/319696经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO Notati

108、on P says X: X is a message P said recently.Like BAN P said X but must P must have said X since beginning of current epoch.P has X: X is a message P can see. Initially available to PReceived by PFreshly generated by PConstructible by P from the above2024/8/312024/8/319797经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求

109、增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用PK(P,K): K is a public key of P. The matching secret key K-1 will never be discovered by any principal but P or a principal trusted by P. Original BAN notion is refined to cover different types of public key functionality.PKy(P,K): K is a public ciphering key of

110、P. Only P can read messages encrypted with K.PKs(P,K): K is a public signature key of P. K verifies messages signed by K-1 are from P.PKd(P,K): K is a public key-agreement key of P.A Diffie-Hellman key formed with K is shared with P.2024/8/312024/8/319898经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金

111、额为消费者购买商品的价款或接受服务的费用XK: X signed with key K.Notationally distinguish: Encrypted messages from signed messages.XK: Not short for XK from P . No longer assume: Principals can recognize own messages. Still assume: Encryption messages are uniquely readable and verifiable as such by holders of the right

112、keys. X *p: X according to P.Used for messages that P doesnt know/recognizeExample: XK where P does not know KP will recognize XK *p as the same thing if received again.2024/8/312024/8/319999经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO逻辑的推理规则及公理SVO逻辑遵从两条基本推理规则：Modus Ponens (M

113、P)：( )Necessitation (Nec)： P believes SVO逻辑共有20条公理：2024/8/312024/8/31100100经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I1相信公理 (Believing)对于任一主体P和公式，有：Ax1：P believes P believes ( ) P believes Ax2：P believes P believes (P believes )公理Ax1表示主体相信由其已有的信任关系逻辑推导出的所有信仰结果。公理Ax2表示主体表明其信任的是

114、什么。2024/8/312024/8/31101101经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I2源关联公理 (Source Association Keys)密钥用于推断消息发送者的身份。Ax3：shared(P，K，Q)R received XQk Q said X Q sees X Ax4：(PK(Q，K)R received X SV(X, K,Y) Q said X 公理Ax3中上标Q暗示消息是Q产生并发送的，而不是P。 公理Ax4中PK(Q，K)表示K是主体Q的数字签名验证密钥。此公理表明如果

115、主体R收到一个签名消息，并且R知道签名的验证公钥是K，它就可以确认消息发方的身份。2024/8/312024/8/31102102经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I3密钥协商公理 (Key Agreement)会话密钥是由密钥协商密钥是良好的得到的。Ax5：(PK(P，Kp)PK(Q，Kq) shared(P，Kp,q，Q)Ax6： F0(K,K) / F0(K,K)公理Ax5中KpqF0(Kp，Kq1 )F0(Kp-1,Kq)，F0指密钥协商函数，如Diffie-Hellman密钥交换。F0(K

116、, K ) implicitly names the (Diffie-Hellman) function that combines K with K-1 to form a shared key.公理Ax6中PK(R，KR)表示KR是R用于密钥协商的公开密钥，而KR-1是R保存的秘密密钥。该公理表示两个公式逻辑上是相等的。也就是说，逻辑注意到密钥协商的对称性。2024/8/312024/8/31103103经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I4接收公理 (Receiving)主体对接收到的一个级联

117、的加密消息并用有效的密钥解密。Ax 7：P received (X1，Xn) P received XiAx 8：P receivedXk P sees K1 P received XAx 9：P received Xk P received X其中Xk 表示标准的加密模式，Xk 表示被签名的消息。AX9中，Principals are assumed to possess public keys (for convenience)2024/8/312024/8/31104104经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或

118、接受服务的费用I5看到公理 (Seeing) 主体只要接收到一个消息就看到了这个消息，并且看到了这个消息的每一部分。主体还可以看到从已看到的消息计算得到的消息。Ax10：P received X P sees XAx11：P sees (X1，Xn) P sees XiAx12：P sees X1 P sees Xn P sees (F (X1，Xn)2024/8/312024/8/31105105经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I6理解公理 (Comprehending) 如果一个主体理解一个消

119、息，并看到此消息的一个函数，那么它理解它所看到的。Ax13：P believes (P sees F(X) P believes (P sees X)F可视为加解密函数，K为参数。2024/8/312024/8/31106106经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I7叙述公理 (Saying)一个主体说过一个级联消息，那么它一定说过且看到消息的每一部分。Ax14：P said (X1，Xn) P said Xi P sees XiAx15：P says (X1，Xn) P said (X1，Xn) P

120、 says Xi2024/8/312024/8/31107107经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I8仲裁公理 (Jurisdiction)Ax16：P controls P says 2024/8/312024/8/31108108经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I9新鲜公理 (Freshness)如果消息的一部分是新鲜，那么整个消息也是新鲜的。有关新鲜消息的任何一对一函数（如加密解密函数）也是新鲜的

121、。Ax17：fresh(Xi) fresh(X1，Xn)Ax18：fresh(X1，Xn) fresh(F(X1，Xn)F must genuinely depend on all components F genuinely depends on the value of X infeasible to compute value of F withoutvalue of X 随机数-验证公理 (Nonce-Verification)新鲜性促使已经被说的消息为当前时间点所说的消息。Ax19：fresh (X)P said X P says X2024/8/312024/8/31109109经

122、营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I11共享密钥的良好对称性公理( Symmetric goodness of shared keys)如果K是P、Q之间的良好密钥当且仅当K是Q、P之间的良好密钥。Ax20：shared(P，K，Q)shared(Q，K，P) 2024/8/312024/8/31110110经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用I12 所有公理P has K P sees K2024/8/31

123、2024/8/31111111VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用BAN逻辑形式化分析方法BANBAN逻辑形式推理证明步骤逻辑形式推理证明步骤1.1.给出协议的消息序列描述给出协议的消息序列描述2.2.对协议进行理想化转换对协议进行理想化转换建立协议的理想化模型；建立协议的理想化模型；给出初始假设状态集合给出初始假设状态集合 ；给出预期目标集合给出预期目标集合 ；3.3.分析理想化的协议模型分析理想化的协议模型利

124、用初设和逻辑公设规则对协议系统进行推理利用初设和逻辑公设规则对协议系统进行推理得出状态断言，以及协议所能得到的、关于信任的最终目标得出状态断言，以及协议所能得到的、关于信任的最终目标断言集合断言集合 ；4.4.最后判断结论：若最后判断结论：若 ，则协议可行。，则协议可行。2024/8/312024/8/31经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO逻辑形式化分析步骤SVO逻辑的协议句法分析技术与BAN逻辑的分析技术同属于推理结构的分析方法。但SVO逻辑不需要BAN逻辑的协议理想化过程，而重点具体化了协

125、议前提的确定过程。SVO逻辑对协议的形式化分析分为以下三步：1.给出协议所基于的前提。2.形式化说明协议将达成的安全目标。3.运用公理和推理规则及其前提，从协议的前提进行推证直至验证协议是否满足其最终运行目标。2024/8/312024/8/31113113经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用SVO逻辑协议前提分类第一类前提是初始假设，即在协议的初始状态时就为真的假设。例如每个主体对其产生的随机数的新鲜性的信任；主体对其与服务器共享的长期密钥的良好性的信任；主体关于服务器对它发送的密钥的质量和新鲜性具

126、有权威的信任等。如：消息SA：Ts, B, Ka,bKa,s第一类前提有：A believe fresh(Ts)；A believe S controls share(A, Ka,b ,B) ；A believe share(A, Ka,s, S)第二类前提反映主体对在协议运行期间发送的消息的接收，可以直接从协议描述得到。在证明过程中经常不使用这类前提，但它们有助于形成后边的前提。如：上例为 A received Ts, B, Ka,bKa,s2024/8/312024/8/31114114经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买

127、商品的价款或接受服务的费用SVO逻辑协议前提分类第三类前提反映每个主体对其收到消息的理解。主体不可能完全理解其所收到的消息的每一部分。如由于分发（distributed）密钥具有随机性，故收到它的主体（而不是产生它的主体）必然不能理解它（unrecognizable）。通过考虑主体对其在第二类前提中的接收到子消息的理解，很容易得到这一类前提。如：上例为 A believes A received Ts, B, *s Ka,s 第四类前提反映接收主体对收到消息加入的解释。这是BAN逻辑中理想化步骤的主要替代部分（primary replacement）。这类前提还与具体协议的特征有关。如: 上例

128、为 A believes （A received Ts, B, *s Ka,s A received Ts, B, share(A, Ka,b ,B),fresh(Ka,b) Ka,s）2024/8/312024/8/31115115经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用一个不可否认协议实例不可否认协议的实现包括证据的生成、证据的交换、证据的验证以及纠纷的解决，方法一般有两种：一是双方进行同时（或接近同时）的秘密交换;另一种借鉴可信第三方（TTP）。经常采用TTP方式。2024/8/312024/8/3

129、1116116经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用不可否认协议提供的证据两个基本证据：NRO（Non-repudiation of Origin)发方不可否认。用于证明发方的确发送了消息，由发方提供。NRR（Non-repudiation of Receipt)收方不可否认。用于证明收方的确收到了消息，由收方提供。如有TTP介入，则还需要下面两个证据：NRS（Non-repudiation of Submission)提交不可否认。用于证明已提交给了TTP，由提交方提供。NRD（Non-repudia

130、tion of Delivery)传递不可否认。证明TTP已交给了意定的接收者，由TTP提供。2024/8/312024/8/31117117经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用ZG不可否认协议Zhou和Gollmann在文献5提出了一个不可否认协议（ZG协议），具体描述为：M1 AB： fNRO,B,L,C,NROM2 BA: fNRR,A,L,C,NRRM3 ATTP: fNRS,B,L,K,NRS_KM4 BTTP: fNRD,A,B,L,K,NRD_KM5 ATTP: fNRD,A,B,L,K

131、,NRD_KA:不可否认协议交换的发起者。B：不可否认协议交换的接收者。TTP：可提供网络服务的在线可信第三方。M：A发送给B的消息。C：A发送给B的密文。K：A定义的消息密钥。L：协议轮标志SI：表示主体I的签名私钥。fNRO,fNRR,fNRS及fNRD:用于标识生成特定消息的协议步骤的标志，为方便起见记为f1,f2,f3,f4.: ftp操作符。NROSA(fNRO,B,L,C)NRR=SB(fNRR,A,L,C)NRS_K=SA(fNRS,B,L,K)NRD_K=STTP(fNRO,A,B,L,K)2024/8/312024/8/31118118经营者提供商品或者服务有欺诈行为的，应当

132、按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议的运行过程消息M的传输分两步：首先由A将消息的密文传给B，在A收到B对此消息的回执后通过可信第三方将K发给B。协议的运行过程为：1.在M1中，A将CK（M）、轮标志L、意定接收者的标识以及NRO发送给B，B将之作为用于证明A在L轮协议发送C的证据。2.B返回一个签名消息NRR用于证明在L轮中收到C。这为A提供了C已被B收到的证据。3.A将K以及一个提交不可否认证据NRS_K发送给TTP4.在M4和M5中，A和B通过ftp操作从TTP处得到一个已先期存放的密钥K以及由TTP签发的传递不可否认证据NRD_

133、K.2024/8/312024/8/31119119经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用如果A希望证明消息已被对方接收，它可向仲裁出示证据：SB(f2,A,L,C)和STTP(f4,A,B,L,K)。前者证明B收到了C，后者证明K已在TTP中，因此意味着B能够得到K并进而得到M。如果B希望证明消息已被发送，它可向仲裁出示证据：SA（f1,B,L,C)和STTP（f4,A,B,L,K)。前者表明C已被A发送，后者证明K也已被发送给了TTP。L表明C和K是在同一轮协议中的。2024/8/312024/8/

134、31120120经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议公平性：从协议执行的开始到协议执行结束的任何一个阶段，通信的双方要么能够同时得到它们所期望的，要么任何一方都得不到有利于自己的信息，从而避免协议的任一方中断执行的协议，或否认其已发生的行为以达到利益不平等的可能。一个协议的不可否认性成立，如果：1.协议任何一步执行后的中止将不会破坏通信双方主体的地位的公平性。2.在协议结束时提供主体参与协议行为的有效证据，即证据的有效性。2024/8/312024/8/31121121经营者提供商品或者服务有欺诈

135、行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用证明ZG协议的不可否认性。1.给出协议前提与假设 A0基本假设：协议的运行环境是不安全的。 A1:每个主体的公钥是公开的。 A2:每个主体的私钥仅为其所知。 A3:TTP believes SA A4: TTP believes SB A5: P believes STTP (P为参与协议运行的主体） A6:TTP believes (B received C) TTP believes(A said C) A7: A said (A,B,L,Ek(M) A said(A,B,L,K) A s

136、aid M A8: B received (A,B,L,Ek(M) B received(A,B,L,K) B received M A9:TTP believes (A said C B received C TTP received K) TTP says K A9表示TTP只有在确信A已说过C，并且B收到了C，以及TTP收到了K，才将K公布到其公开目录中 2024/8/312024/8/31122122经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用A10: TTP says X P ftp X P see

137、s XTTP将其认为是有效的数据放入其公共目录下，并可为任何主体通过ftp操作访问。A11：P believes PK(Q,K) (Q,K) P received Xk-1 P believes(Q said X)A11表示P如果收到一个签名消息，并且P相信这个签名密钥是Q的，则P相信Q说过X。这个假设是AX4的一个扩展。A12:A believes fresh(Na)A13:TTP believes 2024/8/312024/8/31123123经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用2.说明协议目标

138、 根据不可否认协议所要达成的公平性和证据有效性，ZG协议的目标描述如下： 一般目标：G1 A believes (B received M) G2 B believes (A said M) 仲裁目标：G3 J believes (A said M) G4 J believes (B received M)2024/8/312024/8/31124124经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用3. 运用规则和公理进行推证 由M1得： F1：B received SA(fNRO,B,L,C) 由F1,A2,

139、AX4,A11得：F2：B believes(A said(fNRO,B,L,C) 由F2，AX14得：F3：B believes(A said C)由M2得：F1：A received SB(fNRR,A,L,C) 由F1，A2，AX4，A11得F2：A believes (B said(fNRR,A,L,C) 由F2，AX14得： F3: A believes (B said C) 但分析不出主体A关于B从A处接收到C的信仰，其原因是不能保证B所说的C一定就是从A所收到的那个C。2024/8/312024/8/31125125经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿

140、其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用故在原协议的NRO与NRR中增加新鲜随机数,修改如下：1)AB:fNRO,B,L,C,SA(fNRO,B,L,Na,C)2)BA:fNRR,A,L,C,SB(fNRR,A,L,Na+1,C)由于有了随机数Na,所以就能保证B发出的C就是它刚刚接收到的那个C2024/8/312024/8/31126126经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用对修改后的协议进行分析。由消息M2得：F4：A received SB(fNRR,A,L,Na+1,

141、C)由F4，A2，AX4，A11，A12，M1得：F5：A believes (B received (fNRR,B,L,Na,C) A believes (B received C) 由M3得：F6: TTP received SA(fNRS,B,L,K)由F6，A2，A3得：F7：TTP believes (A said (fNRS,B,L,K) TTP received K 2024/8/312024/8/31127127经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用根据假设A9，TTP只有确信A已说过C

142、，并且B收到C，以及TTP收到了K，才能将K公布到其公开目录中，但在原有协议中，TTP并不能确知B是否已收到了C，因此，A可对NRR进行签名，并将结果发给TTP。对M3进行修改如下：M3 ATTP：fNRS,B,L,K,NRS_K,SA(NRR)TTP收到M3后由AX7得：F8：TTP receives SA(NRR)由F8，A3，A11，M1得：F9：TTP believes (A said C B received C)由F8，F9，A9，M3得：F10：TTP says K由F10，A10，M4得：F11：B received(fNRD,A,B,L,K,STTP(fNRO,A,B,L,K

143、)由F11，F9，AX7，A13得：F12：(B received K B received C) B received M2024/8/312024/8/31128128经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用由M5得：F13：A received (fNRD,A,B,L,K,STTP(fNRO,A,B,L,K)由F10，F12，F13，A5，A11，NEC得：F14：A believes(TTP says K) A believes(B sees K) A believes (B received M

144、)得证G1.由F7，F11，A5得：F15：B believes(TTP says K) B believes(A said K)由F3，F15得：F16：B believes(A said M)得证G2.2024/8/312024/8/31129129经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用如出现主体否认其协议行为，并引发纠纷，双方则可按要求J出示证据，通过证明协议仲裁目标的满足与否来检验主体否认行为的不可否认性。假设J相信主体A、B和TTP的签名私钥，并且知道与私钥对应的主体公钥。协议可能发生两种纠纷

145、情况：A否认向B发送了消息M。2024/8/312024/8/31130130经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用协议可能发生两种纠纷情况：A否认向B发送了消息M。B 将M，C，K，L及NRO、NRD_K提交给J。1.检查NRD_K是用T的私钥对(fNRO,A,B,L,K)的签名。J received STTP(fNRO,A,B,L,K) J believes(TTP says K) J believes(A said K)2.检查NRO是用A的私钥对（fNRO,B,L,Na,C)的签名。J rece

146、ived SA(fNRO,B,L,Na,C) J believes(A said C)3.检查MD（K：C）J believes(A said M)得证G3.2024/8/312024/8/31131131经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用B否认收到了M。A将M，C，K，L及NRR，NRD_K提交给J.1.检查NRD_K是用TTP的私钥对(fNRO,A,B,L,K) 的签名。J received STTP (fNRO,A,B,L,K) J believes(TTP says K) J believe

147、s (B received K)2.检查NRR是用B的私钥对(fNRO,A,L,Na+1,C)的签名。J received SB (fNRO,A,L,Na+1,C) J believes(B received C)3.检查MD（K：C）J believes (B received M)得证 G4. 2024/8/312024/8/31132132经营者提供商品或者服务有欺诈行为的，应当按照消费者的要求增加赔偿其受到的损失，增加赔偿的金额为消费者购买商品的价款或接受服务的费用引用文献1 陆钟万. 面向计算机科学的数理逻辑(第二版). 北京：科学出版社，20022 Paul Syverson, P

148、aul C Van Oorshot. On unifying Some Cryptographic Protocol LogicsC.In 1994 Computer Society Symposium on Research in Security and Privacy, IEEE ComputerScoiety1994.14-283 Paul Syverson, Paul C Van Oorshot. A unified Cryptographic Protocol Logics. Manuscript, Dec 19964 李肖坚，形式化分析方法BAN逻辑及其运用示例，2003年7月5 范红、冯登国，安全协议理论与方法，科学出版社，2003年10月6 J.Zhou and D.Gollmann. A fair non-repudiation protocol. In IEEE Computer Society Symposium on Research in Security and Privacy,19962024/8/312024/8/31133133