Abstract
In this paper we verify the security aspects of a cross-layer, application-oriented communication protocol for Wireless Sensor Networks (WSN). The Trustful Space-Time Protocol (TSTP) encompasses a majority of features recurrently needed by WSN applications like medium access control, geographic routing, location estimation, precise time synchronization, secure communication channels and a key distribution scheme between sensors and the sink. Key distribution in TSTP happens after deployment via time-based session keys. The key distribution scheme relies on public cryptography primitives and synchronous clocks as shared data between the parties. We analyzed TSTP’s key distribution protocol using ProVerif and we were able to find two security flaws: one related to the time synchronization component and another being a bad approach related to a mac-then-encrypt method employed. With our findings we propose an improved version of the key distribution protocol, where we change the message authentication scheme in the initial message exchange so that ProVerif’s goals are fulfilled; we also introduce the encrypt-then-mac method so that secret information passing through the communication channel has integrity and does not fall to known attacks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
References
Atzori, L., Iera, A., Morabito, G.: The internet of things: a survey. Comput. Netw. 54(15), 2787–2805 (2010)
Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. J. Cryptology 21(4), 469–491 (2008)
Bernstein, D.J.: The poly1305-aes message-authentication code. In: Proceedings of Fast Software Encryption, Paris, France, pp. 32–49, February 2005
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 331–340. IEEE (2005)
Blanchet, B., Cheval, V., Allamigeon, X., Smyth, B.: Proverif: Cryptographic protocol verifier in the formal model (2010)
Blanchet, B., Smyth, B., Cheval, V.: Proverif 1.90: Automatic cryptographic protocol verifier, user manual and tutorial (2015). http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf
CERP-IoT, V.: Challenges for realising the internet of things, no. March. European Commission-Information Society and Media DG (2010)
Claycomb, W.R., Shin, D.: A novel node level security policy framework for wireless sensor networks. J. Netw. Comput. Appl. 34(1), 418–428 (2011)
Delgado-Mohatar, O., Fúster-Sabater, A., Sierra, J.M.: A light-weight authentication scheme for wireless sensor networks. Ad Hoc Netw. 9(5), 727–735 (2011)
Faquih, A., Kadam, P., Saquib, Z.: Cryptographic techniques for wireless sensor networks: A survey. In: 2015 IEEE Bombay Section Symposium (IBSS), pp. 1–6. IEEE (2015)
Fu, B., Xiao, Y., Deng, H.J., Zeng, H.: A survey of cross-layer designs in wireless networks. IEEE Commun. Surv. Tutorials 16(1), 110–126 (2014)
Gubbi, J., Buyya, R., Marusic, S., Palaniswami, M.: Internet of things (iot): a vision, architectural elements, and future directions. Future Gener. Comput. Syst. 29(7), 1645–1660 (2013)
Kiruthika, B., Ezhilarasie, R., Umamakeswari, A.: Implementation of modified rc4 algorithm for wireless sensor networks on cc2431. Indian J. Sci. Technol. 8(S9), 198–206 (2015)
Mendes, L.D., Rodrigues, J.J.: A survey on cross-layer solutions for wireless sensor networks. J. Netw. Comput. Appl. 34(2), 523–534 (2011)
Yau, A.K.L., Paterson, K.G., Mitchell, C.J.: Padding oracle attacks on CBC-mode encryption with secret and random IVs. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557, pp. 299–319. Springer, Heidelberg (2005). doi:10.1007/11502760_20
Rajeswari, S.R., Seenivasagam, V.: Comparative study on various authentication protocols in wireless sensor networks. Sci. World J. 2016, 16 (2016)
Reghelin, R., Fröhlich, A.A.: A decentralized location system for sensor networks using cooperative calibration and heuristics. In: Proceedings of the 9th ACM International Symposium on Modeling Analysis and Simulation of Wireless and Mobile Systems, pp. 139–146. ACM (2006)
Ren, K., Yu, S., Lou, W., Zhang, Y.: Multi-user broadcast authentication in wireless sensor networks. IEEE Trans. Veh. Technol. 58(8), 4554–4564 (2009)
Resner, D., Frohlich, A.A.: Design rationale of a cross-layer, trustful space-time protocol for wireless sensor networks. In: 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA), pp. 1–8. IEEE (2015)
Resner, D., Fröhlich, A.A.: Key establishment and trustful communication for the internet of things. In: 4th SENSORNETS (2015)
Resner, D., Fröhlich, A.A., Wanner, L.F.: Speculative Precision Time Protocol: submicrosecond clock synchronization for the IoT. In: 21th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2016), Berlin, Germany (August 2016, To appear)
Suo, H., Wan, J., Zou, C., Liu, J.: Security in the internet of things: a review. In: 2012 International Conference on Computer Science and Electronics Engineering (ICCSEE), vol. 3, pp. 648–651. IEEE (2012)
Vijayakumar, P., Vijayalakshmi, V.: Effective key establishment and authentication protocol for wireless sensor networks using elliptic curve cryptography. In: Proceedings of the Conference on Mobile and Pervasive Computing (CoMPC08) (2008)
Wander, A.S., Gura, N., Eberle, H., Gupta, V., Shantz, S.C.: Energy analysis of public-key cryptography for wireless sensor networks. In: Third IEEE International Conference on Pervasive Computing and Communications, pp. 324–328. IEEE (2005)
Wang, Y., Attebury, G., Ramamurthy, B.: A survey of security issues in wireless sensor networks. IEEE Commun. Surv. Tutorials 8(2), 2–23 (2006)
Wong, K.H., Zheng, Y., Cao, J., Wang, S.: A dynamic user authentication scheme for wireless sensor networks. In: IEEE International Conference on Sensor Networks, Ubiquitous, and Trustworthy Computing (SUTC 2006), vol. 1, pp. 8–pp. IEEE (2006)
Zhao, K., Ge, L.: A survey on the internet of things security. In: 2013 9th International Conference on Computational Intelligence and Security (CIS), pp. 663–667. IEEE (2013)
Zhu, S., Setia, S., Jajodia, S.: Leap+: Efficient security mechanisms for large-scale distributed sensor networks. ACM Trans. Sensor Netw. (TOSN) 2(4), 500–528 (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Silva, D.S., Resner, D., de Souza, R.L., Martina, J.E. (2016). Formal Verification of a Cross-Layer, Trustful Space-Time Protocol for Wireless Sensor Networks. In: Ray, I., Gaur, M., Conti, M., Sanghi, D., Kamakoti, V. (eds) Information Systems Security. ICISS 2016. Lecture Notes in Computer Science(), vol 10063. Springer, Cham. https://doi.org/10.1007/978-3-319-49806-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-49806-5_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-49805-8
Online ISBN: 978-3-319-49806-5
eBook Packages: Computer ScienceComputer Science (R0)