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

1、 第十五章 安全协议的形式化分析技术 逻辑推理 形式化语言 形式化分析方法 形式化分析方法应用 逻辑推理 由前提推出结论。前提和结论都是命题。 命题的真或假由命题的内容是否符合客观实际确定。 演绎逻辑 当前提的“真”蕴涵结论的“真”，称前提和结论之间有可推导性关系。即前提和结论之间的推理是正确的。 研究怎样的前提和结论之间具有可推导性关系。 归纳逻辑 只要求得到的结论本身是协调的，与前提是协调的。 前提的“真”并不蕴涵结论的“真”。 逻辑推理的正确性 命题的内容：“真”/“假”，内容决定命题的“真”/“假”。 命题的形式：即逻辑形式。由内容抽象出来。 逻辑形式决定前提和结论的之间的可推导性关系

2、。 不关心前提和结论的真假，而关注前提的真是否蕴涵结论的真。 形式语言 使用自然语言陈述并分析命题常常引出歧义。 需要构造一种符号语言形式语言，描述由命题内容抽象出来的命题逻辑形式。 形式语言使用符号来构造公式 由公式来精确地表示命题的逻辑形式 语义和语法 语义涉及符号和符号表达式的涵义(给符号某种解释) 语法涉及符号表达式的形式结构，但不考虑任何对形式语言的解释。 形式语言的语义和语法既有联系，又有区分。 集合论 数理逻辑 图论：有限状态图 网论：Petri网模型 代数系统：代数系统形式化模型 安全协议的基本概念安全协议特指使用密码学技术的密码协议所谓协议，就是两个或者两个以上的参与者为完成

3、某项特定的任务而采取的一系列步骤。 协议的定义包含三层含义：1. 协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之前，后面的步骤不可能执行；在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤。2. 协议至少需要两个参与者；一个人可以执行一系列的步骤来完成一项任务，但它不构成协议。3. 通过协议必须能够完成某项任务。 安全协议使用密码学技术，协议参与者可能是可以信任的人，也可能是攻击者和完全不信任的人。密码协议包含某种密码算法。 网络通信中常用的密码协议按照其完成的功能分成以下四类： 密钥交换协议 在参与协议的两个或者多个实体之间建立共享的秘密通道，常用于建立在一次通信中

4、所使用的会话密钥。协议可以采用对称密码体制，也可以采用非对称密码体制，例如Diffie-Hellman密钥交换协议。认证协议 认证协议中包括实体认证（身份认证）协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。认证和密钥交换协议 协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。常见的有Needham-Schroeder协议、分布认证安全服务（DASS）协议、ITU-T X.509认证协议等等。电子商务协议 电子商务协议中，主体利益目标往往是不一致的，电子商务协议关注的就是公平性，即协议应保证交易双方都不能通过损害对方利益而得到它不应得的利

5、益。常见的电子商务协议有SET协议等。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 介于应用层和传输层之间 为上层提供安全性IPSSL ChangeCipher SpecProtocolSSL AlertProtocolApplication ProtocolTCPSSL R

6、ecordProtocolSSL HandshakeProtocolHTTPLDAPIMAP 协议分为两层 上层：TLS握手协议、TLS密码变化协议、TLS警告协议 底层：TLS记录协议 上层协议是用于管理SSL密钥信息的交换，下层提供基本的安全服务 TLS握手协议 客户和服务器之间相互认证 协商加密算法和密钥 它提供连接安全性，有三个特点 身份认证，至少对一方实现认证，也可以是双向认证 协商得到的共享密钥是安全的，中间人不能够知道 协商过程是可靠的 TLS记录协议 建立在可靠的传输协议(如TCP)之上 它提供连接安全性，有两个特点 保密性，使用了对称加密算法 完整性，使用HMAC算法 用来封

