Security analysis of Robust User Authentication Protocol

Ad hoc networks are a promising technology for implementing the ubiquitous computing paradigm. And, as in any other domain, security is a very important aspect. Authentication, as a first security goal to be achieved, has been targeted by many protocol propositions. But in order to use an implementation of such a protocol in a real situation, its security properties must be proved. Formal verification through model checking is a technique that can perform this demonstration with high accuracy. We present the use of formal verification over a protocol proposed for wireless sensor networks in order to correctly authenticate the user before allowing him to access the services of the network. Casper/FDR2 approach was used with success in proving that the desired security properties of the protocol were verified.