Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols Hanna, Youssef Rajan, Hridesh Rajan, Hridesh Wensheng, Zhang
dc.contributor.department Computer Science 2018-02-14T00:01:52.000 2020-06-30T01:56:08Z 2020-06-30T01:56:08Z 2006-11-14
dc.description.abstract <p>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.</p>
dc.identifier archive/
dc.identifier.articleid 1268
dc.identifier.contextkey 5474080
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/250
dc.source.bitstream archive/|||Fri Jan 14 22:56:59 UTC 2022
dc.subject.disciplines Programming Languages and Compilers
dc.subject.disciplines Theory and Algorithms
dc.title Lightweight Specification Language and Verification Framework for Sensor Network Security Protocols
dc.type article
dc.type.genre article
dspace.entity.type Publication
relation.isAuthorOfPublication 4e3f4631-9a99-4a4d-ab81-491621e94031
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
Original bundle
Now showing 1 - 1 of 1
228.54 KB
Adobe Portable Document Format