无线传感器网络新鲜性的形式化分析

摘要：

为了更好地解决无线传感器网络的安全与隐私问题,使其具有更广泛的应用领域,提出了一种使用形式化方法Object-Z分析和验证无线传感器网络安全特性的新方法.该方法分析了一个基于Nonce机制的简单密钥协商协议的新鲜性问题.首先定义了协议使用到的数据类型和辅助函数等组件,然后建立了协议的3个角色模型:发起者、响应者和基站.在此基础上通过实例化角色对象构建了密钥协商协议模型,实现角色之间的相互通信,最后采用形式化逻辑推理的方式对协议通信过程的新鲜性进行验证.结果表明,使用Nonce机制可以保证传输数据的新鲜性,说明该分析方法对无线传感器网络的安全特性的分析是有效的.

关键词：无线传感器网络、安全特性、新鲜性、形式化方法

所属期刊栏目：42

分类号：TP393(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目61170245

在线出版日期：2013-06-03（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：245-249