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

• 作者: 朱伟龙 许家胜 陈传峰
• 来源期刊: 东南大学学报（自然科学版）
• 学科: 工学
• 关键词: 无线传感器网络 安全特性 新鲜性 形式化方法
• 年，卷（期）: 2012,（z2）
• 页码范围: 245-249
• 页数: 5页
• 分类号: TP393
• 字数: 4101字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0505.2012.S2.004

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈传峰	福州大学物理与信息工程学院	21	231	5.0	15.0
2	许家胜	福州大学物理与信息工程学院	2	0	0.0	0.0
3	朱伟龙	福州大学物理与信息工程学院	2	1	1.0	1.0