利用类型推理验证Ad_Hoc安全路由协议.pdfVIP

ISSN 1000-9825, CODEN RUXUEW E-mail: jos@ Journal of Software , Vol.20, No.10, October 2009, pp.2822−2833 doi: 10.3724/SP.J.1001.2009.03504 Tel/Fax: +86-10 © by Institute of Software , the Chinese Academy of Sciences . All rights reserved. ∗ 利用类型推理验证 Ad Hoc 安全路由协议 1,2 1,2+ 李 沁 , 曾庆凯 1(南京大学 计算机软件新技术国家重点实验室,江苏 南京 210093) 2(南京大学 计算机科学与技术系,江苏 南京 210093) Verifying Mobile Ad-Hoc Security Routing Protocols with Type Inference LI Qin1,2, ZENG Qing-Kai1,2+ 1(State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China) 2(Department of Computer Science and Technology, Nanjing University, Nanjing 210093, China) + Corresponding author: E-mail: zqk@ Li Q, Zeng QK. Verifying mobile ad-hoc security routing protocols with type inference. Journal of Software, 2009,20(10):2822−2833. /1000-9825/3504.htm Abstract : A type-inference-based formal method is proposed for verifying an ad-hoc security routing protocol in this paper. A calculus, called NCCC (neighborhood-constraint communication calculus), is defined to specify the protocol. The security property of the protocol is described with typing rules in a type system. Based on the Dolev-Yao model, an attacker model, called the message set of protocol format, is refined. At last, the simplified version of SAODV (secure ad hoc on-demand routing protocol) is verified with this method. With the type- inference-based formal method, not only is the security of protocols verified, but also the attacke examples are predicted. The complexity of inference is reduced significantly for refining the me