利用类型推理验证Ad Hoc安全路由协议

被引：7

作者：

李沁 ^{[1
,2
]}

曾庆凯 ^{[1
,2
]}

机构：

[1] 南京大学计算机软件新技术国家重点实验室

[2] 不详

来源：

软件学报 | 2009年 / 20卷 / 10期

基金：

高等学校博士学科点专项科研基金;

关键词：

安全协议验证; ad-hoc网络协议; 安全路由协议; 类型推理;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简Dolev-Yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.

引用

页码：2822 / 2833

页数：12

共 11 条

[1] 安全协议的设计与逻辑分析 [J].

卿斯汉 .

软件学报, 2003, (07) :1300-1309

[2]

A framework for security analysis of mobile wireless networks[J] . Sebastian Nanz,Chris Hankin.Theoretical Computer Science . 2006 (1)

[3] The Seal Calculus [J].

Castagna, G ;

Vitek, J ;

Nardelli, FZ .

INFORMATION AND COMPUTATION, 2005, 201 (01) :1-54

[4]

Ariadne: A Secure On-Demand Routing Protocol for Ad Hoc Networks[J] . Yih-Chun Hu,Adrian Perrig,David B. Johnson.Wireless Networks . 2005 (1)

[5]

Type Inference for Mobile Ambients in Prolog[J] . Elio Giovannetti.Electronic Notes in Theoretical Computer Science . 2004

[6]

Towards a behavioural theory of access and mobility control in distributed systems[J] . Matthew Hennessy,Massimo Merro,Julian Rathke.Theoretical Computer Science . 2003 (3)

[7]

Typed Multiset Rewriting Specifications of Security Protocols[J] . Iliano Cervesato.Electronic Notes in Theoretical Computer Science . 2001

[8] Mobile ambients [J].

Cardelli, L ;

Gordon, AD .

THEORETICAL COMPUTER SCIENCE, 2000, 240 (01) :177-213

[9] Behavioral equivalence in the polymorphic pi-calculus [J].

Pierce, BC ;

Sangiorgi, D .

JOURNAL OF THE ACM, 2000, 47 (03) :531-584

[10] Secrecy by typing in security protocols [J].

Abadi, M .

JOURNAL OF THE ACM, 1999, 46 (05) :749-786

← 1 2 →