## 1 Introduction  
Wireless sensor networks (WSNs) are increasingly used in critical applications where the identity of each communicating entity should be authenticated before exchanging data in the network. The wireless nature of this technology makes it easy for intruders to try to intervene in the network activity and create any of the known attacks in WSNs [1]. Many of the current propositions focus on message authentication for ensuring data authentication and integrity, and others focus on user authentication to give access to the network for certain user profiles. In this paper we propose, on one hand, authentication protocols that allow nodes to join the network in a secure manner, and on the other hand, key establishment protocols that allow nodes to establish keys with nodes that are multiple hops away. Designing secure protocols is an error-prone task. One of the well-known examples is the famous flaw found in the Needham-Schroeder protocol seventeen years after its publication [2]. This protocol aims at establishing a new key between two participants. It is simple since it uses only three exchanges of messages. It clearly shows that designing secure protocols is not an easy task and is error-prone. During the past decades, several automatic tools for verifying the security of cryptographic protocols have been elaborated by several authors, e.g., [PERSON] [3], [PERSON] [4] or Scyther [5]. These symbolic tools use the Dolev-Yao intruder model [6], which considers that the intruder is controlling the network and makes the perfect encryption hypothesis (meaning that it is impossible to obtain the plain text of an encrypted message unless the secret key is known). The state-of-the-art [7] shows that formal methods are now mature and efficient enough to be used in the design of security protocol in order to avoid such logical flaws. Another aspect that should be taken into account during WSNs protocol analysis is the performance related to the security operations. Traditional approach assumes that the best way is to apply the strongest possible security measures to make the system as secure as possible. Unfortunately, such reasoning leads to the overestimation of security measures, which causes an unreasonable increase in the system load [8]. The system performance is especially critical in systems with limited resources such as wireless sensor networks or mobile devices. It is important to design secure mechanisms using, when possible, a fixed number of cryptographic operations regardless of the network size, and to be able to evaluate their performance in such constrained devices. In this paper, we propose several protocols that do not add cryptographic operations on intermediate nodes. We systematically evaluate their overhead and prove their correctness with the automatic formal security verification tool Scyther [5]. The originality of our work resides in the fact that it suites large scale multi-hop wireless sensor networks, which is due to the limited number of cryptographic operations regardless of the number of hops separating the communicating nodes. In addition, it combines several aspects of security, from designing secure protocols to evaluating the implementation of our solution, going through formal automatic analysis of security and overhead of protection analysis. Our contributions can be summarized in the five following points:  
1. Design of multi-hop node authentication mechanisms. 2. Formal automatic analysis of our solutions. 3. Implementation on TelosB motes. 4. Evaluation of the overhead of protection of our solutions. 5. Attack detection based on the _a priori_ overhead evaluation. Our main contribution is the design of several secure authentication protocols. In order to avoid security flaws, we prove the correctness of all our protocols automatically using Scyther [9], which is a tool for the automatic verification of security protocols. This tool considers neither the cost of the communications nor the execution time of the cryptographic operations.