Model Checking of the NS Cryptographic Protocol and Analysis Based on the UPPAAL
Guangquan Zhang · Chongqing Shifan Daxue xuebao. Ziran kexue ban · 2009
Formal analysis methods are currently the mainstream method of cryptographic protocol analysis.Typically,the methods for formal verification of security protocols do not take time into account,and this choice also simplifies the analysis.A methodology is presented here by using a model checker of formal methods based on timed automaton,UPPAAL,to analyze a simplified version of the well known Needham-Schroeder Public-Key Protocol(NS for short).Since the actual sending of the message takes time,timeliness of the message is introduced when modeling the NS protocol.Thus timed automaton for the NS protocol is obtained.Because the check engine of the UPPAAL adopts advanced technology,this methodology can void the state space explosion problem arisen in the general timed automaton application.One of the possible forms of NS protocol authentication failure is presented in UPPAAL tool.This experimental result indicates an intruder's attack upon the NS public-key protocol.Therefore the UPPAAL could find the flaw of the NS protocol.