安全协议，又称密码协议，是建立在密码体制基础上的一种交互通信协议，它运行在计算机通信网络和分布式系统中，借助于密码算法来达到密钥分配、身份认证等目的。目前，安全协议已成为国际信息安全领域的主流研究方向之一。
　　安全协议是构建安全网络环境的基石，它的正确性和安全性对于网络安全至关重要。协议的安全分析是揭示安全协议是否存在漏洞的重要途径。分析方法有攻击检测方法和形式化分析方法等。20世纪80年代末、90年代初以来，安全协议的形式化分析成为研究热点。目前，安全协议的形式化分析方法大致可分为三类：形式逻辑方法、模型检测方法和定理证明方法，它们既有各自的优势，又有各自的劣势。基于此，本文通过把UML2.0与时间自动机结合起来分析和验证安全协议，探索一种将可视化建模语言与形式化方法有效结合的安全协议分析的新途径。具体研究内容如下：
　　(1)介绍了安全协议背景、基本概念及分类，分析和比较了当前安全协议形式化分析的三类主要方法，提出了可视化与形式化相结合的安全协议分析的新方法。
　　(2)介绍了统一建模语言UML2.0及其扩展机制，扩展了UML2.0顺序图，给出了UML2.0交互视图中的顺序图的形式化描述。
　　(3)给出了UML2.0顺序图模型到时间自动机模型的转换方法。这种方法首先将UML2.0顺序图分解得到的所有简单子片段转换成对应的时间自动机，然后根据组合片段转换方法进行合并，最后得到目标时间自动机。
　　(4)将本文提出的可视化与形式化相结合的方法运用到简化了的Needham-Schroeder认证协议（简称NS认证协议）分析中。实验结果表明，入侵者可以轻松地对该协议进行有效攻击。从而证明该方法可用于安全协议分析。
　　此外，典型的安全协议形式化分析方法没有考虑时间因素，这个选择使得分析简单化。在对NS认证协议进行分析时，考虑消息实际传输需花费时间，加密消息、解密消息和产生临时值等都需花费时间，从而构建NS认证协议的时间自动机模型。这种方法使得安全协议分析更切实际。