Model Checking of Needham-Schroeder Protocol Using UPPAAL

摘要

Currently, formal methods are the mainstream methods of cryptographic protocol analysis. Typically, these most used approaches for the protocols analysis do not take time into account, and this choice simplifies the analysis. However, cryptographic protocols like distributed programs in general are sensitive to the passage of time. A method for the protocols that are aware of timing aspects is presented using a model checker of formal methods based on timed automata, UPPAAL. We study a simplified version of the well known Needham Schroeder Public Key Protocol (NS protocol for short). Since the actual encrypting and decrypting of the message takes time, timeliness of the message is introduced when modeling the simplified protocol. Thus, timed automata for the simplified NS protocol are obtained. Due to the check engine of the UPPAAL adopting advanced technology, this method can avoid state space explosion problem arisen in the general timed automata application. The possible forms of simplified NS protocol authentication failure are presented in UPPAAL tool. This experimental result illustrates an intruder's attack upon the NS public key protocol. Therefore the method could find the flaws of the simple protocol.