物联网安全协议形式化分析与验证-张玲玲.pdf

《物联网安全协议形式化分析与验证-张玲玲.pdf》由会员分享，可在线阅读，更多相关《物联网安全协议形式化分析与验证-张玲玲.pdf（57页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、 论 文 题目 物联网安全协议形式化分析与验证 聊城大学 分 类 号 TP319 单 位 代 码 10447 密 级 无 学 号 1210170102 硕 士 学 位 论 文 论文题目 物联网安全协议形式化分析与验证 作 者 姓 名 张玲玲 专 业 名 称 计算机软件与理论 指导教师姓名 谢圣献 教授 学 院 计算机学院 论文提交日 期 2015年 4月 分 类 号 TP319 单 位 代 码 10447 密 级 无 学 号 1210170102 硕 士 学 位 论 文 论文题目 物联网安全协议形式化分析与验证 作 者 姓 名 张玲玲 专 业 名 称 软件工程 指导教师姓名 谢圣献 教授 学

2、院 计算机学院 论文提交日 期 2015年 3 月 原 创 性 声 明 本 人郑重声明：所提交的学位论文是本人在导师的指导下，独立进行研究取得的成果。除文中已经注明引用的内容外，论文中不含其他人已经发表或撰写过的研究成果，也不包含为获得聊城大学或其他教育机构的学位证书而使用过的材料。对本文的研究作出重要贡献的个人和集体，均已在文中以明确方式标明。本人承担本声明的法律责任。 学位论文作者签名： 日期 导 师 签 名 ： 日期 学位论文使用授权声明 本学位论文作者完全了解聊城大学有关 保留、使用学位论文的规定，即：聊城大学有权保留并向国家有关部门或机构送交学位论文的复印件和磁盘，允许论文被查阅和借

3、阅。本人授权聊城大学可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或其它手段保存、汇编学位论文。 学位论文作者签名： 日期 导 师 签 名 ： 日期 聊城大学硕士学位论文 摘 要 物联网技术在各行各业应用越来越广泛， 对物联网技术的研究也越来越多。随着物联网技术中硬件和软件的广泛应用， 安全问题也日益突出。对消息传递中的通信主体进 行身份验证， 对传输的数据进行保密，是物联网技术发展中安全要求的重要部分。 形式化的分析和验证方法是通过形式化的语言进行安全协议的建模， 根据前面的假设进行验证分析协议的安全性。形式化的分析方法是当前安全协议研究的重要方法。越来越多的形式化

4、分析方法被提出，来验证协议是否存在安全隐患。 本文 首先阐述了 物联网的概念及安全协议的基础知识， 针对安全协议的形式化分析方法进行了假设、分析和验证。主要工作有： 第一，对物联网概念和物联网安全协议进行了综述，分析了形式化分析法的分类和基础。 第二，对基于串空间模型理论的形式化验 证方法进行了分析，并通过对 N-S协议进行分析，发现其中存在的安全漏洞，并对其进行了改进。 第三，利用串空间模型理论，在安全协议的设计过程中很好的进行了指导。对设计出的安全协议进行了 验证和分析，证明了协议的安全性。 关键字： 物联网；安全协议；形式化验证；串空间模型 聊城大学硕士学位论文 ABSTRACT The

5、 technology of networking is applied more and more widely in all walks of life. The research to the technology of networking more and mor. With the wide application of the hardware and software technology of the technology of networking, security issues are also increasingly prominent. Authenticatin

6、g to the communication subject messaging, confidential to the confidentiality of transmitted data, is an important part of safety requirements of the development of the Internet of things technology. Methods of formal analysis and verification is modeled by a formal language for security protocols.

7、Verification and analysis the security of the protocol according to the previous assumption. Formal analysis method is an important method to study the current security protocol. Formal analysis methods are put forward more and more, To verify whether the protocol hidden safety problems. This paper

8、first describes the basic knowledge of concepts and security protocols of the networking, Hypothesis 、 analysis and verification to the security protocol formal analysis methods. The major job is : First, describing to the concept and security protocols of net networking, analyzing the classificatio

