Formal Analysis For UML Model Of Security Protocols Using SPIN

UML is a universal visual modeling language used in object-oriented modeling. In spite of its richness expression and expanding ability, UML is not a formal modeling language, it lacks exact semantics, and this leads the weakness in analyzing and validating UML models. Formal methods has the supports of precise mathematic semantics and automatic formal tools, which could be used in analyzing software specification, but formal methods has the disadvantages in designing large-scale software and difficulty in system modeling. To reduce the risks on system development, it is very necessary to formalize and verify UML models.This paper tries to combine the advantages of UML and formal methods, gives a method which could be used to translate UML to PROMELA specification, first we choose the core subset of UML which contains Class Diagram,Sequence Diagram and State Diagram to model the security protocols, then depends on the algorithms we provided to transform it to PROMELA, at last the SPIN model checker was put forward to validate it. this method avoid modeling protocol using formal language PROMELA directly, reduce the difficulty in using formal methods, and give reference to the precise semantics of UML. When this prototype system is perfected, it can be used as an efficient analysis tool to analyze the security of network communication system which takes the network authentication protocol as the kernel of security.