论文部分内容阅读
计算机和网络技术的迅猛发展，导致对计算机系统和开放式的网络系统的攻击日益增多。系统和网络之所以会受到各种各样的攻击，究其原因，最根本的是系统和网络内部存在各种安全缺陷。为此，人们设计了各种各样的安全策略、安全模型来确保系统的安全性，并使用密码协议来保证网络通信的安全。在这些安全策略应用到系统之前，我们必须验证它们是否能够满足其“声称”的安全目标；同样，我们也要对密码协议进行分析，检验其是否存在潜在的、未知的安全漏洞。不管是直接的或间接的机密数据泄露，都可以看作是信息的非法流动，因此可以采用信息流分析的方法，找出系统或网络中潜在的各种安全问题。信息流分析方法是信息安全领域较为本质的一种方法。本文首先介绍了非干扰信息流分析的一般方法，即非确定系统中的信息流非干扰分析技术；然后研究了概率系统和安全协议中的信息流性质，以及这些安全性质的验证方法；本文的主要创新工作如下：1．基于非干扰信息流分析的概率系统安全验证方法实际系统中，攻击者可以通过对系统行为观察进行统计，然后根据统计的概率数据构建概率隐蔽通道，导致机密数据的间接泄露。因此，本文在概率配置下研究了系统的安全性。首先本文对非确定系统中的分析工具SPA进行扩展，得到PSPA，用以描述概率系统的行为。本文提出了PPBNDC性质，并讨论了其在动态概率环境下的适用性，也给出了其不同语义等价下的特征描述，以及基于展开条件的特征描述。本文在PPBNDC性质的基础上，提出了SPBNDC和CPPBNDC性质，这些都是PBNDC性质的充分条件。本文还给出了这些PBNDC类性质之间的关系。这些分析是很有意义的，因为本文提出的这些概率系统中的信息流安全性质能够暴露出那些非确定系统信息流安全性质无法暴露出的系统安全缺陷。2．基于环境敏感信息流分析的安全协议验证方法为了能够描述安全协议的行为，我们对SPA进行扩展，形成了CryptoSPA。本文在CryptoSPA的环境敏感标记转换系统语义模型下，定义了环境敏感的路径等价和弱互拟等价关系，并提出了基于环境知识的一般组合上不可演绎的性质框架ESGNDC?α。在此框架下，讨论了NDCσ、BNDCσ以及PPBNDCσ性质。本文还在ESGNDC?α框架下，讨论了安全协议中的机密性，认证性和公平性，并指出了此框架也适合安全协议的活性分析。3．通过模型检查验证信息流性质BNDC类性质的定义中都有全程量词，因此验证一个系统具有这些性质是非常困难的。本文使用部分模型检查的方法来对BNDC类性质进行验证。首先通过SPA来描述系统的行为，对于某一特定的BNDC类性质，通过一些处理手段，将其定义转换为（E|TopE）＼H≈E＼H。这样，我们首先求出进程E＼H的特征公式φ，其中φ是模态μ演算的公式；那么证明进程满足BNDC性质就变为验证（E|TopE）＼H是否满足特征公式φ。同时本文还提出了安全协议分析中信息流性质的一般化分析，基于这种分析，我们使用的模型检查的方法完全适用于安全协议信息流性质的验证中。