SLEDE: event-based specification of sensor network security protocols

By: Youssef Hanna and Hridesh Rajan

Download Paper

Abstract

The semantic gap between specification and implementation languages for sensor networks security protocols impedes the specification and verification of the protocols. In this work, we present SLEDE, an event-based specification language and its verifying compiler that address this semantic gap. We demonstrate the features of SLEDE through an example specification of the μTesla, secure broadcast protocol for sensor networks.

ACM Reference

Hanna, Y. and Rajan, H. 2006. SLEDE: event-based specification of sensor network security protocols. SIGSOFT Softw. Eng. Notes. 31, 6 (2006), 1–2. DOI:https://doi.org/http://doi.acm.org/10.1145/1218776.1218801.

BibTeX Reference

@article{hanna2006slede,
  author = {Youssef Hanna and Hridesh Rajan},
  title = {SLEDE: event-based specification of sensor network security protocols},
  journal = {SIGSOFT Softw. Eng. Notes},
  volume = {31},
  number = {6},
  year = {2006},
  issn = {0163-5948},
  pages = {1--2},
  doi = {http://doi.acm.org/10.1145/1218776.1218801},
  publisher = {ACM},
  address = {New York, NY, USA},
  entrysubtype = {other},
  abstract = {
    The semantic gap between specification and implementation languages for sensor
    networks security protocols impedes the specification and verification of the
    protocols. In this work, we present SLEDE, an event-based specification
    language and its verifying compiler that address this semantic gap. We
    demonstrate the features of SLEDE through an example specification of the
    μTesla, secure broadcast protocol for sensor networks.
  }
}