Dissertation > Excellent graduate degree dissertation topics show

Security Protocol visual modeling and verification methods for analysis and design

Author: FuJie
Tutor: SongMaoQiang；ZuoZhongLiang
School: Beijing University of Posts and Telecommunications
Course: Software Engineering
Keywords: Security Protocols Formal Analysis Model Checking Visualization model SPIN
CLC: TP393.08
Type: Master's thesis
Year: 2009
Downloads: 19
Quote: 0
Read: Download Dissertation

Abstract

With the increasing development of network technology and the Internet in the global popularity of network security issues has been growing attention. Security protocol is the cornerstone of building a secure network environment, security is a security protocol network security key. It has been proven through a number of different methods that already exist, such as security protocols are not as secure as they claim, the security for security protocol analysis and verification has become a hot research scholars at home and abroad. In order to guarantee the correctness of security protocols, researchers have proposed a variety of analytical methods to solve this problem, but there are some deficiencies. Unified Modeling Language (Unified Modeling Language, UML) is the international advanced software analysis and design for visual modeling language, is a well-defined, easily expressed, powerful and universal modeling language. However, UML lacks precise semantics description of the UML model for further analysis and verification more difficult. Formal methods have precise mathematical semantics and automated verification tool support, you can rigorous analysis software specification and verification, formal methods exist but difficult to design large-scale software, the direct use of formal specification of the system modeling is difficult and other shortcomings. To ensure the security protocol correctness of the design, in the early detection of possible errors, the agreement is formalized analysis visualization model validation is necessary. Simple process meta-language interpreter (Simple Promela Interpreter, SPIN) as a tool for model checking, because with a small memory space occupied and assurance procedures in accordance with the original work is efficiently validated characteristics, are widely used in industry and academia, therefore, we use security protocols SPIN tools UML visual models are analyzed verified. This paper introduces the security protocol, security protocol formal analysis methods, model checking techniques, and focuses on visual modeling language UML and model checker SPIN principle, combined with object-oriented visual modeling and the advantages of formal methods, proposed a kind of security protocol visualization model into PROMELA specification method. First select the UML, including class diagrams, sequence diagrams and state diagrams to model the core subset of the security agreement, and then define a subset of the UML to PROMELA language conversion rules, according to the rules it is automatically converted into PROMELA specification, then call the model SPIN detector for automatic detection. This method avoids the direct use of formal modeling PROMELA language of the agreement, so that the difficulty of modeling and greatly reduces the possibility of error, with high reliability and efficiency analysis. Finally, based on the above research, analysis and design of the UML model to Promela conversion conversion tool.

Related Dissertations

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer applications > Computer network > General issues > Computer Network Security
© 2012 www.DissertationTopic.Net Mobile