Formal Analysis of Some Timed Security Properties in Wireless Protocols

  • Roberto Gorrieri
  • Fabio Martinelli
  • Marinella Petrocchi
  • Anna Vaccarelli
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2884)


We show how a recent language for the description of cryptographic protocols in a real time setting may be suitable to formally verify security aspects of wireless protocols. We define also a compositional proof rule for establishing security properties of such protocols. The effectiveness of our approach is shown by defining and studying the timed integrity property for μTESLA, a well-known protocol for wireless sensor networks. We are able to deal with protocol specifications with an arbitrary number of agents (senders as well as receivers) running the protocol.


Security Wireless Communication Formal Analysis Sensor Networks 


  1. 1.
    Aldini, A., Bravetti, M., Gorrieri, R.: A Process-algebraic Approach for the Analysis of Probabilistic Non-interference. Journal of Computer Security (2003)Google Scholar
  2. 2.
    Broadfoot, P., Lowe, G.: Analysing a Stream Authentication Protocol using Model Checking. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol. 2502, pp. 146–161. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Focardi, R., Gorrieri, R., Martinelli, F.: Non Interference for the Analysis of Cryptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 354–372. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Focardi, R., Gorrieri, R., Martinelli, F.: Real-Time Information Flow Analysis. IEEE JSAC 21(1) (2003)Google Scholar
  5. 5.
    Focardi, R., Martinelli, F.: A uniform approach for the definition of security properties. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 794–813. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Gorrieri, R., Locatelli, E., Martinelli, F.: A Simple Language for Real-time Cryptographic Protocol Analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 114–128. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Gorrieri, R., Martinelli, F.: Process Algebraic Frameworks for the Specification and Analysis of Cryptographic Protocols. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 46–67. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Gorrieri, R., Martinelli, F., Petrocchi, M., Vaccarelli, A.: Compositional Verification of Integrity for Digital Stream Signature Protocols. In: Proc. of IEEE ACSD 2003, pp. 142–149 (2003)Google Scholar
  9. 9.
    Hennessy, M., Regan, T.: A Temporal Process Algebra. I&C 117, 222–239 (1995)zbMATHGoogle Scholar
  10. 10.
    Law, Y.W., Dulman, S., Etalle, S., Havinga, P.: Assessing Security in Energyefficient Sensor Networks. In: Proc. of Small Systems Security Workshop 2003 (2003)Google Scholar
  11. 11.
    Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  12. 12.
    Perrig, A., Canetti, R., Song, D.X., Tygar, D.: Efficient and Secure Source Authentication for Multicast. In: Proc. of NDSS 2001. The Internet Society, San Diego (2001)Google Scholar
  13. 13.
    Perrig, A., Szewczyk, R., Tygar, J.D., Wen, V., Culler, D.: SPINS: Security Protocols for Sensor Networks. Wireless Networks Journal 8, 521–534 (2002)CrossRefzbMATHGoogle Scholar
  14. 14.
    Romer, K.: Time Synchronization in Ad Hoc Networks. In: Proc. of ACM Mobi-Hoc 2001, pp. 173–182 (2001)Google Scholar
  15. 15.
    Schneider, S.: Analysing Time-Dependent Security Properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895. Springer, Heidelberg (2000)Google Scholar
  16. 16.
    Shankar, N., Owre, S., Rushby, J.M.: PVS Tutorial. Tutorial Notes, FME 1993: Industrial-Strength Formal Methods, pp. 357–406 (April 1993)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Roberto Gorrieri
    • 1
  • Fabio Martinelli
    • 2
  • Marinella Petrocchi
    • 2
  • Anna Vaccarelli
    • 2
  1. 1.Dipartimento di Scienze dell’InformazioneUniversità di BolognaItaly
  2. 2.Istituto di Informatica e TelematicaC.N.R.Italy

Personalised recommendations