基于公开密钥认证协议安全性的分析与研究本科毕业论文(编辑修改稿)

基于公开密钥认证协议安全性的分析与研究本科毕业论文(编辑修改稿)内容摘要：

安全。 因为实际应用中，存在着许多未知的攻击方法，这种对公开密钥认证协议的非形式化分析方法只能发现协议中是否存在着已知的缺陷，而不能全面客观地来分析公开密钥认证协议，可能导致不安全的协议经分析是安全 的这样错误的结论。 八十年代以后，随着对公开密钥认证协议安全性分析的进一步探索研究，公开密钥认证协议的形式化分析成为研究热点。 安全协议的形式化分析是采用一种正规的、标准的方法对协议进行分析，以检查协议是否满足其安全目标。 这种方法的出发点是希望将公开密钥认证协议形式化，然后借助于人工推导，甚至计算机的辅助分析，来判别公开密钥认证协议是否安全可靠。 形式化分析方法和攻击检验方式相比，它能全面、深刻地检测到公开密钥认证协议中细微的漏洞。 形式化分析方法不仅能发现现有的攻击方法对协议构成的威胁，而且还可能通过对公开密钥 认证协议的安全性分析，发现协议中细微的漏洞，从而发现对公开密钥认证协议新的攻击方法。 模型检测技术（ Model Checking Technology）是属于一般目的的公开密钥认证协议的形式化分析方法，它是验证有限状态系统的自动化分析工具，常用于硬件电路设计和通信协议。 目前模型检测技术也是一种十分有效的协议形式化分析工具。 模型检测技术最早是用于分析和模拟硬件工作过程的形式化方法，随着形式化方法的日益进步和应用领域的推广，现已应用于软件分析和通信协议模拟等多个领域，但用于安全协议的分析还是近几年新的应用。 关 于模型检测的研究越来越受到人们的关注，因为它对协议的自动验证和协议的工程化设计具有指导意义。 在 1996 年，英国学者 Gavin Lowe 首先使用 CSP 和模型检测技术对公开密钥认证协议进行分析 [13]，在这篇文章中， Gavin Lowe 首次采用 CSP 模型和 CSP 模型检测工具 FDR(故障偏差精炼检测器， Failures Divergences Refinement Checker)来分析 NeedhanSchroeder 公钥协议，并成功地找到一个 BAN 类逻辑等分析方法以前未发现的攻击。 模型检测技术应用 于网络安全协议分析的成功，使学者们相继投入到这个领域。 自 97 年起，计算机科学家及密码学家开始陆续应用模型检测这种新的形式方法来分析网络安全协议的安全性，对多个网络安全协议进行了分析，成功地发现了许多攻击。 在文献 [17]中 Steve Schneider 用 CSP 研究了公开密钥认证协议的安全性质，在文献 [18]中 和 基于对 CSP 和 FDR研究，认为它们是公开密钥认证协议完美的检测工具。 在文献 [19]中 等提出了一种通用的模型检测器，构造了他们的 模型及代数理论，并证明该模型的有效性。 文中并对 NeedhanSchroeder 公钥协议进行了分析，也成功地发现了文献 [20]所找到的攻击。 在文献 [21]中 等设计了一种通用的状态计数工具 Murф，并用它来分析公开密钥认证协议可能达到的状态，进一步得出公开密钥认证协议是否安全的结论。 文中分析了 NeedhamSchroeder 协议、 Kerberos 协议和 TMN 协议，并找到了这些协议所有 15 已知的攻击。 在文献 [22]中 Zhe Dang 等用 ASTRAL 这种实时系统形式化描述语言 构造了模型检测器，文中并对 NeedhamSchroeder 公钥协议和 TMN 协议进行了分析，也成功地发现了 Gavin Lowe 所找到的所有攻击。 英国学者 Gavin Lowe 在模型检测上做出了非凡的创造性成果，相应的结论可参见 [20][13]。 其中文献 [22]是一篇关于模型检测大全性的文章，文中试图为模型检测技术提供一个完整地解决方案。 目前对于协议分析来讲，模型检测已经证明是一条非常成功的途径，这种方法发现了协议的许多以前未发现的新的攻击，极大地促进了网络安全协议分析与设计的研究工作。 但模型检测仍然存 在着许多需要进一步研究的问题，最主要的问题在于：模型检测适用于有限状态系统地分析工具，如何将公开密钥认证协议说明成有限状态系统，而又没有增加或减少公开密钥认证协议的安全性。 这是一个需要继续深入研究和探索的核心问题。 论文安排与研究成果 本论文是在结合国家自然科学基金项目“公开密钥认证协议的模型检测分析”的基础上，围绕着公开密钥认证协议的模型检测技术进行了深入的研究，本论文的工作成果如下： 论文安排 第二章： 指出模型检测技术分析公开密钥认证协议的现状； 研究模型检测技术分析公开密钥认证协议 的基本理论； 介绍两方公开密钥认证协议运行模式分析法并对其进行研究。 第三章： 介绍模型检测工具 SMV。 第四章 介绍公开密钥认证协议； 运用运行模式分析法分析公开密钥认证协议安全性； 尝试使用 SMV 检测两方公开密钥认证协议的模型检测。 主要研究成果 以下是我们取得的一些成果： (1) 系统的介绍了公开密钥认证协议的一些基本概念和公开密钥认证协议安全性分析的重要意义、研究进展和现状。 16 (2)研究了模型检测技术和公开密钥认证协议运行模式分析法。 (3)给出了运用模型检测工具 SMV 分析公开密钥认证 协议的方法。 (4)运用运行模式分析法分析了公开密钥认证协议，并尝试使用 SMV 研究了公开密钥认证协议的安全性检测。 17 2 模型检测技术及运行模式分析法研究 本章首先介绍了模型检测技术和模型检测技术在公开密钥认证协议分析领域取得的研究成果；随后引出了以此技术为理论依据的公开密钥认证协议运行模式分析法，并对其运行模式作了进一步的研究。 引言 模型检测技术原是用于分析和模拟硬件工作过程的形式化方法，随着形式化方法的推广和应用，模型检测技术现已用于软件分析和通信协议模拟等多个领域，但用于公开密钥认证协议 的分析还是近几年比较新的应用。 在 1996 年，英国学者 Gavin Lowe 首先使用 CSP 和模型检测技术对公开密钥认证协议进行分析 [20]。 并首次采用 CSP 模型和 CSP 模型检测工具 FDR(故障偏差精炼检测器， Failures Divergences Refinement Checker)，来分析 NeedhamSchroeder 公钥协议。 在这个模型中，协议参与者被说明成 CSP 中的进程 (process)，消息说明成事件（ event），进而将协议说明成一个通信顺序进程的集合，这些进程并行运行而且和他们的环境交互作 用，其对公开密钥认证协议的验证是从协议说明中抽取一个模型（通常是一个有限状态转换系统），然后用 FDR 检测，从而证明协议的安全性。 此方法成功地找到 NeedhamSchroeder 协议的一个以前从未发现的攻击。 模型检测的成功，使研究者们相继投入到这个领域。 实践证明对于公开密钥认证协议安全性分析来讲，模型检测是一条非常成功的途径。 模型检测技术分析公开密钥认证协议的基本理论 模型检测技术分析公开密钥认证协议的理论研究 模型检测技术可以抽象地描述为：给定一个模型 M 和逻辑描述的性质 P，检查 模型 M中性质 P是否成立。 模型检测技术对协议进行验证与分析，是通过检查在恶意攻击者存在的情况下，协议运行的所有可能的路径，来判断协议是否实现了其安全保证；如果没有，将给出攻击者的攻击路径。 模型检测用于有限状态系统的分析，要用模型检测技术分析公开密钥认证协议，就要研究如何为公开密钥认证协议构造有限状态系统。 目前，模型检测技术分析公开密钥认证协议的基本方法主要采用英国学者 Gavin Lowe 研究成果，即：生成一个协议运行的小系统模型（通常是一个有限状态转换系统），以及一个可与协议互操作的攻击者模型，并用状态探测 工具检测系统是否进入一个不安全状态，即是否存在对协 18 议的攻击。 并且基于代数理论证明：如果小系统是安全的，那么协议是安全的。 这种方法提出了将大系统中协议安全的性质研究约化为小系统中协议安全性质的研究，这是目前这一领域的最新理论研究成果。 使用该方法发现了公开密钥认证协议许多以前未发现的新的攻击，极大地促进了公开密钥认证协议分析与设计的研究工作。 （ 1）模型检测对被分析协议的基本假设： 任何一个系统都有其赖以存在的假设条件，用以避免结论的不当使用以及对一些限制的理解，同样，用模型检测技术分析公开密钥认证协议 ，对协议是有一定要求的，因为只有能用有限状态描述且满足一定条件的协议才能模型检测，并不是所有的公开密钥认证协议都能用模型检测技术来分析。 在文献 [26]中给出了能被模型检测技术所分析的公开密钥认证协议的基本假设，具体描述如下： 1)加密部分从文字形式上是可以区分的 公开密钥认证协议中所用到的加密项从文字上就可以区分。 这意味着一个主体接收到一个加密项就知道这个加密项属于哪个消息，是消息的哪一部分。 这个假设可以防止入侵者重置协议中的消息，也能防止入侵者用另一条消息对原消息进行替换。 这个条件很容易满足，例如只要在 每个加密项中放入项的编号即可。 2)身份的可确定性 参与协议运行的所有主体的身份是可以通过协议运行中的加密项推导出来的。 这样一个主体当他接收了一个加密项后，他就可以确定这个加密项是否为他而发。 更进一步，如果这个加密项起源于一个诚实的主体，接收者可以判断出谁是加密项的产生者，谁是这个加密项的接收者。 假设 1 和假设 2 容易满足，只要在每个加密项中明显包含每个主体的身份即可：更进一步说，如果消息是来自诚实主体，那么接收方就能确定谁是消息的发送方和谁是消息的接收方。 这两个假设条件可避免许多攻击，并且也使公开密钥认证 协议的分析更容易。 3)协议运行时不用协议运行期间建立的任何临时秘密 如果一个特别的数据项不是那种要保持为秘密的数据项，那么一个监视通信的第三者就能够从有该数据项参与的运行中获知此数据项的值（或者这个值是公共信息，第三者早已知道它）；更进一步，如果一个特别的密钥不是那种要保持为秘密的密钥，那么一个监视通信的第三者就能够通过持有该密钥的逆参与的运行中获知此密钥的数值（或者明显得到，或者通过加密某些数据项）。 （ 2）模型检测对基于模型的假设： 1)完善加密假设 协议采用的密码系统是完美的，不考虑密码系统被攻破的 情况等。 2)入侵者的知识和能力 ①可窃听及中途拦截系统中传送的任何消息； ②可解密用他自己加密密钥（公钥或单钥）加密的消息； ③在系统中可插入新的消息； 19 ④即使不知道加密部分的内容，也可重放他所看到的任何消息（其中可改变明文部分）； ⑤可运用他知道的所有知识（如临时值等），并可产生新的临时值等。 （ 3）模型检测的结论 运用模型检测技术分析公开密钥认证协议，就要构造小系统模型，关于小系统的定义和安全性质的定义和结论如下： 1)小系统的定义： 所谓小系统是指参与协议运行的各主体都是唯一的（例如，一个初 始者，一个响应者），作用也是唯一的。 这些主体也都是诚实的：他们严格按照协议规定和遵循自己的身份参与协议运行，并不与入侵者运行协议。 2)安全性破坏定义： 定义 1（强安全性破坏）： 一个诚实的主体相信在协议运行中用到的一个值是仅他和另外诚实主体之间的共享秘密，但入侵者知道这个值。 定义 2（一般安全性破坏）： 一个诚实的主体相信在一个完整协议运行中用到的一个值是仅他和另外诚实主体之间的共享秘密，但入侵者知道这个值。 小系统理论旨在解决：在协议及其环境条件下，如果小系统是安全的，那么大系统也是安全的。 文献 [19]中用大量篇幅，创建了一套基于代数方法的理论，并证明了如下结论： 如果在某一特定的小系统中不存在对协议强安全性破坏的攻击，那么对任意系统也不存在强安全性破坏的攻击，当然也就不存在攻击导致一般安全性破坏的攻击，即如果小系统是安全的，那么协议是安全的。 小系统理论理论大大减少了安全协议分析的工作量，并从理论上增强了协议分析结果的可信任度。 这个理论结果极大地促进了模型检测技术在安全协议分析领域的广泛应用，使安全协议形式化分析的主流从逻辑方法转向了模型检测，进而使安全协议的形式化分析更上一层楼。 模型检测技 术的现状及存在的问题 用模型检测技术分析网络安全协议，只要对被分析的协议在小系统上进行强安全性破坏分析，就可以保证协议在任意系统上的安全性。 这一理论大大减少了公开密钥认证协议分析的工作量，并从理论上保证了人们对协议分析结果的信心。 所以对于协议安全性分析来讲，模型检测技术已经证明是一条非常成功的途径。 这种方法发现了协议的许多以前未发现的新的攻击。 但模型检测技术仍然存在着一些问题： （ 1） 现有方法是否作到了理论上所要求的强安全型破坏分析。 （ 2） 如何评价和衡量不同的检测方法和检测工具。 （ 3） 这种分析方法对协议的种类有所限制， 对具有满足以下情况的协议不能进 20 行分析指导： 1)黑匣协议。 2)采用 非标准的加密方式的协议。 3)消息中包含长期秘密项的协议，如主体的私钥等这类协议，目前模型检测无法分析。 我们将用于若干次协议运行的数据项，如主体的公开密钥、秘密密钥等定义为长期项。 而将主体在一次协议运行中引入的短期数据项，如临时值，短期密钥等定义为短期项。 长期项和。