## 6 Related Work  
Since the development of the SNEP protocol, a number of security analyses has been carried out. There are two popular methods of formal modeling and verification of security protocols: through an automated tool and algebraic specification techniques. Both methods have been applied in validating SNEP's security properties. In [17], an AVISPA model has been developed to verify two security properties: authenticity and confidentiality of SNEP message components. Two separate models have been developed to verify the scenarios: requesting information from the base station to a normal node and key distribution between two nodes. In this analysis, an attack has been found, where an intruder masquerading in the role of the base station requests information from a node. It has been claimed that exploiting this attack, the intruder may receive confidential data from a node. However, this claim is not justified, since a node sends data to the base station in encrypted format (note that the node to base station data transmission protocol is explained in Section 2.2), and the intruder is not able to divulge the encryption key. The models we are presenting in this paper are different from the models explained in [17] in many ways that are explained here:  
1. We develop the model of the counter exchange protocol with strong freshness, which they did not. 2. They develop a node to node key distribution followed by data transmission (in total, six messages are being exchanged), while we develop an integrated model (in total, five messages are being exchanged). 3. Finally, the attack we discovered was not reported by the previous model. A popular, open-source software verification tool, Spin [18], has been used to verify the confidentiality and authentication of SNEP [19]. In this study, a fine-state machine-based model for SNEP has been developed first. Next, the security properties (_i.e._, authenticity and confidentiality) have been expressed using the linear temporal logic (LTL). Finally, these properties have been verified using Spin. Note that the model checking tool (_i.e._, Spin) they have used is not particularly developed for security property validation. Thus, the focus of this paper is to show how Spin could be used in security property validation. Here, only the key distribution protocol SNEP has been modeled. As we mentioned earlier, modal logic and algebraic specification techniques have been used to validate the security properties of a protocol. Here, we present two such efforts ([20,21]), where instead  
Figure 16: Proposed modification to prevent a DoS attack. of automated tools, the security properties of SNEP have been validated using a mathematical proof. In [20], the Coffey-Saidha-Newe (CSN) modal logic has been used to verify the SNEP key agreement sub-protocol. CSN [22] combines the logic of belief and knowledge during execution of a protocol and, thus, is capable of verifying both security and trust. The analysis has not found any weakness of the key agreement protocol and also has confirmed the property's strong security due to the use of nonces. Another algebraic specification technique, based on the observational transition systems (OTS)/CafeOBJ method, has been used to formally analyze SNEP's data transmission and node to node key agreement protocols [23]. In [21], a generalized [PERSON]'s timed generalized non-deducibility on compositions (tGNDC) schema has been utilized for formal verification of well-known key management protocols for WSN, including \(\mu\)TESLA, Localized Encryption and Authentication Protocol (LEAP)+ and Lightweight Security Protocol (LiSP). Unlike SPINS, which is a network layer protocol, TinySec, a link layer security architecture, is fully implemented for the first time for WSNs [24]. TinySec is a lightweight protocol with a generic security package designed to impact minimally on performance. The security goals of TinySec protocols are access control, message integrity and confidentiality.