论文总字数：40192字

摘 要

随着互联网业务的高速发展，计算机网络上升为信息交换的主流手段。在其带来便利的同时，也导致人类遭受隐私信息泄露，进而遭受财产损失等。为保障信息安全，人们投入大量人力物力，其中认证协议的安全性是重点研究的内容之一。

形式化分析方法是辅助安全协议设计、弥补协议安全漏洞的有效手段大致分类为模型检测方法、定理证明方法和信仰逻辑方法。AVISPA工具全称是网络安全协议及应用的自动认证工具，融合了模型检测等形式化分析方法，能够自动分析协议安全性。而SPAN工具将AVISPA的功能形象化、本地化，表现为信息序列图表的形式。

本文选用SPAN工具分析了SSL协议和Kerberos协议的安全性。根据AVISPA的系统结构，首先阐述HLPSL描述方法，再成功描述这两种协议。按照SPAN工具提供的协议仿真验证了协议描述的准确性，修改了协议描述直至与协议交换过程一致。最后模拟SSL协议和Kerberos协议在应用中的窃听环境，利用模型检测等形式化工具分析它们的安全性。分析结果表明，SSL协议会遭受证书伪造、篡改的攻击，而Kerberos协议使用的对称密钥体系存在安全性不足的问题。根据分析结果，改进SSL协议，促使用户不完全信任SSL证书，且入侵者无法获取用于加密证书的公钥；改进Kerberos协议，用公钥密码体系取代对称密钥能够保障即使一个密钥被破解而其他密钥依然安全。

关键词：认证协议，安全性，SPAN，SSL协议，Kerberos协议

SECURITY ANALYSIS OF AUTHENTICATION PROTOCOL

ON INFORMATION SYSTEMS

Abstract

With the rapid development of the Internet services, the computer network has been the main approach to interchange of information. The Internet brings convenience to people, while also brings about privacy leakage and further more monetary loss. People devote to themselves to protect information security in which authentication protocol is in major.

Formal analysis can aid security protocol design and fix bugs effectively. Formal analysis includes model checking, theorem proving and belief logic. AVISPA is the abbreviation of Automated Validation of Internet Security-sensitive Protocols and Applications. It includes model checking and some else formal analysis, and also can be automatic. SPAN makes the function of AVISPA vivid and localization which is described as Message Sequence Charts.

Choose SPAN to analyze SSL protocol and Kerberos protocol. According to AVISPA system architecture, explain HLPSL specification method first and then specify the two protocols. Modify the specification by protocol simulation in SPAN till the specification fits protocol exchange. Last, simulate intruder’s environment in application of SSL and Kerberos protocols and use verification tools like model-checker to analyze if the protocol is secure. It turned out that SSL protocol suffers from attack on falsify certification and the public key system isn’t secure on Kerberos protocol. To improve SSL protocol, make users not believe in SSL certification and provide the intruder from fetching public-key for encrypting certification; to improve Kerberos protocol, public-key replacing symmetric-key keeps other keys safe even if the intruder crack one key.

KEY WORDS: Authentication protocol, security, SPAN, SSL protocol, Kerberos protocol

目录

第一章 绪论 1

1.1 引言 1

1.2安全协议 1

1.2.1安全协议的概念与作用 1

1.2.2认证协议的发展历史 2

1.2.3 认证协议的安全隐患回顾 2

1.3认证协议的安全问题的研究进展 3

1.4本文的研究背景及组织结构 5

第二章 HLPSL协议描述语言 7

2.1 HLPSL语法 7

2.2 基于HLPSL语言的安全协议描述方法 10

第三章 形式化分析工具 13

3.1 协议形式化分析逻辑 13

3.2 SPAN形式化分析工具 14

第四章 SSL协议的形式化分析 18

4.1 基于HLPSL语言的SSL协议描述 18

4.2 SSL协议的描述准确性 23

4.3 SSL协议的安全性分析 23

4.3.1 OFMC分析及攻击仿真 24

4.3.2 ATSE分析及攻击仿真 25

4.4 SSL协议的安全性改进 27

第五章 Kerberos协议的形式化分析 30

5.1基于HLPSL语言的Kerberos协议描述 30

5.2 Kerberos协议的描述准确性 35

5.3 Kerberos协议的安全性分析 36

第六章 总结与展望 38

绪论

引言

随着互联网络以及基于互联网的业务的高速发展，计算机网络成为当前主流的交换信息所采用的重要手段^[1]。计算机网络改变了一代人的生活习惯，传统的纸质书信被电子邮件、聊天工具取代；实体商店被网店取代。计算机网络缩短了人与人之间的距离，从最早的及时文字聊天，发展为网络语音通话，再到网络视频通话。无论军用还是民用，计算机网络都具有举足轻重的地位，并快速渗入到社会生活的各个领域。

