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

2020/6/291第十五章安全协议的形式化分析技术2020/6/292逻辑推理及形式化语言•逻辑推理•形式化语言•形式化分析方法•形式化分析方法应用2020/6/293逻辑推理•逻辑推理由前提推出结论。前提和结论都是命题。命题的真或假由命题的内容是否符合客观实际确定。•演绎逻辑当前提的“真”蕴涵结论的“真”，称前提和结论之间有可推导性关系。即前提和结论之间的推理是正确的。研究怎样的前提和结论之间具有可推导性关系。•归纳逻辑只要求得到的结论本身是协调的，与前提是协调的。前提的“真”并不蕴涵结论的“真”。2020/6/294逻辑推理•逻辑推理的正确性–命题的内容：“真”/“假”，内容决定命题的“真”/“假”。–命题的形式：即逻辑形式。由内容抽象出来。–逻辑形式决定前提和结论的之间的可推导性关系。–不关心前提和结论的真假，而关注前提的真是否蕴涵结论的真。2020/6/295形式化语言•形式语言–使用自然语言陈述并分析命题常常引出歧义。–需要构造一种符号语言——形式语言，描述由命题内容抽象出来的命题逻辑形式。•形式语言使用符号来构造公式•由公式来精确地表示命题的逻辑形式•语义和语法–语义涉及符号和符号表达式的涵义(给符号某种解释)–语法涉及符号表达式的形式结构，但不考虑任何对形式语言的解释。–形式语言的语义和语法既有联系，又有区分。2020/6/296形式化分析方法•集合论•数理逻辑•图论：有限状态图•网论：Petri网模型•代数系统：代数系统形式化模型2020/6/297安全协议•􀂄安全协议的基本概念–安全协议特指使用密码学技术的密码协议–所谓协议，就是两个或者两个以上的参与者为完成某项特定的任务而采取的一系列步骤。•协议的定义包含三层含义：1.协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之前，后面的步骤不可能执行；在参与者之间呈现为消息处理和消息交换交替进行的一系列步骤。2.协议至少需要两个参与者；一个人可以执行一系列的步骤来完成一项任务，但它不构成协议。3.通过协议必须能够完成某项任务。安全协议使用密码学技术，协议参与者可能是可以信任的人，也可能是攻击者和完全不信任的人。密码协议包含某种密码算法。2020/6/298安全协议•网络通信中常用的密码协议按照其完成的功能分成以下四类：–密钥交换协议•在参与协议的两个或者多个实体之间建立共享的秘密通道，常用于建立在一次通信中所使用的会话密钥。协议可以采用对称密码体制，也可以采用非对称密码体制，例如Diffie-Hellman密钥交换协议。–认证协议•认证协议中包括实体认证（身份认证）协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。–认证和密钥交换协议•协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。常见的有Needham-Schroeder协议、分布认证安全服务（DASS）协议、ITU-TX.509认证协议等等。–电子商务协议•电子商务协议中，主体利益目标往往是不一致的，电子商务协议关注的就是公平性，即协议应保证交易双方都不能通过损害对方利益而得到它不应得的利益。常见的电子商务协议有SET协议等。2020/6/299DH算法描述1.Alice与Ｂob确定两个大素数n和g，这两个整数不保密，Alice与Ｂob可以使用不安全信道确定这两个数．2.Alice选择另一个大随机数x，并计算A如下：A=gxmodn3.Alice将Ａ发给Ｂob4.Ｂob选择另一个大随机数y，并计算B如下：B=gymodn5.Ｂob将Ｂ发给Alice6.计算秘密密钥K1如下：K1=Bxmodn7.计算秘密密钥K2如下：K2=Aymodn2020/6/2910SSL/TLS协议栈•介于应用层和传输层之间•为上层提供安全性IPSSLChangeCipherSpecProtocolSSLAlertProtocolApplicationProtocolTCPSSLRecordProtocolSSLHandshakeProtocolHTTPLDAPIMAP2020/6/2911SSL/TLS概况•协议分为两层–上层：TLS握手协议、TLS密码变化协议、TLS警告协议–底层：TLS记录协议–上层协议是用于管理SSL密钥信息的交换，下层提供基本的安全服务•TLS握手协议–客户和服务器之间相互认证–协商加密算法和密钥–它提供连接安全性，有三个特点•身份认证，至少对一方实现认证，也可以是双向认证•协商得到的共享密钥是安全的，中间人不能够知道•协商过程是可靠的•TLS记录协议–建立在可靠的传输协议(如TCP)之上–它提供连接安全性，有两个特点•保密性，使用了对称加密算法•完整性，使用HMAC算法–用来封装高层的协议2020/6/2912SET协议目标•信息在Internet上的安全传输，保证网上传输的数据不被黑客窃听•订单信息和个人账号信息的隔离，在将包括消费者账号信息的订单送到商家时，商家只能看到订货信息，而看不到消费者的账户信息•消费者和商家的相互认证，以确定通信双方的身份，一般由第三方机构负责为在线通信双方提供信用担保•要求软件遵循相同的协议和消息格式，使不同厂家开发的软件具有兼容和互操作功能，并且可以运行在不同的硬件和操作系统平台上2020/6/2913DesktopcomputerCardHolderHowSETwithCreditCardWorksServerMerchantServerAcquiringBankCardIssuerBank876543219CACertificateAuthority00-cardholderregistration132-purchaserequest-merchantpassessigned,encryptedauthorizationtotheacquirerforcheck-cardvalidationwithissuer4-issuerauthorizesandsignstransaction5-acquirerauthorizesmerchantandsignsthetransaction6-cardholderreceivesthegoodsandareceipt7-merchantdepositthetransactiontohisaccount8-merchantgetspaid9-cardholderreceivesbillfromcardissuer2020/6/2914安全协议系统模型•如果将安全协议所处环境视为一个系统，那么这个系统中，一般而言包括一些发送和接收消息的诚实的主体和一个攻击者，以及用于管理消息发送和接收的规则。诚实主体诚实主体诚实主体诚实主体环境/攻击者通信通信通信通信2020/6/2915安全协议的性质评估一个安全协议是否安全就是检查其所欲达到的安全性质是否遭到攻击者的破坏。•认证性–声称者使用仅为其与验证者知道的密钥封装的一个消息–声称者使用私钥对消息签名，验证者使用公钥来验证–声称者通过可信第三方来证明自己。•秘密性–保护协议消息不被泄露给非授权拥有此消息的人，即使是攻击者观测到了消息的格式，它也无法从中得到消息的内容或提炼出有用的信息。–保证协议消息秘密性的最直接的方法是对消息进行加密。–安全协议中，一般不考虑具体的密码算法的执行细节，但在实际应用中这往往有可能造成协议秘密性的缺陷。2020/6/2916安全协议的性质•完整性–保护协议消息不被非法篡改、删除和替代。–常用的方法有封装和签名–SSL和IKE等协议中就涉及到保护协议消息完整性的具体实现细节•不可否认性–目的是通过通信主体提供参与协议交换的证据来保证其合法利益不受侵害，即协议主体必须对自己的合法行为负责，而不能也无法事后否认。–协议必须具有两个特点：证据的正确性、交易的公平性。在不可否认性之中还可引申出其他一些相关性质，如适时中止性、公平性、可追究性等。2020/6/2917安全协议的缺陷•安全协议的安全性–安全协议是许多分布式系统安全的基础，确保这些协议的安全运行是极为重要的。–安全协议有若干几个消息传递，消息之间存在着复杂的相互作用和制约；–协议中使用多种不同的密码体制，–目前的许多安全协议存在安全缺陷。原因有两个：•协议设计者误解或者采用了不恰当的技术；•协议设计者对环境要求的安全需求研究不足。–对协议的安全性进行分析和研究是一个重要的课题。2020/6/2918安全协议的缺陷•S.Gritzalis和D.Spinellis根据安全缺陷产生的原因和相应的攻击方法对安全缺陷进行了分类：–基本协议缺陷：•协议设计中没有或很少考虑防范攻击者。–口令/密钥猜测缺陷：•弱口令导致攻击者能够进行口令猜测攻击；或者弱密钥使攻击者能够破解该密钥。–陈旧（stale）消息缺陷：•协议设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等等。2020/6/2919安全协议的缺陷–并行会话缺陷•协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的重要消息。–内部协议缺陷•协议可达性存在问题，协议的参与者中至少有一方不能够完成所有必须的动作而导致缺陷。–密码系统缺陷•协议中使用的密码算法的安全强度导致协议不能完全满足所要求的机密性、认证等需求而产生的缺陷。2020/6/2920安全协议的逻辑形式化分析•安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存在安全缺陷。•从安全协议的分析和设计角度来看，应当对协议的安全性作出认真的分析和验证。•安全协议的分析方法–攻击检验方法；–形式化的分析方法。2020/6/2921安全协议的逻辑形式化分析•攻击检验方法–搜集使用目前的对协议的有效攻击方法，逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力。–在分析的过程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析。–这种分析方法对已知的攻击非常有效的。–不能发现协议中未知的安全隐患。2020/6/2922安全协议的逻辑形式化分析•形式化的分析方法–采用各种形式化的语言或者模型，为安全协议建立模型，并按照给定的假设和规则，分析、验证方法证明协议的安全性。–近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。–形式化的分析方法是目前研究的热点，但是就其实用性来说，还有待进一步突破。–安全协议的形式化分析有助于：•界定安全协议的边界，即协议系统与其运行环境的界面•更准确地描述安全协议的行为。•更准确地定义安全协议的特性。•证明安全协议满足其说明，以及证明安全协议在什么条件下不能满足其说明。2020/6/2923协议形式化分析技术(1)1）通用的形式化描述语言•使用通用的、不是为分析安全协议专门设计的形式化描述语言和协议校验工具建立安全协议的模型并进行校验。主要思想是将安全协议看作一般的协议，并试图证明协议的正确性。•采用的工具和模型与验证一般协议的类似，例如使用有限状态图、Petri网模型、LOTOS语言等等。•方法的主要缺点是仅证明协议的正确性而不是安全性。2020/6/2924协议形式化分析技术(2)2）专家系统•设计专用的专家系统来制定安全协议的校验方案并进行协议检验，从而对协议的安全性作出结论。•主要思想是针对所设计的协议而开发专用的专家系统，通过专家系统发现协议是否能够达到不合理的状态（比如密钥的泄露等等）。•这种技术能够识别缺陷但是不能证明协议的安全性，也不能发现未知的缺陷。2020/6/2925协议形式化分析技术(3)3）安全需求模型•基于知识和信任逻辑，针对具体协议建立相应的形式化安全需求模型•依据给定的逻辑初设和公理规则对该模型进行形式化分析推理•通过推理获取的结果来推断协议能否完成预期的目标、证明协议结论的正确性。•形式系统的组成（初始符号、形式规则、公理、变形规则）2020/6/2926协议形式化分析技术(4)•这种方法是目前为止使用最广泛的一种