Research On Key Technologies Of Design And Analysis Of Secure Routing In Mobile Ad Hoc Networks

Mobile ad hoc networks (MANETs) are collections of wireless mobile devices withrestricted broadcast range and resources, are multi-hop wireless network without fixedinfrastructure. These networks are decentralized, with nodes acting both as hosts androuters, forwarding packets for nodes that not in transmission range of each other.Secure routing can obtain information of trusted routing only depend on incorporatingbetween honest nodes. Implement of this “dependence” need to resort to somecryptographic primitives to establish integrity authentication of routing informationand to provide entity authentication between honest nodes. However, difference withsecurity analysis of cryptographic protocol, we must consider behavior of networkintermediate nodes that form routing. Therefore, formal analysis technologies forsecure protocol can’t be directly used for security verification of routing. We mustdevelop new formal approaches of security analysis of routing for mobile ad hocnetworks.Two families of popular models have been designed for the rigorous analysis ofsecurity protocols: the so-called symbolic models (Dolev-Yao, formal) on the one handand the computational (cryptographic, concrete) models on the other hand. In thisdissertation, aim at the particularity of routing security analysis for mobile ad hocnetworks, we study theories and approaches of routing security analysis in UC(Universally Composable) model that is a computational model of security analysis ofcryptographic protocols and PCL (Protocol Composable Logic) that is a symbolanalysis model. The main results presented are as follows:1.Correct representation of security threat model of routing is basis of securityanalysis of routing. In this dissertation, we firstly analysis issues of existingsecurity threat model, such as active-n-m attacker model, the parametric attackermodel and the adaptive attacker model. Based on existing security threat model ofrouting and Dolev-Yao threat model, we propose a new threat model-thehierarchical threat model.2. UC-RP (UC for Routing Protocol) model based on UC theory is latest approachof routing security analysis. In this dissertation, aim at analysis issue ofdevelopment and analysis of multi-paths distance vector routing, the concept oftrusted system state is proposed. Trusted system state is security requirement of multi-paths distance vector routing. The ideal functionality is given and securitydefinition is proposed. We further complete and improve UC-RP model.3.PCL is a symbol model for reasoning about security properties for cryptographicprotocols such as authentication protocols and key agreement protocols etc. Inthis dissertation, we extend PCL and propose a PCL-RP (PCL for RoutingProtocol) model to model mobile ad hoc networks and analysis security of routing.In PCL-RP, the concepts of location and neighboring location of thread areintroduced. The dynamic topology of multi-hop wireless networks was describedby the set of neighbors for threads. The broadcast rule of neighboring locationthreads models the feature of wireless broadcast communication. Symbol traceproposed models execution process of routing and network trace proposed in thisdissertation models network evolution that resulted from events on symbol trace.The semantics of predicates and modal formula are defined and security ofrouting is analyzed on network trace.4.Symbolic analysis of PCL-RP is dramatically simpler than full-fledgecryptographic analysis of UC-RP. In particular, it is readily amenable toautomation. However, symbolic analysis does not a priori carry anycomputational soundness guarantees. Following recent work on computationalsound symbolic analysis, we propose UCSA-RP (Universally ComposableSymbol Analysis for Routing Protocol) by reconciling UC-RP and PCL-RP. Wedemonstrate how symbol analysis of PCL-RP can be used to assert the security ofrouting within UC-RP.5.The algorithm of AMR (Aggregate Multi-paths Routing) is a routing mechanismthat computes the maximal set of node-disjoint paths. In this dissertation,integrating the algorithm of AMR and AODV, we develop multiple node-disjointpaths secure distance vector routing (SMDVR), and security of SMDVR isanalyzed in UC-RP. It is proved that the security of SMDVR can be reduced tothe security of the digital signature.6.In this dissertation, we firstly study issues in DCAR (Distributed coding-AwareRouting) and propose a new security destination that is fit for coding-awaresecure routing. And then, based on DCAR, we develop a secure routing DCASR(Distributed Coding-Aware Secure Routing). We model DCASR and analysissecurity properties in PCL-RP. It is proved that DCASR can satisfy our securitydestination. In UCSA-RP, We show that DCASR satisfies symbolic securitycriterion in PCL-RP if and only if the corresponding cryptographic protocol is secure in UC-RP.