skip to main content

Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols

Hanna, Youssef Wasfy ; Rajan, Hridesh ; Wensheng, Zhang

Digital Repository @ Iowa State University 2006

Texto completo disponível

Citações Citado por
  • Título:
    Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols
  • Autor: Hanna, Youssef Wasfy ; Rajan, Hridesh ; Wensheng, Zhang
  • Assuntos: Programming Languages And Compilers ; Theory And Algorithms
  • Descrição: The contribution of this work is an approach for lightweight specification and verification of nesC implementations of sensor networks security protocols. Our approach provides annotations to specify objectives, network topology, intruder models, and channel fault models. The objectives of the protocols can be specified in terms of user-defined events, which is significantly more expressive compared to earlier approaches such as CAPSL that provide a fixed set of objectives. Moreover, our approach is extensible in that it allows new intruder and channel fault models to be added to the verification process. These models are themselves written in nesC. To show the feasibility of our approach, we describe the implementation of our verification framework. Our verification framework uses the model checker SPIN as the underlying technology. Our approach was able to detect earlier known bugs in protocols and an assumption violation in the protocol implementation.
  • Editor: Digital Repository @ Iowa State University
  • Data de publicação: 2006

Buscando em bases de dados remotas. Favor aguardar.