然而计算机网络带来便利的同时，人类遭受一系列由于网络引发的财产损失、隐私泄露、数据被篡改窃取、生命威胁的打击。大量互联网消息可能携带着木马、病毒。普通用户稍有不慎，很容易中招。而且有些病毒隐蔽性很高，有的甚至潜伏很久才爆发。一旦爆发，给用户带来的损失伤害难以统计。我们提倡提高用户的安全意识，增强防范警觉性，让用户从根本上认识问题的严重性。但是仅仅让用户防范远远不够，从源头提高网络环境的安全性应该是关键，应该避免未授权用户访问关键信息，应该避免非法实体获取用户数据，篡改和伪造数据，应该保证网络环境不安全的情况下用户依然能够安全获得数据，应该保证能够被授权并控制信息流向及行为。

在硬件、软件及协议设计和具体实现上考虑网络安全，抵御对系统造成的安全隐患，增强抵抗外部入侵攻击的能力。这其中协议安全漏洞不容忽视。在各种服务的实现而不依附实体程序中，本地程序、远程服务端的程序都会造成协议的安全隐患。这些安全隐患轻则影响服务质量，严重时服务器会直接崩溃。因此采用高度安全的实施策略，十分必要去保障网络的安全性，尽早发现其中隐藏的安全漏洞，抵御潜在的攻击风险。在这些策略之中，认证协议对于保障网络安全显示出重要的作用。

然而统计显示，认证协议被新开发的数量和规模远远超过人类严格分析和验证的能力，认证协议势必存在大量的安全漏洞。这对于需要认证协议标准并投入运用的公司企业是一个严重问题；对于个人用户来说，他们需要保障个人数据隐私安全，也同样构成问题。而且设计安全协议时极易出错^[2]，即使只讨论最基本的认证协议。

认证协议的安全性分析一直以来是信息安全领域重点研究的内容之一^[3]。研究内容包括在协议中认证进行交互的主体身份；确保安全有效地分配密钥和保守各种秘密。但是设计和分析一个网络安全协议任务艰巨，极难实现。即便最简单的安全协议考虑安全性、周期性并且无冗余这些要素都要投入大量人力物力。为克服艰巨的任务，人们提出多种的分析方法辅助协议设计，形式化分析方法^[4]是其中的很重要的手段。人们投入了大量的精力，同时开发出相关的协议验证工具，取得了不错的成果。

1.2安全协议

1.2.1安全协议的概念与作用

安全协议是通过密码技术进行消息交换并获得安全保密性的通信协议，也可以称之为密码协议。但是单纯依靠密码算法不能完全保障网络安全，实体间的认证、安全地分配密钥或其他各类秘密是重中之重。通信协议是两个及以上的主体为了完成某种目标任务进而采取的一系列措施。以上定义可以归纳为三层。1.协议是一个有序的过程，也就是说每一步骤的执行必须等到前一个步骤执行完才能开始；2.至少有两个协议的参与者；3.一系列措施及步骤执行完成后，必须实现了某种任务。通过正确使用加、解密技术解决传递消息的安全问题是安全协议的目标。这些安全问题往往表现出不可抵赖性，消息的授权访问控制保障消息的可用性，实现消息的机密性，实现信息和身份的鉴别性，保证数据的完整性等方面。

安全协议按最基本的作用分为三类：认证协议、密钥交换协议、认证和密钥交换协议。密钥交换协议解释为会话过程中安全建立密钥，往往使用对称或非对称密码、数字签名等技术完成密钥交换。认证协议使用哈希函数、口令证书等加密的方式认证主体身份，其作用是确认参与者的身份，并为主体分发会话密钥。认证和密钥交换协议是完成通信实体的身份认证，同时实现密钥交换。

1.2.2认证协议的发展历史

Needham-Schroeder协议诞生于1978年，从出现的时刻算起，安全协议经历30多年的演变。 NSSK和NSPK协议是Needham-Schroeder协议在非对称密码和对称密码下的两种版本，早期较为经典的著名的安全协议还包括有Otway-Rees协议、Yahlom协议和Wide-Mouth Frog协议等，及重要的一些实用的协议，CCITT X.509协议和Kerberos协议。这些早期的安全协议常常被作为安全协议分析的样本，当新的分析方法出现时，率先分析这几个重要协议，从而判断分析方法是否有效性。