7、装高层的协议 信息在信息在InternetInternet上的安全传输，保证网上传输的上的安全传输，保证网上传输的数据不被黑客窃听数据不被黑客窃听 订单信息和个人账号信息的隔离，在将包括消费订单信息和个人账号信息的隔离，在将包括消费者账号信息的订单送到商家时，商家只能看到订者账号信息的订单送到商家时，商家只能看到订货信息，而看不到消费者的账户信息货信息，而看不到消费者的账户信息 消费者和商家的相互认证，以确定通信双方的身消费者和商家的相互认证，以确定通信双方的身份，一般由第三方机构负责为在线通信双方提供份，一般由第三方机构负责为在线通信双方提供信用担保信用担保 要求软件遵循相同的协议和消息格式

8、，使不同厂要求软件遵循相同的协议和消息格式，使不同厂家开发的软件具有兼容和互操作功能，并且可以家开发的软件具有兼容和互操作功能，并且可以运行在不同的硬件和操作系统平台上运行在不同的硬件和操作系统平台上Desktop computerCard HolderHow SET with Credit Card WorksServerMerchant ServerAcquiring BankCard Issuer Bank876543219CACertificate Authority00- cardholder registration132- purchase request- merchant p

9、asses signed, encrypted authorization to the acquirer for check- card validation with issuer4- issuer 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 g

10、ets paid9- cardholder receives bill from card issuer 如果将安全协议所处环境视为一个系统，那么这个系统中，一般而言包括一些发送和接收消息的诚实的主体和一个攻击者，以及用于管理消息发送和接收的规则。诚实主体诚实主体诚实主体诚实主体环境/攻击者通信通信通信通信 评估一个安全协议是否安全就是检查其所欲达到的安全性质是否遭到攻击者的破坏。 认证性 声称者使用仅为其与验证者知道的密钥封装的一个消息 声称者使用私钥对消息签名，验证者使用公钥来验证 声称者通过可信第三方来证明自己。 秘密性 保护协议消息不被泄露给非授权拥有此消息的人，即使是攻击者观测到了消

11、息的格式，它也无法从中得到消息的内容或提炼出有用的信息。 保证协议消息秘密性的最直接的方法是对消息进行加密。 安全协议中，一般不考虑具体的密码算法的执行细节，但在实际应用中这往往有可能造成协议秘密性的缺陷。 完整性保护协议消息不被非法篡改、删除和替代。常用的方法有封装和签名SSL和IKE等协议中就涉及到保护协议消息完整性的具体实现细节 不可否认性目的是通过通信主体提供参与协议交换的证据来保证其合法利益不受侵害，即协议主体必须对自己的合法行为负责，而不能也无法事后否认。协议必须具有两个特点：证据的正确性、交易的公平性。在不可否认性之中还可引申出其他一些相关性质，如适时中止性、公平性、可追究性等。

12、 安全协议的安全性 安全协议是许多分布式系统安全的基础，确保这些协议的安全运行是极为重要的。 安全协议有若干几个消息传递，消息之间存在着复杂的相互作用和制约； 协议中使用多种不同的密码体制， 目前的许多安全协议存在安全缺陷。原因有两个： 协议设计者误解或者采用了不恰当的技术； 协议设计者对环境要求的安全需求研究不足。 对协议的安全性进行分析和研究是一个重要的课题。 S.Gritzalis和D.Spinellis根据安全缺陷产生的原因和相应的攻击方法对安全缺陷进行了分类：基本协议缺陷： 协议设计中没有或很少考虑防范攻击者。口令/密钥猜测缺陷： 弱口令导致攻击者能够进行口令猜测攻击；或者弱密钥使攻

13、击者能够破解该密钥。 陈旧（stale）消息缺陷： 协议设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等等。 并行会话缺陷 协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的重要消息。 内部协议缺陷 协议可达性存在问题，协议的参与者中至少有一方不能够完成所有必须的动作而导致缺陷。 密码系统缺陷 协议中使用的密码算法的安全强度导致协议不能完全满足所要求的机密性、认证等需求而产生的缺陷。 安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存在安全缺陷。 从安全协议的分析和设计角度来看，应当对协

14、议的安全性作出认真的分析和验证。 安全协议的分析方法攻击检验方法；形式化的分析方法。 攻击检验方法 搜集使用目前的对协议的有效攻击方法，逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力。 在分析的过程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析。 这种分析方法对已知的攻击非常有效的。 不能发现协议中未知的安全隐患。 形式化的分析方法 采用各种形式化的语言或者模型，为安全协议建立模型，并按照给定的假设和规则，分析、验证方法证明协议的安全性。 近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。 形式化的分析方法是目前研究的热点，但是

