基于UML安全协议的建模和自动检测-计算机软件与理论专业论文.docx

F·：531 F·：531 8 华南师范大学硕士学位论文 基于UML安全协议的建模和自动检测 摘要 网络安全是目前人们关注的一个热点，而安全协议的安全性却是网络安全的 关键。安全协议应用于网络上传送文件和进行各种交易以及对计算机系统的访问 等。人们已通过不同的方法证明一些已存在的安全协议并不如它们所声明的那样 安全。对安全协议的安全性进行验证成为国内外研究的热点。 本文主要研究安全协议的可视化建模，以及自动检测。论文首先介绍了安全 协议，接着介绍安全协议的形式化方法和自动检测方法，并着重介绍模型检测工 具SPIN的原理和它的建模语言PROMELA。接着提出了安全协议的UML建模规则和 过程，并讨论了安全协议的UML模型转化成PROMELA语言的过程以及如何自动产 生攻击者模型。为了实现安全协议的可视化设计与自动验证，开发了自动转化工 具来实现这一日标。 关键词：安全协议，SPIN。模型检测，UML。 第1页麸72页 华南师范大学硕士学位论文 华南师范大学硕士学位论文 基于UML安全协议的建模和自动检测 AbStract The network security is a focus which people pay close attention to at present，and the safety of security protocol is the key to the network security．The security protocol applies to conveying the file，carrying on various kinds of trade in the network and visiting to computer system etc． people have already proved that some security protocols are not as safe as they have been declared through different methods．So verifying safe of security protocol becomes the hotspot． The main task of the thesis is to investigate the visual modeling and automatically verifying of security protoc01．The paper introduces the security protocol at first，and introduces the formalized methode and automatically verifying of security protocol，It also introduces the principles，characteristics of model checking tool SPIN and its modeling language PROMELA emphatically．Then the paper proposes the rule and course of UML modeling of security protocol，and the process of transforming UML model of security procotol to PROMELA programs and how to produce attacker model automatically are presented．In order to combine the visual design of security protocol with its automatically verifying．the automatic verification tool for UML model of security procotol has been designed and developed． Key words：Security procotol，SPIN，Model checking，UML． 第2页共72页 华南师范大学硕士学位论文 华南师范大学硕士学位论文 基于UML安全协议的建模和自动检测 第一章 绪论 I．I．课题背景 随着网络技术的应用与发展，特别是政府、军事机构，以及电子商务的兴起 与广泛应用，信息安全问题成为学术界和工业界共同关注的关键问题，