Verifying sensor network security protocol implementations

By: Youssef Hanna

Download Paper

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.

ACM Reference

Hanna, Y. 2008. Verifying sensor network security protocol implementations. Iowa State University.

BibTeX Reference

@mastersthesis{hanna2008verifying,
  title = {Verifying sensor network security protocol implementations},
  author = {Hanna, Youssef},
  year = {2008},
  school = {Iowa State University},
  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.
  }
}