|
Dissertation Title: Formal Security Evaluation of Ad Hoc Routing Protocols (pdf)
Dissertation Overview:
This dissertation discusses current techniques used to evaluate security properties in Mobile Ad Hoc Networks (MANETs). We develop a novel technique to provide exhaustive state analysis for a given scenario which provides automation into the security analysis process using the SPIN model checker and developing exhaustive topology generation, analysis, and reporting routines.
The model files are accessible below: |
|
SPIN Model Files
The following SPIN files are designed to evaluate 5-node network.
Protocol: Dynamic Source Routing (DSR)
Filename: dsr_in_5node.pml
Description: Working DSR 5-node model
Protocol: Secure Routing Protocol (SRP)
Filename: srp_nda-rreq_5node.pml
Description: Model file used to detect a successful node drop attack against SRP rreq. Target will sign corrupted route.
Protocol: Ariadne
Filename: ari_nda-rreq_5node.pml
Description: Attacker stores messages to break per-hop forward hash. Malicious insider can break by dropping a node from the path (NDA)
Protocol: Ariadne
Filename: ari_inda-rreq_5node.pml
Description: Attacker stores messages to break per-hop forward hash. Malicious outsider can break by dropping a node from the path (INDA)
Protocol: endairA
Filename: end_nda-2_5nodel.pml
Description: Attacker uses knowledge of colluding attacker's key to drop intermediate nodes during rreq and provide the correct signatures during rrep.
Automated Topology Generation and Analysis Files (Perl)
The following PERL files are designed to work with a 5-node network.
Filename: AnalyzeProtocol-5node.pl
Description: This file analyzes MANET routing protocols for route discovery integrity. The file reads a base SPIN Promela file (.pml) file model for a source routing protocol. The base SPIN file contains a fully disconnected network (all links set to 0). The file is then sent through three process engines below (all these can be run individually if desired).
Filename: GenSpinTopo-5node.pl
Description: Generates all possible topologies for N=5. A unique Promela file is produced for each topology case.
Filename: EvalEng.pl
Description: Compiles and executes each Promela case file. Cases encountering assertion failures (i.e., successful attacks) generate a .trial file.
Filename: ReptEng-5node.pl
Description: Reads the .trail files and associated .pml files. The initiator, target, corrupted path, and current topology are extracted and reported to file.