Adaptive Model Checking For Security Protocols Based On L* Learning Algorithm

Security protocols are the basis of network security. Formal methods are the mainstream of analyzing whether the security protocol is in accordance with the security target. Currently it is necessary to amend or redesign the protocol with vulnerabilities artificially. This manual approach is not only inefficient, but also relies heavily on the experience, which leads to the possibility of involving new vulnerabilities.With the increasing complexity of the network environment and the growing requirements of communication security, the adaptive technology is introduced into the security protocol analysis. Security protocols, which are more effective and more responsive to network environment, are made by the integration and automation of protocol analysis and design. Adaptive model checking technology for security protocols based on L* learning algorithm is researched in this thesis.Firstly, security protocols and formal methods are introduced in the thesis. Attention is focused on the model checking technique.Secondly, an adjusted automata learning algorithm for security protocol adaptive model checking is put forward based on the classic learning algorithm called L* and its improved algorithms. The raw model can be refined by the L* algorithm through learning counterexamples. However, it has some limitations such as bounded alphabets and the minimal adequate teacher(MAT). In many application scenarios, however, a minimal adequate teacher might be unable to answer some of the membership queries because parts of the object to learn are not completely specified, not observable, it is too expensive to resolve these queries, etc. Then, these queries may be answered inconclusively. An adjusted automata learning algorithm called La* is proposed, through which the problem of inexperienced teacher and large alphabets can be addressed. It is proved to be correct and efficient. It will be helpful to improve adaptive model checking efficiency, reduce the cost, solve state space explosion problem and resist many kinds of attack methods for security protocols.Finally, conventional formal analysis methods for security protocols do not provide an automated revise function. This thesis provides a fully automated schema to not only evaluate security protocols' properties but also to correct their flaws mechanically. The most noticeable difference between our schema and the existing approaches is that our schema is a close loop framework, which can help to adaptively update the protocol model according to any change without human intervention. For a given protocol system, we only need a raw model to start the first round model checking. The counterexample created by model checking will not terminate the verification procedure. An automaton learning algorithm is used to update the model in terms of the counterexample. What's more, the counterexample will be further analyzed to ensure it whether a false positive. If so, would only the model be modified, otherwise the protocol itself should also be revised accordingly. Additionally, being a general framework, the schema could allow us to choose proper model checking technologies and automaton learning strategies as needed. An example implementation on the well-known Needham-Schroeder protocol illustrates the effectiveness of our schema.