Degree Type

Thesis

Date of Award

2008

Degree Name

Master of Science

Department

Computer Science

First Advisor

Hridesh Rajan

Abstract

Verifying sensor network security protocol implementations using testing/simulation might leave some flaws undetected. Formal verification techniques have been very successful in detecting faults in security protocol specifications; however, they generally require building a formal description (model) of the protocol. Building accurate models is hard, thus hindering the application of formal verification. In this work, a framework for automating formal verification of sensor network security protocols is presented. The framework Slede extracts models from protocol implementations and verifies them against generated intruder models. Slede was evaluated by verifying two sensor network security protocol implementations. Security flaws in both protocols were detected.

Copyright Owner

Youssef Wasfy Hanna

Language

en

Date Available

2012-04-30

File Format

application/pdf

File Size

52 pages

Share

COinS