东南大学学报（自然科学版）
東南大學學報（自然科學版）
동남대학학보（자연과학판）
JOURNAL OF SOUTHEAST UNIVERSITY
2012年
z2期
245-249
,共5页
无线传感器网络%安全特性%新鲜性%形式化方法
無線傳感器網絡%安全特性%新鮮性%形式化方法
무선전감기망락%안전특성%신선성%형식화방법
为了更好地解决无线传感器网络的安全与隐私问题,使其具有更广泛的应用领域,提出了一种使用形式化方法Object-Z分析和验证无线传感器网络安全特性的新方法.该方法分析了一个基于Nonce机制的简单密钥协商协议的新鲜性问题.首先定义了协议使用到的数据类型和辅助函数等组件,然后建立了协议的3个角色模型:发起者、响应者和基站.在此基础上通过实例化角色对象构建了密钥协商协议模型,实现角色之间的相互通信,最后采用形式化逻辑推理的方式对协议通信过程的新鲜性进行验证.结果表明,使用Nonce机制可以保证传输数据的新鲜性,说明该分析方法对无线传感器网络的安全特性的分析是有效的.
為瞭更好地解決無線傳感器網絡的安全與隱私問題,使其具有更廣汎的應用領域,提齣瞭一種使用形式化方法Object-Z分析和驗證無線傳感器網絡安全特性的新方法.該方法分析瞭一箇基于Nonce機製的簡單密鑰協商協議的新鮮性問題.首先定義瞭協議使用到的數據類型和輔助函數等組件,然後建立瞭協議的3箇角色模型:髮起者、響應者和基站.在此基礎上通過實例化角色對象構建瞭密鑰協商協議模型,實現角色之間的相互通信,最後採用形式化邏輯推理的方式對協議通信過程的新鮮性進行驗證.結果錶明,使用Nonce機製可以保證傳輸數據的新鮮性,說明該分析方法對無線傳感器網絡的安全特性的分析是有效的.
위료경호지해결무선전감기망락적안전여은사문제,사기구유경엄범적응용영역,제출료일충사용형식화방법Object-Z분석화험증무선전감기망락안전특성적신방법.해방법분석료일개기우Nonce궤제적간단밀약협상협의적신선성문제.수선정의료협의사용도적수거류형화보조함수등조건,연후건립료협의적3개각색모형:발기자、향응자화기참.재차기출상통과실례화각색대상구건료밀약협상협의모형,실현각색지간적상호통신,최후채용형식화라집추리적방식대협의통신과정적신선성진행험증.결과표명,사용Nonce궤제가이보증전수수거적신선성,설명해분석방법대무선전감기망락적안전특성적분석시유효적.