Clark和Jacob在1997年对安全协议总结和概况之后，列举了众多拥有实用性和研究价值的安全协议。根据学者们的调研，安全协议^[2]分类如下：“以下ISO系列协议属于无可信第三方的对称密钥协议：ISO系列协议包括ISO对称密钥单边认证协议、相互认证协议、Andrew安全RPC协议等等。以下ISO系列协议属于应用密码校验函数的认证协议：应用CCF的单边认证协议、相互认证协议。具有可信第三方的对称密钥协议包括NSSK协议、Yahlom协议等。对称密钥重复认证协议含有：Kerberos协议版本5、Neuman-Stubblebine协议等。无可信第三方的公开密钥协议包括以下ISO协议版本：公开密钥单边认证协议、相互认证协议、并行相互认证协议、Diffie-Hellman协议等。具有可信第三方的公开密钥协议包括NSPK协议。”

1.2.3 认证协议的安全隐患回顾

安全协议本质上由几行程序组成，例如分配密钥的安全协议。故安全协议的分析归根结底是修改并查证这些程序。然而与运行计算机程序和执行指令避免潜在的问题不同，非法用户的主要目标是在安全协议的运行期间利用漏洞并通过滥用指令获得或改变重要信息。这种危险是灾难性的。程序执行中完成消息交换并存在制约和相互作用；多种密码体制的使用令安全协议存在大量安全漏洞。

D.Spinellis和S.Gritzalis^[6]按照产生安全缺陷的原因和对应的攻击方式，将安全缺陷进行分类如下：

• 基本协议缺陷

基本协议缺陷指的是在设计过程中很少甚至没有考虑防范攻击造成协议漏洞，例如应用对称密码系统加密消息时，容易遭受中间人攻击。

• 陈旧消息缺陷

陈旧消息缺陷主要针对协议设计时没有引入新鲜性参数，使得攻击者能够对于消息进行重放攻击，这些往往包含消息目的地攻击和消息源攻击。

• 口令/密钥猜测缺陷
• 用户习惯从常用的词汇里面选择自己的偏好词作为自己的口令，攻击者往往把握用户的这种心理猜测口令，针对性地攻击；不安全的伪随机数生成的算法来构造密钥的时候，攻击者能够恢复已经不再安全的生成算法构造出的密钥。
• 内部协议缺陷

内部协议缺陷往往指的是至少有一个协议主体不能完成所有必需的协议交换，协议最终不可达，导致产生缺陷。

• 并行会话缺陷

并行会话缺陷往往指的是缺乏防范并行会话攻击的意识，使得攻击者参与协议交换过程中获得了协议中有价值的信息。并行会话攻击包括了单一角色和多角色的并行会话缺陷等等。

• 密码系统缺陷

密码系统缺陷往往指的是使用相应的密码算法造成机密性和完整性不能具备，安全协议存在并产生缺陷。

当前热门的安全漏洞攻击有brute-force attack暴力攻击。这种暴力攻击将编辑用户名列表、向服务器发送名字申请证书作为攻击手段，力求取得信任。还有利用特洛伊木马盗窃有效的证书和私钥。这种攻击主要攻击私钥，而私钥是证书安全系统的核心。

1.3认证协议的安全问题的研究进展

单纯依靠设计很难保证协议符合安全目标。必须借助形式化方法辅助设计和分析。20世纪70年代末期以来，众多的形式化研究方法涌现，这些方法中，基于知识与信念推理的模态逻辑方法、基于定理证明的分析方法、SPI演算方法等具有代表性。1996年Lowe提出模型校验技术并分析安全协议。模型校验技术用于验证有限状态的系统，是一种自动化验证技术。下面将认证协议的分析方式归纳如下：

• 模型检测

模型检测^[7]是通过穷举系统所有的可能的输入，对给定的系统模型，搜索其中的所有的状态空间，来达到验证系统所期望的性质的目的。基本原理图如1.3.1所示。

图1.3.1模型检测

模型检测与知识信仰逻辑和定理证明方法相比具有两个优势：一、支持并且能自动验证待检测系统是否满足协议规范；二、如果不满足协议的设计规范，模型检测器能够给出反例，以错误轨迹的形式反馈给用户，定位出错位置准确而便捷，进而修改模型。但模型检测也存在两个弱点：一、只适合验证有限状态系统，系统存在无限状态不能直接验证；二、对状态空间进行搜索大规模的系统易出现状态爆炸的问题，容易导致验证过程的异常终止。

模型检测与另外两种形式化方法的相同之处：验证前均需要假设，故验证结果与实际情况不能完全一致；分析结果也不具完备性，不可能完整检测和分析协议。不同之处：逻辑推理工具识别关键假设，但不能比较详细地描述攻击过程；模型检测工具能够对攻击路径进行模拟，但是需要人为分析攻击结果，主观性较强；定理证明方法基于定理或公理推导，进而证明协议是否安全；模型检测在发现新的攻击方面能力较强；模型检测能够实现高度自动化，其他两种方法不具备。

