Abstract:Based on the characteristics of ad hoc security routing protocols (SRPs), the advantages anddisadvantages of the strand space theory are analyzed. An analysis model for protocol attacks, which leads to anonexistent route that is accepted by the protocol, is designed on the basis of the strand space model. Finally, thispaper demonstrates the usefulness of this model in the case of a security ad hoc routing protocol: Extended SRP.

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 message set of protocol.