15、就其实用性来说，还有待进一步突破。 安全协议的形式化分析有助于： 界定安全协议的边界，即协议系统与其运行环境的界面 更准确地描述安全协议的行为。 更准确地定义安全协议的特性。 证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。1）通用的形式化描述语言 使用通用的、不是为分析安全协议专门设计的形式化描述语言和协议校验工具建立安全协议的模型并进行校验。主要思想是将安全协议看作一般的协议，并试图证明协议的正确性。 采用的工具和模型与验证一般协议的类似，例如使用有限状态图、Petri网模型、LOTOS语言等等。 方法的主要缺点是仅证明协议的正确性而不是安全性。2）专家系统 设计专用的

16、专家系统来制定安全协议的校验方案并进行协议检验，从而对协议的安全性作出结论。 主要思想是针对所设计的协议而开发专用的专家系统，通过专家系统发现协议是否能够达到不合理的状态（比如密钥的泄露等等）。 这种技术能够识别缺陷但是不能证明协议的安全性，也不能发现未知的缺陷。3）安全需求模型 基于知识和信任逻辑，针对具体协议建立相应的形式化安全需求模型 依据给定的逻辑初设和公理规则对该模型进行形式化分析推理 通过推理获取的结果来推断协议能否完成预期的目标、证明协议结论的正确性。 形式系统的组成（初始符号、形式规则、公理、变形规则） 这种方法是目前为止使用最广泛的一种方法，最著名的是BAN逻辑。BAN逻辑是

17、基于知识和信任的形式逻辑模型，进行基于知识和信任的分析。BAN逻辑假设协议的安全是完整性和新鲜度的函数，使用逻辑规则来对协议的属性进行跟踪和分析。 通常，BAN逻辑只能推出给定初设的协议结果，对一般的安全性的证明依赖于给定攻击模型的初设。 使用BAN逻辑分析安全协议的步骤如下：协议的理想化转化；假设所有的协议初始状态；使用逻辑规则对系统的状态作出断言；运用逻辑原理得到关于信任的断言；4）代数系统形式化模型 基于密码学系统的代数特性开发协议的形式化模型 将安全协议系统当作一个代数系统模型，表示出协议的参与者的各种状态，然后分析某种状态的可达性。 Michael Merritt已经证明了代数模型可

18、以用来分析安全协议。 美国海军研究实验室（Navy Research Lab.）开发的协议分析器是这种方法中最成功的一个应用，可以用来在各种协议中寻找新的和已知的缺陷。 安全协议分析的问题形式化分析方法在安全协议的应用是研究的热点。目前应用并不广泛的主要原因,是需要事先建立安全协议的安全性形式化模型。该过程比较复杂困难。目前并没有一种方法能够给出安全协议安全性的充分而且必要的理论证明。由于安全协议本身的复杂性，上述每一类方法都有不同的侧重点，或多或少地存在不足之处。使用上述方法分析安全协议的时候，应当仔细分析协议的特点、应用环境和需求，综合使用这些分析方法，以得到一个比较合理的结果。 由Bur

19、rows, Abadi & Needham提出，从而解决了SPA（Security Protocol Analysis)问题上迈出一大步。 它是关于主体信仰以及用于从已有信仰推出新的信仰的推理规则的逻辑。这种逻辑通过对认证协议的运行进行形式化分析，来研究认证双方通过相互发送和接收消息能否从最初的信仰逐渐发展到协议运行最终要达到的目的认证双方的最终信仰，其目的是在一个抽象层次上分析分布网络系统中认证协议的安全问题。 如在协议执行结束时未能建立起关于诸如共享通信密钥、对方身份等信任时，则表明这一协议有安全缺陷。 BAN逻辑包含believing、seeing、controlling和say

