Formal Verification of a Cross-Layer, Trustful Space-Time Protocol for Wireless Sensor Networks

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.