2.1 Model Description2.1.1 Model Assumptions6. AcknowledgementsCan Ad Hoc Routing Protocols be Shown Provably Secure? Todd R. Andel * Computer Science Department Florida State University Abstract. Formal security analysis of ad hoc routing protocols has historically been lacking, normally following non-formal inspection to identify flaws and attacks. This leads to a cycle of published development, attack, development, attack, … . Recent formal models and methods attempt to introduce rigor into the analysis ap-proach. We discuss flaws in a previously proposed security framework based on the simulatability model, commonly used in cryptographic proofs. We show how im-proper application and inappropriate assumptions lead to our discovery of an attack on both the endairA and ARAN protocols, which had been previously shown to be provably secure under this model. Instead of attempting to prove security of ad hoc routing protocols, we propose a framework for analyzing attacks and vulnerabilities. This alleviates the need for a common definition of routing security or the restriction of bounding the problem domain by unattainable assumptions. Keywords. MANETs, Provable Security, Secure Routing Protocols, Simulatability 1 Introduction In the late 1990's and early 2000's research into routing protocols for mobile ad hoc net-works (MANETs) primarily focused on functionality and efficient operation of wireless multi-hop networks. Royer and Toh [1] provide a survey which discusses many of the proposed protocols for this area. Security of these protocols, once an afterthought, is now being addressed as many pro-posed secure ad hoc routing protocols are being researched (see the survey by Hu and Perrig [2]). The majority of these secure protocols are based on the Dynamic Source Routing (DSR) [3] or the Ad Hoc On-Demand Distance Vector (AODV) [4] protocols. Unfortunately, the analysis of ad hoc routing protocol security features is typically infor-mal and tends to consistently result in a stamp of approval from the protocol developer, as they claim to show their protocol has met their definition of security. The effect is a false sense of security, and many of these "secure" protocols are later shown to have flaws. One reason for this is that there does not seem to be any standard definition of secure routing. Each author tends to define security within their own boundaries or as-sumptions to meet their needs. There have been recent attempts to develop formal analysis models to prove (or dis-prove) routing protocol security. Yang and Baras [5] focus on modeling insider attacks against Secure AODV (SAODV) [6] by adding extensions to the strand spaces [7] formal method and use of the Athena [8] model checker. Marshall [9] performed an analysis of * The views expressed in this article are those of the author and do not reflect the official policy or position of the United States Air Force, Department of Defense, or the U.S. Government. 1the Secure Routing Protocol (SRP) [10] using a formal method tool package called CPAL-ES [11]. We focus our analysis in this paper on the simulatability model proposed by Buttyán, Vajda, and Ács [12,13], based on classical proofs in cryptographic session key operations. This model is a valiant attempt to prove security properties, but falls short of its intended goal. Section 2 of this paper provides background on the simulatability model proposed by Buttyán, Vajda, and Ács. In Section 3 we discuss failures in this model and describe an attack on the endairA and ARAN protocols, which had been previously shown to be se-cure in the model of Section 2. In Section 4 we propose a framework as a basis for secu-rity comparison between MANET protocols. Section 5 lists our conclusions and future work. 2 Simulatability Model Background On-demand source routing protocols, such as DSR [3], depend on a route discovery proc-ess, allowing the source to identify an entire path to a given destination. This path is a significant security issue, in that if it is corrupted the ensuing data transmission attempt-ing to use the path will fail. Secure routing protocols attempt to deal with protection of these predetermined paths, however obscure attacks usually render such protocols inse-cure after they have been published. Buttyán and Vajda [12] contend these undiscovered flaws primarily result from the lack of a common definition of secure routing, and that there is not a formal or mathematical process to analyze such routing protocols for secu-rity flaws. The formal model they propose attempts to "…make the first steps towards a formal model in which one can precisely define what secure routing means and prove (or fail to prove) that a given protocol indeed satisfies that definition." [12] 2.1 Model Description Their proposed model [12] follows a common simulatability technique historically used to analyze cryptographic proof systems. The model consists of two separate yet nearly identical models referred to as a real-world model and an ideal-world model. Both mod-els consist of basic Turing machine components to simulate an on-demand source routing protocol for an instance in time (i.e. mobility is not accounted for). The composition of the ad hoc network is represented by the undirected graph G = (V, E, L), where V is the set of nodes, E is the set of edges, and L is a labeling function which assigns each node a unique identifier (e.g. node A will typically be identified by the label A). For each node v ∈ V, the neighborhood determines which nodes are within transmis-sion distance of the sender and is formally defined as NG(v) = {v' : (v, v') ∈ E}. The con-figuration, formally defined as conf = (G, v~), represents the location of the adversarial node . The work in [13] extends the model to allow multiple, possibly colluding, ad-versarial nodes. v~Figure 1, based on [13], depicts the various Turing machines used to simulate the given protocol. Machine H models the upper protocol layers, initiates routing requests, and collects identified routes. Machines M1 to Mn model the operation of the non-corrupted nodes according to the given protocol. Machine C models the communication 2channels by taking the output of each node and delivering it to the respective neighbors as defined by NG(v). Machines A1 – Am describes the adversarial nodes. The adversaries have the same capabilities as non-corrupted nodes, but are not required to follow the rout-ing protocol.