攻击图是一种简洁的表现形式,它表现了一个系统中所有结束于一个不安全状态的路径,一个入侵者可以通过这些路径实现他的目标。系统管理员可以使用攻击图来确定他们的系统的脆弱程度,以及决定使用什么安全措施来加固系统。目前安全专家通过手动绘制攻击图来确定联网系统的脆弱点,但是手绘攻击图非常繁琐,且容易出错,对于大型系统来说也不现实,因此如何自动地生成攻击图并对其进行自动分析就很有必要。如果把攻击看成是对一个安全性属性的违反,我们可以使用模型检查来自动生成攻击图,对于攻击者来说一条成功的路径就是模型检查器产生一个反例。但传统的模型检查器只能为用户从错误行为集合中提供一个反例,这就影响了模型检查的效率,如何让用户可以得到全部的反例,也是需要研究的问题。在本文中,我们介绍了如何通过规范的技术让用户可以自由地检查由自动分析发现的设计缺陷。我们使用了模型检查的方法来给出结果,并对传统的模型检查理论进行了改进,提出了新的模型检查体系,即将所有的错误行为集定义成失败场景图。我们探讨了两种可以自动生成失败场景图的算法及其性能,即符号模型检查算法和明确状态模型检查算法。我们将该体系和算法应用在了网络安全领域,对网络攻击进行了建模,并定义了一种场景图的实例:攻击图,用于表现入侵者攻击计算机网络的过程。我们集中研究了攻击图的自动生成、表现和分析的方法,以解决现实世界中与网络安全有关的问题。本文主要的组织结构如下:首先定义了失败场景图,接着描述了根据有限模型生成场景图的两种算法并评测了它们的性能。随后将这些规范的概念应用在了安全领域,用场景图来定义并分析了攻击模型和攻击图,并探讨了在生成它们后如何进行分析。然后介绍了一个可用的攻击图工具包,包括它的框架、模块和用户图形界面。通过将该工具包应用在一个网络实例上,来显示它是如何生成攻击图并进行分析的。最后给出了结论。