| With the rapid development of information technology, computer software system has been widely used in every social field. As the scale and complexity of software systems increases, it may also increase the possibility of software defects. Combination of the software development method and formal method is one of the good solutions for ensuring software quality and reliability.This paper presents a lightweight formalization framework based on extended UML, which combined the best of the UML and formal methods. Through analyzing the specific domain, this framework supports selecting and extending the appropriate UML models to model the specific domain, and then UML model can be transferred to formal model automatically. This framework can help to make it easier to use formal methods and make the formal methods popularized in the actual software development. Based on this framework, an extended UML method for the verification of security protocols has been proposed. In order to simplify the process and reduce the difficulty of security protocol modelling, extending mechanisms for the class diagram and sequence diagram of UML are presented, which provide an engineering specification for the security protocol formalizing. In addition, for verifying the confidentiality and correspondence of security protocols by ProVerif, a transformation from extended UML model to ProVerif Spi calculus model is realized with matching rules and knowledge reasoning. Besides, the verifying results are analyzed through a regular expression, so the flaws of protocol can be found easily, and it can also help to refine the modelsFinally, an UML-based verification platform for security protocols is developed, and the handshake, NS public key and buyer-seller watermarking protocols are verified, that shows the validity and applicability of this method. |
PDF Full Text Request