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

Formal analysis of freshness in wireless sensor networks

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

In order to solve the security and privacy issues of the wireless sensor networks and ex- pand their application fields, a novel method which uses the formal method Object-Z is proposed to analyze and verify security features. In this method, the freshness of a simple key agreement proto- col based on the Nonce mechanism is analyzed. First, the protocol components such as data types and auxiliary functions are defined, and then three role models, i. e. , the initiator, the responder and the base station are built. A protocol model in which roles can communicate with each other is built by instantiating role objects. Finally, the freshness of communication process in the protocol is verified by formal reasoning. The results show that the Nonce mechanism can guarantee the freshness of transmission data, and the proposed method is valid in analyzing secure features.