This thesis presents a number methodologies for computer assisted vulnerability analysis of routing protocols in ad-hoc networks towards the goal of automating the process of finding vulnerabilities (possible attacks) on such network routing protocols and correcting the protocols. The methodologies developed are (each) based on a different representation (model) of the routing protocol, which model predicated the quantitative methods and algorithms used. Each methodology is evaluated with respect to effectiveness …
Author: Yang, Shah-an
Source: University of Maryland
Download Link: Click Here To Download This Report (PDF)
Reference URL 1: Visit Now
Reference URL 2: Visit Now
Contents
1 Introduction
1.1 Outline
1.2 Vulnerability Analysis of Ad-Hoc Routing Protocols : An Overview
1.3 Main Contributions of this Dissertation
1.4 Dissertation Outline
2 A Formal Model for Ad Hoc Routing Protocol Vulnerability Analysis
2.1 Introduction
2.2 Background
2.2.1 Verification of Ad Hoc Routing Protocols
2.2.2 Secure Ad Hoc Routing Protocols
2.2.3 Securing Fixed Routing Protocols
2.2.4 Formal Methods
2.3 Criteria for Secure Routing
2.4 Proposed extended strands model
2.4.1 Partial Order Semantics and CTL
2.4.2 Messages and events
2.4.3 Role
2.4.3.1 Logical Theories for Φ
2.4.4 Protocols
2.4.5 Strands
2.4.6 Goal bindings
2.4.7 Causal relations
2.4.8 Constraint Program
2.4.9 Semibundles
2.4.10 Bundles
2.4.11 Topologies
2.4.12 Constraint program feasibility
2.4.13 Algorithm for checking feasibility
2.5 Search procedure
2.5.1 Protocol specification language
2.6 Implementation
2.7 Results
2.8 Discussion
3 Probabilistic-Timed Formal Model
3.1 Introduction
3.1.1 Related Work
3.2 Review of OLSR
3.2.1 Components of OLSR
3.2.1.1 Local Topology Maintenance
3.2.1.2 Information Dissemination
3.3 Protocol Specification by Extended Executable Model
3.3.1 Basic Formal Model
3.3.2 Formal Timing Analysis
3.3.3 Probabilistic Timing Analysis
3.3.3.1 Preliminaries
3.3.3.2 Deriving the Timing Model from the Formal Model
3.3.3.3 Volume Computation
3.3.3.4 Adapting Lasserre’s Algorithm to Temporal Structure
3.3.3.5 Coupling Monte-Carlo Integration with Exact Com-putation
3.4 Discussion
4 Trace-Based Model within an Optimization Framework : OLSR Example
4.1 Introduction
4.2 New Security Requirement
4.2.1 Policy Iteration Formulation
4.2.1.1 Cross-Entropy Optimization
4.2.1.2 Multi-Layer Perceptrons
4.3 Initial Experiments
4.3.1 Experiment 1
4.3.2 Experiment 2
4.3.3 Experiment 3
4.4 Discussion
5 Discussion and Future Work
Bibliography