【作者】 薛伟；

【导师】 沈明玉；

【作者基本信息】 合肥工业大学 ， 计算机软件与理论， 2012， 硕士

【摘要】 信息时代高效率快节奏的工作使人们忽视那些看似与正常系统运行关系不大其实贯彻全局的安全工作，终于使得安全工作的匮乏到达了引爆点。近年来的有线网安全事件呈指数级上升，使得专家学者们对无线网的安全性进行未雨绸缪的分析和研讨。作为无线网中的重要应用之一的无线传感器网络（WSN）因其在军事，工业，农业中的广泛应用和远大前景，其安全性更加值得研究方案和提出解决方法。不同于有线网，WSN节点间的物理信道是空气介质，而且节点通常部署在无人维护、不可控制的环境中。因此WSN的安全如何很大程度上由其安全协议决定。虽然在该领域已有先驱提出一些实用的协议，但这些协议对于应用不同的WSN局限性比较大、漏洞较多。安全协议的分析与设计已成为一项兼具创新性和挑战性研究课题。随着学术的深究和应用的进展，作为协议形式化分析中的翘楚可证明安全理论有效地应用于各种协议的分析和研究中。本文合适地将可证明安全理论中的CK模型引入WSN的安全协议SPINS的分析和论证。本文首先阐述了WSN的网络特性与安全需求，并在此基础上对SPINS协议的安全性进行初步的探讨。随后引入可证明安全理论并对其进行简单介绍，后文重点研究了CK模型的核心部分，并分析了其论证过程和证明方法。通过将CK模型中的理想模型和现实模型应用在SPINS协议中，将构建一个理想模型下与现实模型下SPINS协议相对应的新协议，分别在两种模型下对应的敌手ADV与UDV对它们进行形式化分析研究，通过各种攻击手段得出其安全性漏洞以及其满足的语义和多项式安全，最终推导出SPINS协议构成了现实环境中的安全通道的结论。更多还原

【Abstract】 In the information age, people are exhausted of high efficiency and fast-pacedbusiness, thus, those seemingly mean to all security job which though all of itcollapsed. Beause of rapidly rising network security events in these years, thesecurity of wireless network is analyzed and discussed by experts. As one of theimportant application, WSN is widely used in military, industrial, agriculture.Therefore, the security is worth of be researched and solved. The difference fromwired network is physical channel between of WSN is air medium. Usually, theyare distributed in uninhabited and uncontrollable environment. Thence the securitydepends on the protocols. Although some pratical security protocols have beenproposed, these are vulnerable and limited in different WSN applications. Analysisand design of security protocols has become both innovative and challengingresearch topics. With the research of academics and progress in applications,provable security theory that are important results in protocol formal analysiseffectively is used in the analysis and rescerch of the various protocols. In thispaper, CK model which is one of the provable security theories is recommended inSPINS protocol.First of all, network characteristics and security needed to be elaborated.Security of SPINS protocol was discussed preliminarily on this basis. Then,provable security theory was leaded into this paper and introducted briefly. Afterthat, core part of CK model was foused on. By ideal model and real model appliedin SPINS protocol, a new protocol which corresponds to SPINS protocol wasbuilded. Through the formal analysis results of two protocols’ models, securityloopholes which was derived from various attack means, its’semantics andpolynomial security, the conclusion that SPINS protocol was constituted of securitychannel in reality, was derivated.更多还原