无线传感器网络SPIN协议的改进及验证

在无线传感器网络中,对SPIN协议的研究主要是通过仿真进行的,很少有对其进行形式化验证.本文在SPIN协议的基础上进行改进得到了适用于有损网络的协议--SPIN-E协议,并使用有色Petri网对SPIN-E协议进行形式化建模,通过CPN Tools对协议的活性、可达性、有界性等特性进行了分析和验证.     

基于SPIN的无线传感器网络安全协议建模与分析

模型检验方法在有线网安全协议的分析和设计方面取得了巨大成功。无线传感器网络对安全协议同样具有严格的要求;与有线网相比,无线传感器网络在通信环境和网络节点等方面都更为脆弱,为相应的安全协议的分析和设计提出了挑战。提出了一种适用于无线传感器网络的安全协议形式化建模分析方法。它充分借鉴了传统有线网络安全协议的建模方法,在其基础上充分考察了无线传感器网络的通信环境以及网络节点,建立起一个全面并且直观的安全协议运行模型。以A.Perrig等人提出的SPINS安全协议为例,应用模型检验工具SPIN对其认证性和机密性等安全需求进行了分析验证,发现了该协议存在的漏洞。实例分析证实了模型检验方法在分析无线传感器网络安全协议时的有效性,从而推进了其在安全协议分析方面的应用范围。     

不可否认协议的Petri网建模与分析

Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用．作为一种特殊的安全协议,不可否认协议虽然已得到了多种形式化方法的分析,但还没有人使用Petri网来分析它们．以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其他形式化方法无法描述的协议性质．使用该方法分析Zhou和Gollmann于1996年提出的一个公平不可否认协议,可以发现该协议的一个许多其他形式化方法不能发现的已知缺陷．     

基于Petri网的协议并行化处理模型的描述和验证

本文提出了一个ＯＳＩ／ＲＭ运输层协议并行处理模型，以适应协议的高效处理，根据模型特点，使用Ｐｅｔｒｉ网作为形式化描述工具，对该模型进行描述，分析和验证。     

无线传感器网络LEACH协议的Petri网模型及性能分析

Petri网是分析网络协议一种有效的形式化建模工具,基于对无线传感器网络LEACH协议运行机制的分析,为协议建立广义随机Petri网(GSPN)性能模型,并用SPNP软件对建立的性能模型进行分析,模型数据验证了模型的有效性,同时讨论了性能模型对协议的低功耗改进所起的指导作用。     

基于时延Petri网的密码协议分析及性能评估

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径，但是密码协议的形式化分析研究目前还不够深入，针对这一现状，该文提出用时延Petri网来表示和分析密码协议。该模型不但能够反映协议的静态和动态的特性，而且能够对密码协议进行时间、空间上的性能评估。作为实例，文章对MSR无线协议作了详细的形式分析和性能评估。最后，与其它形式化分析密码协议的方法作了比较。     

EAP-MD5协议的安全性分析与改进

安全协议的验证对确保网络通信安全极其重要,形式化分析方法使得安全协议的分析简单、规范和实用,成为信息安全领域的研究热点。针对802.1x/EAP-MD5认证协议,提出一种基于着色Petri网(CPN)的安全协议形式化验证方法,并给出具体的形式化分析过程。建立协议的CPN模型,分析协议执行过程中可能出现的不安全状态,利用CPN状态可达性判定这些不安全状态是否可达,从而验证协议的安全性。对于802.1x/EAP-MD5协议在中间人攻击下的安全漏洞问题,提出协议的改进方案,采用预共享密钥机制生成会话密钥加密交互信息,同时运用数字证书对服务器进行认证,以提升中间人攻击的难度及增强网络接入认证协议的安全性。     

基于安全协议代码的形式化辅助建模研究

随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。     

网络安全认证协议形式化分析

形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段。安全协议的形式化分析正成为国际上的研究热点。用于安全协议分析的逻辑需要对入侵者进行形式化建模,用于刻画入侵者能力。我们运用一种基于算法知识概念的逻辑分析安全协议,入侵者假定使用算法来计算其知识,入侵者的能力也通过对其所使用的算法作适当的限制来获得。运用模型检测器SPIN对TMN协议进行分析,实验结果证明了此方法的有效性,可方便地用于其他网络安全协议验证。     

一种基于Petri网的安全协议验证方法

安全协议是实现网络安全的关键,如何验证安全协议的安全性是一个非常重要的工作。论文提出一种基于着色Petri网的安全协议形式化描述与安全验证方法,此方法建立在逆向状态分析和着色petri网可达性矩阵的基础之上,并采用具体协议来验证该方法的有效性。     

无线传感器网络的路由协议研究

无线传感器网络（WSNs）是计算机、通信和传感器3项技术相结合的产物，因其巨大的应用前景受到了越来越广泛的关注。介绍了WSNs的一些特点，指出传统路由协议不能有效应用于WSNs的路由协议；然后分类阐述了当前较为典型的路由协议．分析了它们的优缺点；对比分析了这些协议的特点；总结了路由协议设计应满足的要求、存在的挑战以及可能的研究方向。     

无线传感器网络的路由协议研究

无线传感器网络(WSNs)是计算机、通信和传感器3项技术相结合的产物,因其巨大的应用前景受到了越来越广泛的关注。介绍了WSNs的一些特点,指出传统路由协议不能有效应用于WSNs的路由协议;然后分类阐述了当前较为典型的路由协议,分析了它们的优缺点;对比分析了这些协议的特点;总结了路由协议设计应满足的要求、存在的挑战以及可能的研究方向。     