9、n and basic law to the formal analysis methods. Second, analyzing to the formal verification method based the theory of strand space model, and analyzing to the N-S protocol, discoed the security vulnerability exist, and improved it. Third, in the design process of security protocols in very good fo

10、r guidance using the Strand space model theory. Verified and analyzed to the design of the security protocol, prove the security of the protocol. Keyword: The Internet of things; Security protocol; Formal verification; 聊城大学硕士学位论文 Strand space model 目 录 第一章 绪论 . 8 1.1 研究背景和意义 . 8 1.2 国内外研究现状 . 2 1.3

11、本文的结构 . 3 1.4 本文主要研究成果 . 4 第二章 物联网及安全协议形式化概述 . 5 2.1 物联网的发展 . 5 2.2 物联网的定义 . 5 2.3 物联网的研究现状 . 6 2.4 物联网体的体系结构 . 7 2.5 物联网关键技术研究 . 9 2.6 安全协议形式化研究综述 . 12 2.7 安全协议形式化相关研究 . 17 第三章 利用串空间模型对安全协议进行形式化分析与验证 . 23 3.1 基本概念 . 23 3.2 攻击者模型 . 27 3.3 利用串空间理论模型对安全协议进行形式化分析和验证 . 29 第四章 基于认证测试方法的安全协议验证和设计 . 31 4.1

12、 认证测试方法基本概念和原则 . 32 4.2 N-S 公钥协议的验证和改进 . 35 聊城大学硕士学位论文 4.3 N-S 协议的改进及验证 . 38 4.4 基于认证测试方法的 N-S 公钥协议再设计 . 39 第五章 结论与展望 . 45 参考文献 . 46 致 谢 . 49 聊城大学硕士学位论文 第一章 绪论 引言 随着网 络的普及 智能设备的应用，人们希望在任何时间和任何地点，都可以对事物进行控制，能够第一时间与智能设备进行通信，因此物联网技术应运而生。但随之而来的是物联网的安全，对全世界安全行业提出了新的要求和希望。本文希望通过对常见的网络安全协议形式化分析与验证， 使 用户 对

13、网络安全 有全面认识。 1.1 研究背景和意义 物联网是近几年发展起来的一个新技术，严格意义上说它应该是信息技术的一个重要部分。可以通俗的用“物联网就是物体和物体之间的互联”来表示。物联网技术被称为信息业发展的第三次革命，它能够通过识别技术、云计算技术和智能 感知系统与网络进行深 度 融合，并应用于生产领域中 1。 物联网的定义包含两个方面，一是其核心仍然是网络，是在网络基础上的扩展和延伸。其次，用户端由单纯的计算机，电子产品扩展到了任何物体之间，只要具备了智能功能，就可以并入到互联网，进行信息的交互和通信，也就是刚才提到的物物相息。 物联网技术的应用其实是物联网技术与生产过程想结合，可以说

14、互 联网是一个应用。因此，物联网发展的关键就是进行创新，所以创新是物联网发展的关键技术，也可以说是物联网的灵魂 2。 物联网技术出现后，各国政府和企业都高度重视，学术界也开展了 对物联网技术的理论研究。近些年，物联网技术 在农业、家居、航空航天、军事、医疗等领域应用越来越广泛， 这些领域都是关系到国民生计和国家安全的关键领域，也成了国外敌对势力，不法份子攻击的目标。物联网由三个层次组成，分别是感知层、网络层和应用层，它的核心部分仍然是网络。物联网 作 为互联网特殊的一部分，它对安全有着更多的需求。其中，对物联网信息传送过程中，双方的主体身聊城大学硕士学位论文 2 份进行验证，对传输数据进行加密

15、，保证数据传输不被攻击，是物联网应用下一步要解决的问题，这就涉及到安全协议。 安全协议，也叫密码协议，是以密码学为基础的，属 于一种信息传递协议，目的是为在网络中传输的各种数据提供安全的信息传递服务。密码学是安全协议存在的一个基础，但是网络安全并不能够完全依靠密码学中的算法。安全协议是互联网一个重要的组成部分，通过对通信双方实体的验证，双方之间的安全密钥的分配，发送和接收消息的确认等 3。 自从互联网诞生之日起，网络安全就被各方关注，对于安全协议的设计分析及应用也 越 来越多。现存的安全协议的设计中还存在着过程复杂，需要人工设计，需要有丰富的经验，并且劳动重复性高，效率低。许多当时被认为是安全

