Flaws in security protocols are subtle and hard to find. Finding flaws in the security protocols for sensor networks is even harder because they operate under fundamentally different system design assumptions such as event-driven vs. imperative or message passing, resource and bandwidth constraints, hostile deployment scenarios, trivial physical capturing due to the lack of temper resistance, group-oriented behavior, ad hoc and dynamic topologies, open-ended nature, etc. These assumptions lead to complex security protocols, which in turn makes them much harder to verify. The award from the National Science Foundation to the PI: Hridesh Rajan and the Co-PI: Wensheng Zhang provides support for research aimed at developing novel specification and verification techniques for security protocols in sensor networks. Sensor networks are increasingly becoming an integral part of the nation's cyber infrastructure, making it vital to protect them against cryptographic errors in security protocols. There are several existing techniques for specifying and verifying cryptographic protocols; however, none accommodates all the system design assumptions mentioned above. This research is advancing the state of the art in specification and verification of cryptographic protocols for sensor networks. Applications of sensor networks are numerous from military to environmental research. By providing mechanisms to find cryptographic errors in the security protocols for sensor networks this research program is improving the reliability of these networks, making a direct impact on all areas where these networks are utilized. More information about this project is available here. This is an ongoing project in the Laboratory for Software Design.