关键词: 安全设计模式, 代数规约, 形式化验证, 模型检测

Abstract: With the wide use of the World Wide Web and mobile computing technology, system security has received more and more attentions. Using security models to design and verify system security solutions is an effective way to improve the system security. The existing methods select the applicable security patterns according to the security requirements of the system and then combine the patterns into a system security solution. The security is verified by the model detection method. However, these methods often regard the scheme as a whole for verification, ignoring the combination details of internal security patterns, and it is difficult to locate defects in a complex system containing a large number of patterns. A verification method for pattern-driven system security design is proposed. Firstly, the algebraic protocol language SOFIA is used to describe the security model and its combination to build a formal model of the system security solution. Secondly, the SOFIA protocol is converted to the Alloy protocol, and the model checking tool is used to verify the correctness of the pattern combination and the security of the system. A case study demonstrates that this method can effectively verify the correctness of system security solution.

Key words: security design pattern, algebraic specification, formal verification, model checking