20、ing message语句，并以一种自然结构进行语义描述。 Burrows, Abadi & Needham定义一种基于信任的逻辑精确地表示这些信任找准、抓住导致信任的原因 BAN通过形式化的方法回答以下问题协议在工作吗？协议能否使用？协议达到了预定的目标吗？协议比别的协议需要更多的安全假设吗？协议做了不必要的事吗？ BAN逻辑形式化分析方法重点放在对协议涉及的通信各方的信任以及由这些信任的进一步推演所得到的通信结果上 不考虑由程序执行时所引入的错误如死锁，甚至密码系统的不正确使用问题 考虑到入侵的可能性，并不试图去处理不信任的参与方的认证，也不检测加密方案及未经授权的密码体系。 BA

21、N逻辑形式推理过程1. 给出协议的消息序列描述；2. 对协议进行理想化转换；【】3. 分析理想化的协议模型；4. 判断结论。 BAN逻辑的符号、语法、语义、规则(1)BAN形式体系建立在多种类的模型逻辑上在BAN逻辑中区分几种对象 主体(principals) 加密密钥(encryption keys) 公式(formulas)，也称为语句(statements)。 BAN逻辑的符号、语法、语义、规则(2)公式或语句的连接符(conjunction)用逗号表示【例如】(X,Y)表示X和Y的结合具有结合性和交换性BAN逻辑认为消息(message)和语句(statements)是一样的。VR03