• 协议组成逻辑

协议组成逻辑^[4]是最近出现的用于证明网络协议安全性的新方法。中心思想是与行动相联系的断言将抑制包含这种行动的协议执行操作。这授予用户权力，解释协议中存在的各种可能运行的情况，而不需要解释可能被攻击者操作的步骤。然而，对协议组成逻辑（PCL）的研究仍处于开始阶段，更多更好地研究应该被积极投入。

• Fuzzing测试技术

Fuzzing是一种自动化软件测试技术，它是让外部输入的数据影响程序内部的一系列执行行为。Fuzzing在挖掘程序漏洞及检验程序安全性方面是一种有效的测试方法，因此受到安全专家与软件开发商的重视。Fuzzing还能够验证软件的健壮性，验证侧重点是目标的交互过程，聚焦输入与输出Fuzzing本质上是黑盒测试技术。Fuzzing的工作过程如下：特定的测试工具构造出大量半有效的测试数据，合成输入参数时按照目标处理方式，然后发送至待测试目标的交互点。Fuzzing监控状态，收集过程中的异常细节，对异常分析定性，进而发现目标的安全漏洞。在Peach框架下的Fuzzing工具在实际使用中存在不足之处，目前不存在高效并泛用的Fuzzing工具。

• SPIN

SPIN^[8]工具适用于并行运算系统，尤其能够辅助分析协议，验证是否满足一致性。它以PROMELA（Process Meta Language）作为输入语言，用SPIN工具对模型进行检测，首先需要证明公式。

SPIN工具具有以下几个鲜明特点：

• 开源性。方便使用者继续研究和改进。
• 不固定。自动化执行，能够相互交叉。
• 部分状态检验。On-the-fly技术自动对系统的部分状态进行检验，不必构建全局状态图。
• 简便直观。提供类似C语言的建模语言，有很强的直观性。
• 描述精确。引入线性时态公式，在描述系统时所需满足的性质精确，并在原有基础上得到了提高。
• 串空间模型

串空间模型是典型代数证明方法。它基于不变集，将安全属性和协议描述转换成图结构。使用串空间模型，有两种描述协议的方法：一种是描述主体行为时用消息传代数；另一种是画出协议的传送过程，依靠图的方式。串空间模型引入偏序结构，反映因果关系，有效避免了状态空间爆炸的问题。空间爆炸问题在模型检测方法中普遍存在。同时在协议执行时，用图示的方法表示执行过程，便于借助已有的图理论和算法分析安全协议。利用串空间构建匿名框架^[3]，完备了整个匿名系统的研究。但也存在不足：研究新匿名性框架具有局限性，被动型攻击者受限于网络中；在相对简单的网络环境中，匿名性分析协议过程仍然很复杂。今后工作重点是模型建立分级，设计并实现自动化分析的匿名工具。

串空间模型是一种混合方法，将定理证明和协议迹的方法相结合。经过实验验证，串空间模型是分析协议实用、直观和严格的方法。命题和推理规则组成模态逻辑方法，基于知识和信仰推理。其中BAN类逻辑最为著名^[9]。基于定理证明的分析方法分为两类，证明构造法和推理构造法。根据Dolev-Yao模型，SPI演算方法是假定每一步的协议执行都会与攻击者的步骤执行相交叉。SPI演算增强与扩充了PI演算，同时支持密码系统原语，这样能够对于基于密码系统的安全协议进行描述。

1.4本文的研究背景及组织结构

设计一个符合认证目标的、正确的、没有冗余的协议也相当困难，尽管认证协议的参加协议主体只有两三个，交换的消息只有三到五条。在开放网络中，例如互联网，应该保证协议安全工作在最坏情况的环境中。糟糕的情况可以是入侵者窃听或者篡改消息，我们称之为攻击者或敌人。严重的攻击甚至不需要破解密码，只要找出协议的弱点就能被实施,例如攻击者扮演诚实代理并发起“冒充攻击”；一个协议的会话消息也就是协议的一次执行被应用于其他会话并发起“重放攻击”。这些攻击可能有时来源于协议设计时一个微小的错误的想法，往往容易被忽略。就算人类花费大量精力认真检查协议，也很难查出协议存在的漏洞，很难决定各种复杂方式，因为不同的协议会话可能在恶意入侵的干扰下彼此交织。

剩余内容已隐藏，请支付后下载全文，论文总字数：40192字

相关图片展示：