Verifying Security Protocols for Sensor Networks Using Algebraic Specification Techniques

  • Iakovos Ouranos
  • Petros Stefaneas
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4728)


Algebraic specification languages are formal methods that provide a rigorous basis for modeling of several systems. Security protocols are safety critical systems that need to be verified before their implementation. In this paper we have formally specified sensor network encryption protocol (SNEP) and a key agreement protocol for sensor networks, both from the SPINS protocol suite, with the OTS/CafeOBJ method, a well known formal specification technique applied not only in research, but also in industry. Based on this specification, we have proved that each protocol possesses an important safety(invariant) property.


Algebraic Specification and Verification CafeOBJ Sensor Networks Observational Transition Systems SPINS Protocol suite 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bjørner, D.: Logics of Formal Specification Languages - The Possible Worlds cum Domain Problem. In: Proceedings of 4th Panhellenic Symposium on Logic (2003)Google Scholar
  2. 2.
    Ogata, K., Futatsugi, K.: Proof Scores in the OTS/CafeOBJ Method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)Google Scholar
  3. 3.
    Ogata, K., Futatsugi, K.: Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 596–615. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Diaconescu, R., Futatsugi, K.: CafeOBJ Report. World Scientific, Singapore (1998)Google Scholar
  5. 5.
    Perrig, A., Szewczyk, R., Wen, V., Culler, D., Tygar, J.D.: SPINS: Security Protocols for Sensor Networks. In: Proceedings of MOBICOM 2001, pp. 189–199 (2001)Google Scholar
  6. 6.
    Goguen, J., Malcolm, G.: A hidden agenda. Technical Report CS97-538, University of California at San Diego (1997)Google Scholar
  7. 7.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inform. Theory IT-29, 198–208 (1983)Google Scholar
  8. 8.
    Ogata, K., Futatsugi, K.: Rewriting - based verification of authentication protocols. In: WRLA 2002. ENTCS, vol. 71 (2002)Google Scholar
  9. 9.
    Ogata, K., Futatsugi, K.: Modeling and Verification of Real-Time Systems Based on Equations. Science of computer programming 66(2), 162–180 (2007)Google Scholar
  10. 10.
    Diaconescu, R., Futatsugi, K., Ogata, K.: CafeOBJ: Logical Foundations and Methodologies. Computing and Informatics 22, 1001–1025 (2003)Google Scholar
  11. 11.
    Ogata, K., Futatsugi, K.: Formal analysis of Suzuki and Kasami distributed mutual exclusion algorithm. In: FMOODS 2002, pp. 181–195 (2002)Google Scholar
  12. 12.
    Seino, T., Ogata, K., Futatsugi, K.: Specification and Verification of a Single-Track Railroad Signaling in CafeOBJ. IEICE Trans. Fundamentals E84-A(6), 1471–1478 (2001)Google Scholar
  13. 13.
    Xiang, J., Kong, W., Futatsugi, K., Ogata, K.: Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management. In: WEBIST 2006 (2006)Google Scholar
  14. 14.
    Ouranos, I. Stefaneas, P., Frangos, P.: A Formal Specification Framework for ad hoc mobile communication networks. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Plášil, F., Bielikova, M. (eds.) SOFSEM 2007, vol. 2, pp. 91–102, Institute of Computer Science AS CR, Prague (2007) ISBN 80-903298-9-6 Google Scholar
  15. 15.
    Ouranos, I., Stefaneas, P., Frangos, P.: An Algebraic Framework for Modeling of Mobile Systems. IEICE Trans. Fundamentals E90-A(9) (to appear, 2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Iakovos Ouranos
    • 1
  • Petros Stefaneas
    • 2
  1. 1.School of Electrical and Computer Engineering 
  2. 2.School of Applied Mathematical and Physical Sciences, National Technical University of Athens 

Personalised recommendations