公开(公告)号：CN103476033B

公开(公告)日：2016-04-06

申请号：CN201310456973.1

申请日：2013-09-25

Applicant: 南京大学

Inventor： 陈志 ,  彭超宇 ,  李宣东 ,  岳文静 ,  王林章 ,  曾雅芸

IPC: H04W12/12 ,  H04W80/08 ,  H04W84/18

Abstract: 本发明给出一种基于模型检验的无线传感器网络安全协议验证方法，用时间自动机所组成的状态迁移系统表示无线传感器网络安全协议，用模态/时序逻辑公式表示无线传感器网络中安全协议所需满足的条件，将对无线传感器网络安全协议验证转化为验证状态迁移系统是否为公式的一个模型。本发明在安全协议验证过程中充分考虑了无线传感器网络的特性，在模态/时序逻辑公式中加入时钟约束条件，能够对无线传感器网络安全协议进行全面的验证。

公开(公告)号：CN103476033A

公开(公告)日：2013-12-25

申请号：CN201310456973.1

申请日：2013-09-25

Applicant: 南京大学

Inventor： 陈志 ,  彭超宇 ,  李宣东 ,  岳文静 ,  王林章 ,  曾雅芸

IPC: H04W12/12 ,  H04W80/08 ,  H04W84/18

Abstract: 本发明给出一种基于模型检验的无线传感器网络安全协议验证方法，用时间自动机所组成的状态迁移系统表示无线传感器网络安全协议，用模态/时序逻辑公式表示无线传感器网络中安全协议所需满足的条件，将对无线传感器网络安全协议验证转化为验证状态迁移系统是否为公式的一个模型。本发明在安全协议验证过程中充分考虑了无线传感器网络的特性，在模态/时序逻辑公式中加入时钟约束条件，能够对无线传感器网络安全协议进行全面的验证。