Abstract
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.
Work partially supported by MURST Project ”Metodi Formali per la Sicurezza ed il Tempo” (MEFISTO); by MIUR project COVER; by IST-FET project ”Design Environments for Global ApplicationS (DEGAS)”; by CNR project ”Tecniche e Strumenti Software per l’Analisi della Sicurezza delle Comunicazioni in Applicazioni Telematiche di Interesse Economico e Sociale” and by a CSP grant for the project ”SeTAPS II”.
Chapter PDF
Similar content being viewed by others
References
Aldini, A., Bravetti, M., Gorrieri, R.: A Process-algebraic Approach for the Analysis of Probabilistic Non-interference. Journal of Computer Security (2003)
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)
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)
Focardi, R., Gorrieri, R., Martinelli, F.: Real-Time Information Flow Analysis. IEEE JSAC 21(1) (2003)
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)
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)
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)
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)
Hennessy, M., Regan, T.: A Temporal Process Algebra. I&C 117, 222–239 (1995)
Law, Y.W., Dulman, S., Etalle, S., Havinga, P.: Assessing Security in Energyefficient Sensor Networks. In: Proc. of Small Systems Security Workshop 2003 (2003)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
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)
Perrig, A., Szewczyk, R., Tygar, J.D., Wen, V., Culler, D.: SPINS: Security Protocols for Sensor Networks. Wireless Networks Journal 8, 521–534 (2002)
Romer, K.: Time Synchronization in Ad Hoc Networks. In: Proc. of ACM Mobi-Hoc 2001, pp. 173–182 (2001)
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)
Shankar, N., Owre, S., Rushby, J.M.: PVS Tutorial. Tutorial Notes, FME 1993: Industrial-Strength Formal Methods, pp. 357–406 (April 1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Gorrieri, R., Martinelli, F., Petrocchi, M., Vaccarelli, A. (2003). Formal Analysis of Some Timed Security Properties in Wireless Protocols. In: Najm, E., Nestmann, U., Stevens, P. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2003. Lecture Notes in Computer Science, vol 2884. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39958-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-39958-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20491-6
Online ISBN: 978-3-540-39958-2
eBook Packages: Springer Book Archive