无线传感器网络路由协议的分析与比较

无线传感器网络的路由协议设计与传统的无线ad-hoc网络有很多不同,资源高度受限和结点失效频繁是其面临的两大挑战,相关技术研究已经成为无线传感器网络研究中的热点.对近年来无线传感器网络路由协议的研究成果进行归纳、分析和比较,介绍了无线传感器网络的特点以及影响其路由协议设计的关键因素.根据协议的实现特点将无线传感器网络路由协议分为5类,对每一类涉及的重要协议进行详细阐述与分析,最后对这些协议的特点进行归纳和比较,并展望了未来这一研究方向的发展趋势.     

PEACH: Power-efficient and adaptive clustering hierarchy protocol for wireless sensor networks

The main goal of this research is concerning clustering protocols to minimize the energy consumption of each node, and maximize the network lifetime of wireless sensor networks. However, most existing clustering protocols consume large amounts of energy, incurred by cluster formation overhead and fixed-level clustering, particularly when sensor nodes are densely deployed in wireless sensor networks. In this paper, we propose PEACH protocol, which is a power-efficient and adaptive clustering hierarchy protocol for wireless sensor networks. By using overhearing characteristics of wireless communication, PEACH forms clusters without additional overhead and supports adaptive multi-level clustering. In addition, PEACH can be used for both location-unaware and location-aware wireless sensor networks. The simulation results demonstrate that PEACH significantly minimizes energy consumption of each node and extends the network lifetime, compared with existing clustering protocols. The performance of PEACH is less affected by the distribution of sensor nodes than other clustering protocols.     

无线传感器网络路由技术研究

无线传感器网络是当前研究和应用的热点,路由协议是其研究的重要领域.在比较与其它传统无线网络路由协议区别的基础上,归纳了无线传感器网络路由协议应具有的特性,并对近年来针对无线传感器网络提出的有代表性的路由协议进行了研究,总结了各种路由协议的特点和适合的应用场合,重点分析了它们的不足之处,最后指出了无线传感器网络路由技术未来发展的趋势.     

无线传感器网络路由协议分类研究

无线传感器网络具有与传统网络不同的特点,且与应用高度相关。传统网络及移动自组织网络的路由协议不能有效地用于无线传感器网络,因而研究人员提出了众多的路由协议。在介绍了无线传感器网络的特点及路由协议设计的关键问题之后,总结分析了现存的路由协议的分类方法,并对各类路由协议从路由策略、路由协议的特点、性能等多方面进行了对比分析,指出了各类路由协议的优缺点及其包含的路由协议。最后总结出未来的研究热点和发展趋势。     

三层建立虚拟簇的能量有效MAC协议

由于传感器节点本身不能自动补充能量或能量补充不足,节约能量是传感器网络MAC协议设计首要考虑的因素。而传统网络的MAC协议重点考虑节点使用带宽的公平性,提高带宽利用率和增加网络的实时性,这意味着传统网络的MAC协议不能直接用于无线传感器网络,需要研究新的适用于无线传感器网络的MAC协议。综合比较了已有的各种无线传感器网络MAC层协议优缺点,着重研究了EBRI-MAC协议,对这个协议进行了改进,提出TLVC-MAC 协议,采用基于路由信息分三层建立虚拟簇的方式进一步减少能量消耗,提高能量效率。     

层次式无线传感器网络中的协商机制研究

无线传感器网络由具有计算、通信和感知能力的小型自治实体组成,层次式体系结构作为一种有效的组织方式能够降低网络能量消耗,延长网络的生存周期。从多Agent系统的角度研究构成这种层次式无线传感器网络的相关协议和算法的意图协商过程,建立其协商模型,为层次式无线传感器网络路由协议或分簇算法提供一种评价和分析方法。基于该模型的实际网络协议分析表明,具有相同协商机制而意图信息量不同的层次式无线传感器网络在性能方面存在一定的差异,良好的意图和基于良好意图的完善协商机制可以有效提高网络的性能。     

无线传感器网络节能路由研究

分簇结构作为一种提高能源利用率、减少网络能耗的有效途径,成为当前无线传感器网络节能路由协议的研究热点。介绍和分析了LEACH、PEGASIS和HEED三种典型节能分簇路由协议,通过对三者的综合比较总结出现有分簇路由协议存在的问题,并提出相应的解决思路。解释了要想将WiFi应用于无线传感器网络面临的困难。最后,展望了无线传感器网络路由协议未来的研究工作。     

T-LEACH: The method of threshold-based cluster head replacement for wireless sensor networks

In wireless sensor networks, power is the most essential resource because each sensor node has limited batteries. Many kinds of existing clustering protocols have been developed to balance and maximize lifetime of the sensor nodes in wireless sensor networks. These protocols select cluster heads periodically, and they considered only ‘How can we select cluster heads energy-efficiently?’ or ‘What is the best selection of cluster heads?’ without considering energy-efficient period of the cluster heads replacement. Unnecessary head selection may dissipate limited battery power of the entire sensor networks. In this paper, we present T-LEACH, which is a threshold-based cluster head replacement scheme for clustering protocols of wireless sensor networks. T-LEACH minimizes the number of cluster head selection by using threshold of residual energy. Reducing the amount of head selection and replacement cost, the lifetime of the entire networks can be extended compared with the existing clustering protocols. Our simulation results show that T-LEACH outperformed LEACH in terms of balancing energy consumption and network lifetime.