22、04-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabQPYXVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabXP XPXPXP )X(#VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabQPKPKQPXVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabKXYX)X(HVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab

23、 1.1P.XQPXP,QPPKK 1.2P.XQPXP,QP1KK 1.3P.XQPXP,QPPYY 要保证这个规则是合理的，我们则必须保证P自己没有说过X；这就要将公式XK表示成XK from Q，并且要求Q不能是P 消息含义规则消息含义规则关心消息的解释。其中三分之二关心加密消息的解释。它们关心解释如何得到消息源的信任 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 1.4P.XQPY ,XQPVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 1.5P.XPXP,QPPKK 1.6P.XPXP,QP1K

24、K 1.7P.XPXP,PPKK 1.8P.XPY,XP 1.9P.XPXPYVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 2.1P.XQPXQP,X#P 2.2P.Y,X#PX#PVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 3.1P.XPXQP,XQP 3.2P.Y,XPYP,XP 3.3P.XPY,XP 3.4P.XQPY ,XQPVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 4.1P.XQPXP),X(HQPQ拥有消息XVR0304-DOC0-学习讨

25、论：形式化分析方法 北京航空航天大学计算机学院 VR LabVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabbsKabK,A:BA VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabbsKabK,A:BA bsabKKBA:BABAabKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Labn1KnK1X,.,XVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院

26、VR LabTAAATKTBBBTKBATAABKBTBABKAAN#ABN#BBATABK 协议的初始必须是不变的，以保证每个协议的成功。 典型的，初始假设都是陈述两个主体之间共享什么样的密钥，哪个主体产生新鲜的随机值，哪个主体在某些特定的方式下是可信任的。 在大多数的情况下，初始假设是标准和明显的。一旦所有的初始假设被写出，验证协议就等同于对作为结论的公式做出证明。 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBAAABKBABABKBABAABKBAABABK 认证协议经常是建立某些用共享会话密钥的基础，所以，我们可得到认证协议的目标这样的结

27、论描述。 因此，如果认为A和B之间有密钥K，认证则是完成了A相信K是A与B之间的通信密钥，B相信K是A与B之间的通信密钥。 一些协议可能要求的比这更多 VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabVR0304-DOC0-学习讨论：形式化分析方法VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBASA,:asbsKKabsabsAKLTBKLTAS, ,:abbsKaKabsTAAKLTBA, ,:abKaTAB1:SABMessage 1Message 2Message 3Message 4The Kerb

28、eros ProtocolVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabasbsababKKKsKsBATBATAS, ,:fromABATBATBAababbsabKKaKKs, ,:fromBBATABababKKa,:VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabSAAasKSBBbsKSASasKSBSbsKBASabKBASBKBASAK)(#sTB)(#sTA)(#aTBVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBAAabKBABabKBABAab

29、KBAABabKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabThe main steps of the proof are as follows: A receives Message 2. The annotation rules yield thatasbsababKKKsKsBATBATA,),( ,holds afterward. Since we have the hypothesisSAAasKthe message-meaning rule for shared keys applies and yields the followin

30、g:),),( ,(bsababKKsKsBATBATSAOne of our rules to break conjunctions (omitted here) then produces)( ,(BATSAabKsVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabMoreover, we have the following hypothesis(假设):)(#sTAThe nonce-verification rule applies and yields:),(BATSAabKsAgain, we break a conjunction, to

31、 obtain the following:BASAabKThen, we instantiate K to Kab in the hypothesis:BASAKderiving the more concrete:BASAabKFinally, the jurisdiction rule p3.1 applies, and yields the following:BAAabKThis concludes the analysis of Message 2.VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBABabKBAABabKVR0304-DO

32、C0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBAAabKBABabKBABAabKBAABabKBABAabKVR0304-DOC0-学习讨论：形式化分析方法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)KabVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab1. ATKABAMNBAM,2. BTATKBKABAMNBAMNBAM,3. BTATKABBKABAKNKNM,4. AT

33、KABAKNM,VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab1. ATKABAMNBAM,ATKCANNB,2. BTATKBKABAMNBAMNBAM,),(BTATKCBKCANNNNT 3. BTATKABBKABAKNKNM,),(BTABATABKCKBKCKANABANNBBANB4. ATKABAKNM,ATABKCKANBBANA,VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabTAAATKTBBBTKTATATKBATAABKTBTBTKBATABKBATBABKXBTAXATBANA#B

34、NB#CNA#VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBABAABKBAABABKBAAABKBABABKCNBACNABVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBANTBTBBBANBABBTBTABKBKKKB,)(#)(#,BABNBBANBABBTABKBKKBBATBBABBATBABABABKKK)(#,BABBATBBATBABABABKKK,P3.1P1.1P2.1VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBAAABKCNBACNA

35、B因为缺少| #()cBNVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabCNABBAAABKCNBABABABKVR0304-DOC0-学习讨论：形式化分析方法VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab4. ABKBN 1. ANBA,2. ATBTKKABABAKAKBN, ,3. BTKABKA,5. ABKB1NVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabM2.

36、ATBTABABABATBTKKKKKAKKABABABABABANAKAKBN),(#,M3. BTABBTKKKABBABKA,M4. BfromBANANABABABKKBKB,M5. fromABANBNABABABKKBKB,1 将消息写成“收到”形式VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabTAAATKTBBBTKTATATKBATAABKTBTBTKBATABKBATBABK)(BATAABK#)(BATABK#ANA #BN#B )(BABABK#)(BATBABK#VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大

37、学计算机学院 VR LabBAAABKBABABKBABAABKBAABABK)(#BAAABK)(#BABABKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 1 .),(#),( ,(),(#),( ,(,CBABABANTABABABANATAABTABABABATBTABABABATKKKKAKKKKKAKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab2 .)(),(#),( ,(),(#CBATABABABANTANAABBTABABABKKKKKAAVR0304-DOC0-学习讨论：形式化分析方

38、法 北京航空航天大学计算机学院 VR Lab4 .).(#3 .,)(#),(CBAACBAABATABATAABABABABKKKKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab5 .)()(),(CBATBTfromBABTBBABBTABBTKKKKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab6 .)()(),(#CBATBBATBBABABABABKKK)(BABABK#VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab7 .)(#),(),(CBABBAT

39、BBATBBATBABABABABKKKK)(BABABK)(BAAABKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab8 .)( ,()( ,(),(CBANBABfromBANABAAABABABABKBKKBKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab9 .)()( ,(),(#CBABABANBABAAABABABKKBK10.).(CBAABABKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab3 .CBAAABK7 .CBABABK9 .CBABAA

40、BK10.CBAABABK4 .).(#CBAAABK)(#BABABKVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab)(#BNB VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabBAAABKBATBABKBAABKATABKKABA,N)(BABABK#VR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR Lab 协议的理想化过于依赖分析时的直觉，协议的理想化使得在原始协议与理想化协议之间

41、存在一个潜在的语义鸿沟。 Ban逻辑分析的正确性严重依赖于前几步，但前三步在有效达成目标上存在问题。即使对协议行为做出了准确的解释，也不能保证能够正确理解协议设计者的真正意图，因而虽然对主体行为的理解不存在任何歧义，但仍可能存在对同一协议有两种理想化的结果。 BAN不够完备，即BAN逻辑不能查出协议的所有问题，只能证伪。 BAN逻辑系统没有为协议理想化过程提供标准的转换格式，这就使得对同一个协议由于分析者的不同理解而得到不同的理想化版本。 不合理的假设认为参与协议运行的主体都是诚实的。实际上许多合理协议并不满足主体诚实性假设，且诚实概念也缺乏良好规范的定义初始状态假设难以确定，而假设对分析结论

42、的正确得出至关重要。没有形式化规则来确定假设，从而无法确认和自动验证假设的正确性和有效性。 BAN逻辑为认证协议的设计提供了可参考的准则。认证主体用会话密钥加密另一个认证主体所知的明文信息，来表示已获得了会话密钥。协议中会话密钥的使用必须以新鲜性为保证，以防密钥重放。认证协议中，在传送包含关键的敏感信息的消息中，尽可能以显式表现出参与协议的各个主体，使接收的主体能清晰地意识到其它主体的存在。在协议中可信服务器的信仰很重要，因此区分服务器作用的强弱是十分必要的。 1994年Syverson和Orschot提出了SVO逻辑，它的出现标志着BAN及BAN类逻辑的成熟。1996年，他们又在SVO逻辑的

43、公理，以及语义上有进行了更准确的定义。SVO逻辑吸收了BAN类逻辑系统的优点，同时又具有十分简洁的推理规则和公理。它为逻辑系统建立了用于推证合理性的理论模型。在形式化语义方面，它具有极好的扩展能力。 定义T为初始术语集合，包括互不相交的常量符号集合：主体、共享密钥、公钥、私钥以及序列号等。基于此，n维函数表示有n个变量的函数，如加、解密函数等。SVO逻辑将语言划分为集合T上的消息语言MT和公式语言FT。消息语言MT 是满足下列性质的最小语言集合：1.如果XT，则X是消息。2.如果X1，Xn是消息，F是任意一个n维函数，则F(X1，Xn)是消息。3.如果是公式，则是消息。 公式语言FT是满足下列

44、性质的最小公式集合：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，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,

45、 K, Y) 是公式，其中X，Y是消息，K是密钥。（SV(X, K, Y)指签名验证，即X为签名后得到消息，K为签名验证密钥，Y为被签名的消息。） 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 P Received by P Freshly generated by P Constru

46、ctible by P from the above 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 P. Only P

47、 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. XK: X signed with key K. Notationally distinguish: Encrypted messages fr

48、om 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 keys. X *p: X according to P. Used for messages that P doesnt know/recognize Example: XK w

49、here P does not know K P will recognize XK *p as the same thing if received again.SVO逻辑遵从两条基本推理规则：Modus Ponens (MP)：( )Necessitation (Nec)： P believes SVO逻辑共有20条公理：对于任一主体P和公式，有：Ax1：P believes P believes ( ) P believes Ax2：P believes P believes (P believes )公理Ax1表示主体相信由其已有的信任关系逻辑推导出的所有信仰结果。公理Ax2表示主体表

50、明其信任的是什么。密钥用于推断消息发送者的身份。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的数字签名验证密钥。此公理表明如果主体R收到一个签名消息，并且R知道签名的验证公钥是K，它就可以确认消息发方的身份。会话密钥是由密钥协商密钥是良好的得到的。Ax5：(PK(P，Kp)PK(Q，Kq) shared(P，Kp,q，Q)Ax6： F0(K,K) / F0

51、(K,K)公理Ax5中KpqF0(Kp，Kq1 )F0(Kp-1,Kq)，F0指密钥协商函数，如Diffie-Hellman密钥交换。F0(K, 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保存的秘密密钥。该公理表示两个公式逻辑上是相等的。也就是说，逻辑注意到密钥协商的对称性。主体对接收到的一个级联的加密消息并用有效的密钥解密。Ax 7：P received (X1，X

52、n) 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) 主体只要接收到一个消息就看到了这个消息，并且看到了这个消息的每一部分。主体还可以看到从已看到的消息计算得到的消息。Ax10：P received X P sees XAx11：P sees (X1，Xn) P sees XiAx12：

53、P sees X1 P sees Xn P sees (F (X1，Xn) 如果一个主体理解一个消息，并看到此消息的一个函数，那么它理解它所看到的。Ax13：P believes (P sees F(X) P believes (P sees X)F可视为加解密函数，K为参数。一个主体说过一个级联消息，那么它一定说过且看到消息的每一部分。Ax14：P said (X1，Xn) P said Xi P sees XiAx15：P says (X1，Xn) P said (X1，Xn) P says XiAx16：P controls P says 如果消息的一部分是新鲜，那么整个消息也是新鲜的。

54、有关新鲜消息的任何一对一函数（如加密解密函数）也是新鲜的。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 say

55、s X( Symmetric goodness of shared keys)如果K是P、Q之间的良好密钥当且仅当K是Q、P之间的良好密钥。Ax20：shared(P，K，Q)shared(Q，K，P) P has K P sees KVR0304-DOC0-学习讨论：形式化分析方法 北京航空航天大学计算机学院 VR LabSVO逻辑的协议句法分析技术与BAN逻辑的分析技术同属于推理结构的分析方法。但SVO逻辑不需要BAN逻辑的协议理想化过程，而重点具体化了协议前提的确定过程。SVO逻辑对协议的形式化分析分为以下三步： 给出协议所基于的前提。 形式化说明协议将达成的安全目标。1. 运用公理和推

56、理规则及其前提，从协议的前提进行推证直至验证协议是否满足其最终运行目标。 第一类前提是初始假设，即在协议的初始状态时就为真的假设。例如每个主体对其产生的随机数的新鲜性的信任；主体对其与服务器共享的长期密钥的良好性的信任；主体关于服务器对它发送的密钥的质量和新鲜性具有权威的信任等。 如：消息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) 第二类前提反映主体对在协议运行期间发送的消息的接收，可以直接从协议描述得到。在证明过

57、程中经常不使用这类前提，但它们有助于形成后边的前提。 如：上例为 A received Ts, B, Ka,bKa,s 第三类前提反映每个主体对其收到消息的理解。主体不可能完全理解其所收到的消息的每一部分。如由于分发（distributed）密钥具有随机性，故收到它的主体（而不是产生它的主体）必然不能理解它（unrecognizable）。通过考虑主体对其在第二类前提中的接收到子消息的理解，很容易得到这一类前提。如：上例为 A believes A received Ts, B, *s Ka,s 第四类前提反映接收主体对收到消息加入的解释。这是BAN逻辑中理想化步骤的主要替代部分（primar

58、y replacement）。这类前提还与具体协议的特征有关。如: 上例为 A believes （A received Ts, B, *s Ka,s A received Ts, B, share(A, Ka,b ,B),fresh(Ka,b) Ka,s） 不可否认协议的实现包括证据的生成、证据的交换、证据的验证以及纠纷的解决，方法一般有两种：一是双方进行同时（或接近同时）的秘密交换;另一种借鉴可信第三方（TTP）。经常采用TTP方式。 两个基本证据：NRO（Non-repudiation of Origin)发方不可否认。用于证明发方的确发送了消息，由发方提供。NRR（Non-repudi

59、ation of Receipt)收方不可否认。用于证明收方的确收到了消息，由收方提供。 如有TTP介入，则还需要下面两个证据：NRS（Non-repudiation of Submission)提交不可否认。用于证明已提交给了TTP，由提交方提供。NRD（Non-repudiation of Delivery)传递不可否认。证明TTP已交给了意定的接收者，由TTP提供。Zhou和Gollmann在文献5提出了一个不可否认协议（ZG协议），具体描述为：M1 AB： fNRO,B,L,C,NROM2 BA: fNRR,A,L,C,NRRM3 ATTP: fNRS,B,L,K,NRS_KM4 BT

60、TP: fNRD,A,B,L,K,NRD_KM5 ATTP: fNRD,A,B,L,K,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)消息M的传输分两步