学位论文 > 优秀研究生学位论文题录展示

物联网传感网络安全协议形式化研究

作　者: 李俊霖
导　师: 周华
学　校: 云南大学
专　业: 系统分析与集成
关键词: 物联网安全协议形式化通信顺序进程定理证明
分类号: TN915.08
类　型: 博士论文
年　份: 2011年
下　载: 1488次
引　用: 2次
阅　读: 论文下载

内容摘要

目前,对物联网的研究越来越深入,物联网在未来社会的发展和应用越来越广泛,随着各种物联网硬件和应用软件开发和研究,物联网的安全问题也凸显出来,如何对物联网的通信主体进行身份认证,如何对数据进行保密安全的传输,这是一个迫切需要研究和解决的应用需求。安全协议在通信主体的身份认证、密钥的分配和数字签名等方面发挥着重要作用,但是,安全协议的安全性设计、分析和证明长期以来一直是信息安全研究的重点和难点问题,随着攻击的新手段和新技术不断涌现,安全协议的设计,分析和证明也在不断的接收新的挑战。本文在当前比较公认的物联网概念和体系结构基础上,针对物联网传感网络的安全协议的形式化设计,分析和证明展开研究,主要工作为：1、通过分析当前比较公认的物联网概念和体系结构,对物联网体系结构与传统的网络体系结构作了分析比较,得出物联网传感网络的特点和安全属性；2、根据物联网传感网络的特点和安全属性,提出针对物联网传感网络攻击者的模型：3、根据物联网传感网络的特点和安全属性,提出一种基于无线网络的物联网传感网络SNIT(The Sensing Network of the Internet of Things)模型；4、针对SNIT模型,对通信主体进行抽象,提出一种基于协议元的形式化设计方法,该方法首先对协议元进行选择和设计,并对其进行基于UM击模型下的SK安全属性进行证明；5、针对SNIT模型提出一种SNIT协议,该协议根据发起通讯请求的通信主体的不同SNIT办议又分为SNIT_C, SNIT_S_三个协议,并对三个协议进行形式化描述和攻击者建模；6、采用CSP对SNIT协议进行形式化分析和模型验证；7、采用串空间理论对SNIT协议进行定理证明,对模型的无穷状态空间进行推理,解决模型验证所不能完成状态空间爆炸问题；总之,本文提出对安全协议的形式化设计、分析和证明较之于传统的非形式化设计和分析,具有较强的数学理论基础,可以保证在攻击者模型所具备的攻击条件下安全协议的可靠性,保密性和数据一致性。

全文目录

摘要  3-5
Abstract  5-6
目录  6-9
第1章绪论  9-19
  引言  9
  1.1 研究背景  9-10
  1.2 研究内容和方法  10-14
  1.3 研究原则和思路  14-16
  1.4 研究流程及成功标准  16-17
  1.5 论文创新点  17
  1.6 论文组织结构  17-18
  1.7 本章小结  18-19
第2章物联网及安全协议形式化研究综述  19-31
  引言  19
  2.1 物联网的发展  19-20
  2.2 物联网的定义  20
  2.3 物联网的体系结构  20-23
    2.3.1 应用层  21-22
    2.3.2 感知层  22
    2.3.3 网络层  22-23
  2.4 物联网的研究现状  23-24
  2.5 无线传感网络综述及研究现状  24-25
  2.6 安全协议形式化研究综述  25-30
    2.6.1 安全协议设计的困难性  26
    2.6.2 形式化方法设计  26-28
    2.6.3 形式化方法分析  28-29
    2.6.4 形式化方法验证  29
    2.6.5 形式化方法定理证明  29-30
  2.7 本章小结  30-31
第3章相关研究基础  31-45
  引言  31
  3.1 Dolev-Yao模型  31-33
    3.1.1 攻击者的知识和能力  32
    3.1.2 攻击者的行为  32-33
  3.2 通信顺序进程  33-35
    3.2.2 CSP基本定义  33-35
    3.2.3 CSP运算符  35
  3.3 攻击者模型  35-37
  3.4 运行环境模型  37-38
  3.5 CK模型  38-40
  3.6 CSP模型验证  40-41
  3.7 串空间定理证明  41-43
  3.8 基于密钥的单向杂凑函数  43-44
  3.9 异或运算  44
  3.10 本章小结  44-45
第4章物联网传感网络建模  45-53
  引言  45
  4.1 物联网传感网络的特点  45-46
  4.2 物联网传感网络结构建模  46-49
  4.3 物联网传感网络建模分析  49-50
  4.4 物联网传感网络通信主体的抽象  50-52
  4.5 本章小结  52-53
第5章基于SNIT的协议元库构建方法  53-60
  引言  53
  5.1 协议元库的构建目标  53
  5.2 协议元库的构建思路  53-54
  5.3 协议元的选取标准  54
  5.4 协议元库的构建  54-59
  5.5 协议的自动化生成  59
  5.6 本章小结  59-60
第6章 SNIT协议建模  60-83
  引言  60
  6.1 相关符号及术语  60-61
  6.2 SNIT协议设计目标  61
  6.3 SNIT协议设计  61-63
  6.4 SNIT协议的安全分析  63-69
    6.4.1 AM模型中的攻击者行为能力模型  63
    6.4.2 SNIT协议在AM模型下的SK安全  63-66
    6.4.3 SNIT协议的模型认证器  66
    6.4.4 SNIT协议在AM模型到UM模型的转化  66-68
    6.4.5 SNIT协议的安全分析  68-69
  6.5 SNIT协议建模分析  69-71
  6.6 SNIT_C协议建模  71-73
  6.7 SNIT_M协议建模  73-76
  6.8 SNIT_S协议建模  76-79
  6.9 SNIT协议自动化分析  79-82
  6.10 本章小结  82-83
第7章 SNIT协议模型验证  83-120
  引言  83
  7.1 攻击者行为模型  83-85
  7.2 SNIT保密性分析  85-105
    7.2.1 SNIL_C的保密性  87-94
    7.2.2 SNIT_M的保密性  94-99
    7.2.3 SNIT_S的保密性  99-105
  7.3 SNIT认证性验证  105-119
    7.3.1 M对S的认证  107-113
    7.3.2 S对M的认证  113-119
  7.4 CSP自动验证工具  119
  7.5 本章小结  119-120
第8章 SNIT协议定理证明  120-150
  引言  120
  8.1 对串空间的改进  120-122
  8.2 协议正确性条件  122-123
  8.3 攻击者能力模型  123
  8.4 SNIT协议的证明  123-148
    8.4.1 SNIT_C  126-133
    8.4.2 SNIT_M  133-140
    8.4.3 SNIT_S  140-148
  8.5 证明结果  148-149
  8.6 本章小结  149-150
第9章总结与展望  150-154
  引言  150
  9.1 研究成功标准的确认  150-151
  9.2 总结  151-152
  9.3 未来工作展望  152-153
  9.4 本章小结  153-154
参考文献  154-158
附录A 攻读博士学位期间主持和参与的项目  158-159
附录B 攻读博士学位期间发表和录用的论文  159-160
附录C 攻读博士学位期间获得的奖励  160-161
附录D 攻读博士学位期间获得的证书  161-162
致谢  162-164
告别语  164

物联网传感网络安全协议形式化研究

内容摘要

全文目录

相似论文