SLEDE: event-based specification of sensor network security protocols

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.

REFERENCES

• 1: G. Denker and J. Millen. CAPSL integrated protocol environment. In DARPA Information and Survivability Conference and Exposition (DISCEX'00), pages 207--221, Hilton Head, South Carolina, Jan 2000.
• 2: D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(12):198--208, mar 1983.
• 3: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 4: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 5: Jonathan K. Millen, CAPSL: Common Authentication Protocol Specification Language, Proceedings of the 1996 workshop on New security paradigms, p.132, September 17-20, 1996, Lake Arrowhead, California, United States [doi>10.1145/304851.304879]
• 6: Adrian Perrig , Robert Szewczyk , Victor Wen , David Culler , J. D. Tygar, SPINS: security protocols for sensor netowrks, Proceedings of the 7th annual international conference on Mobile computing and networking, p.189-199, July 2001, Rome, Italy [doi>10.1145/381677.381696]