16、的协议，在经过多年运行后，被检测出存在 安全 漏洞。 进行修改后，又会引起其它亲的安全隐患。在进行安全协议的设计过程，也存在着需求和设计脱离的情况。在安全协议经过分析验证，发现存在严重的安全漏洞后，需要全部重新设计和验证，需要花费大量的人力物力和财力，造成浪费。 互联网的发展，新的攻击技术和方法手段也不断涌现，安全协议的设计也会越来越困难。 1.2 国内外研究现状 安全协议对互联网尤其是物联网起着非常重要的作用，它是网络安全构造的一个重要基础。最初的安全协议是 Needham Schroeder 协议 （简称 N-S）协议，它诞生于 1978 年，至今已经三十多年 了，对安全协议的研究仍然处于

17、初级阶段，学术界研究者在安全协议的设计和分析还会面临巨大挑战。 虽然说安全协议发展经过了三十多年了，但在安全协议的设计和分析方面，真正的用于商业的产品还没有出现，更不要说工业级的安全协议。 另外，设计出的安全协议，如何对 其 进行有效的证明，如何提高安全协议的分析效率，如何得出最优协议，都是下一步学术界应该不断探索的一个重要课题。 安全协议研究经历了三十多年，有关人员对于安全协议的分析提出了很多方法和模型，最为典型的一类就是形式化分析方法 4。 Dolev和 Yao在 1983年发表的论文 中首次将形式化的方法用于对安全协议进行分析 5。 牛津大学 Hoare提出 了CSP，它主要是通过利用代

18、数理论对并行系统进行设计与分析 6。 通用模型检测聊城大学硕士学位论文 3 工具 FDR是基于 CSP而实现的， 它主要由 欧洲的 Formal Systems LTd公司 来完成7,8。 Song等人 在 1999年设计出 了 协议自动验证工具 Athena，它主要是将串空间模型理论与检测技术相结合 9； Guttman和 Thayer在 2000年发表的论文中，首次提出了基于串空间理论 模型 的认证测试方法，这是串空间理论发展的一个重要突破 10。 到 目前为止，针对 传感网络 RFID 安全协议 也已经 被提出 来，相关文献也有了报道。但这些都没有形式化的设计与分析，而是基于传统的非形式

19、化的。例如，Sarma 提出的 Hash-Lock 协议 11，它主要是针对无 线 传输网络而设计的； Weis等人提出 了 随机化 Hash-Lock 协议 12 ； David 等人 提出 的 David 数字图书馆协议 13； Rhee 等人提出 FID询问 -响应 分布式 R认证协议 14， LCAP协议 15，再次加密机制，基于授权代理的协议等等。 但是在安全协议的应用中，有关协议也被发现越来越多的安全漏洞 。例如，Hash-Lock协议， 它对于假冒攻击没有办法辨别。 随机化 Hash-Lock协议 对于攻击者的恶意攻击和跟踪没有办法抵御； Hash 链协议 由于对于后台数据库没有

20、进行认证，也容易被攻击者攻击。 相比于传统的传感网，物联网传感网络通过传感器获取数据，不仅能够在本地应用，也可以通过数据云平台传递到远端。由于在服务器端还需要对本地服务器和传感器进行双方主体认证，所以对于物联网传感网进行传输时，要设计专门的安全协议。对于物联网安全协议的文献和报道，相对较少 16。 1.3 本文的结构 第 1章 通过对目前物联网的 形式分析和研究，说明本研究的 目的和意义，国内外的研究现状，研究内容和论文的组织形式。介绍了物联网的定义、 体系结构、现状。对于安全协议的形式化分析和验证进行了说明。 第 2章 介绍了本文研究所涉及的基础知识， Dolev-Yao模型，串空间理论、串空间模型的测试方法等，为后面的章节提供理论基础。 第 3章 主要分析了 N-S安全协议的基础，并利用串空间理论对 N-S安全协议加以改造，引入了消息类型检测概念。 第 4章 对改进的 N-S安全协议进行了建模和测试及证明。