物联网安全协议形式化分析与验证

摘要

物联网技术在各行各业应用越来越广泛，对物联网技术的研究也越来越多。随着物联网技术中硬件和软件的广泛应用，安全问题也日益突出。对消息传递中的通信主体进行身份验证，对传输的数据进行保密，是物联网技术发展中安全要求的重要部分。　　形式化的分析和验证方法是通过形式化的语言进行安全协议的建模，根据前面的假设进行验证分析协议的安全性。形式化的分析方法是当前安全协议研究的重要方法。越来越多的形式化分析方法被提出，来验证协议是否存在安全隐患。　　本文首先阐述了物联网的概念及安全协议的基础知识，针对安全协议的形式化分析方法进行了假设、分析和验证。主要工作有：　　第一，对物联网概念和物联网安全协议进行了综述，分析了形式化分析法的分类和基础。　　第二，对基于串空间模型理论的形式化验证方法进行了分析，并通过对N-S协议进行分析，发现其中存在的安全漏洞，并对其进行了改进。　　第三，利用串空间模型理论，在安全协议的设计过程中很好的进行了指导。对设计出的安全协议进行了验证和分析，证明了协议的安全性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景和意义

1.2 国内外研究现状

1.3 本文的结构

1.4 本文主要研究成果

第二章 物联网及安全协议形式化概述

2.1 物联网的发展

2.2 物联网的定义

2.3 物联网的研究现状

2.4 物联网体的体系结构

2.5 物联网关键技术研究

2.6安全协议形式化研究综述

2.7 安全协议形式化相关研究

第三章 利用串空间模型对安全协议进行形式化分析与验证

3.1 基本概念

3.2 攻击者模型

3.3利用串空间理论模型对安全协议进行形式化分析和验证

第四章 基于认证测试方法的安全协议验证和设计

4.1 认证测试方法基本概念和原则

4.2 N-S公钥协议的验证和改进

4.3 N-S协议的改进及验证

4.4 基于认证测试方法的N-S公钥协议再设计

第五章 结论与展望

参考文献

致谢

攻读硕士学位期间发表的学术论文