当前位置:首页 > 名家 > 专家新论 > 正文
安全协议形式化验证方法综述
发布者:  来源:  发布时间:2013-11-25

1 安全协议形式化方法现状

    作为安全协议研究中最重要的一种方法,形式化分析方法分支众多,目前较为常见的方法就有数十种之多,根据其理论基础和论证思路的不同主要可分为以下三大类:

    1) 模态逻辑。由一些命题和推理规则组成命题,表示主体对消息的知识或信仰,运用推理规则可以从已知的知识和信仰推导出新的知识和信仰。模态逻辑方法主要包含以下几种方法:BAN逻辑、类BAN逻辑,以及RV逻辑。BAN逻辑是最早的以逻辑形式提出的方法,它的一个重要特点是简单直观、易于掌握,其规则及推理与自然语言相似。但是,BAN逻辑还存在一定的问题:由于语义的不完备,使其可能无法检测出协议存在的某些安全缺陷。为了突破这一局限性,许多研究以BAN逻辑为基础,通过一定的改进或扩展,提出了新的逻辑方法,这些统称为BAN类逻辑。BAN类逻辑尽管存在这样那样的缺陷,但在安全协议形式化分析领域仍具有举足轻重的地位,而且其简单、直观、易用性仍受到很多人的欢迎,也带来了许多思路和启发。

    2) 模型检测(Model Checking)。最早是应用于硬件工作过程的分析和模拟,是一种有限状态并发系统自动化验证技术,顾名思义,它的一个重要优点是其自动化程度高。基本原理:首先用规范语言进行系统建模,然后用逻辑语言描述系统性质,最后以状态搜索算法验证系统相关性质是否能够得到满足。1996年,Gavin Lower首次将模型检测器FDR用于安全协议验证,结合CSP模型成功地发现了Needham-Schroeder公钥协议中一个近17年来未知的并行话路攻击缺陷。此后,作为安全协议自动化验证的最重要的方法,模型检测得到了快速发展。通过大量的协议分析表明,基于代数模型的状态检验方法是一种十分有效的方法,检测出很多新的攻击,其优点是自动化程度高,无需人为干预,自动产生反例来说明协议中存在的缺陷。但它还存在一些问题:状态空间爆炸问题,协议参与主体的数目需要受到限定。为了解决这个问题,引入了BDD的符号方法,使其能够搜索的状态扩展到10120个。

    3) 定理证明。首先用形式化语言进行系统建模,并以规约的形式给出系统要满足的属性,然后证明这些规约是否能够满足。它与模型检测相比,一个重要的区别是,模型检测是寻找协议中存在的缺陷,而定理证明方法则是证明协议所能够满足的安全属性,所以定理证明方法针对的是安全协议的正面,而模型检测方法针对的是安全协议的反面。定理证明方法的最大优势是参与主体数目不受限制,不存在状态空间爆炸问题,其不足之处是:①证明步骤多;②逻辑证明过程复杂,对使用者的水平提出了较高的要求;③自动化困难。

    作为目前主要的三大类形式化方法,其在安全协议领域所取得的成就有目共睹。然而,由于理论基础限制以及安全协议自身的困难性,使得这些方法在不同程度上都存在着缺陷。三类方法比较:

    1) BAN逻辑作为模态逻辑中最具代表性的形式化方法,其分析简单,较为实用,但只能分析安全协议的认证性不能分析保密性。BAN逻辑的最大问题是语义不完备性,利用其证明的安全协议,后来被发现存在安全漏洞。因此,人们只能相信BAN逻辑证明协议的不安全性,而不能相信其证明的协议安全性。

    2) 模型检测的优点是自动化程度高,能够自动验证一个系统是否满足其所设计的规范,然而模型检测方法存在状态空间爆炸问题,限定协议参与主体的数目。其显著的优点是对协议缺陷的检测较为直观。然而,跟模态逻辑方法一样,可能存在未能检测出的协议缺陷,并不能证明协议是完全正确的。

    3) 定理证明的方法不同于模型检测,其优点是能够处理无限状态空间问题,克服了状态空间爆炸问题。一般用于证明协议的正确性,难以用于发现协议的缺陷。而且,基于定理证明的方法在自动化方面无法与模型检测方法比拟。与前两种方法相比,定理证明方法验证的步骤往往非常多并且要使用逻辑推理,这使得其复杂性较高,要求使用者具备较高的水平。

2 Applied pi演算

    pi演算[5]作为一种成熟的形式化方法,有完善的理论体系以及支持其安全性验证的工具,但可以看到,pi演算虽然给出明确的语法定义及承诺,实现了进程通信和并发的构造,但并没有针对安全协议分析的相应设计。为了更加方便地使用pi演算来进行安全协议的形式化分析,Abadi等学者于2001年将pi演算扩展成Applied pi演算[6]。Applied pi演算继承了pi演算的通信和并发构造,增加了函数和等式原语。这个演算能很容易地处理标准数据类型,而且对安全协议的形式化描述也很方便,能够方便地表达协议的加解密、hash函数以及签名等操作。Applied pi演算中最重要的两个理论是观察等价(≈)和静态等价(≈s)。

    基于进程等价的协议安全性证明主要通过两个系统的观测等价来实现,其基本思想是将协议看作一个并行进程系统P,用另一个系统Q表示规范协议的并行进程运行模型,如果第三者(攻击者)不能区分这两个系统的行为,说明这两个系统是观测等价的,即协议是安全的。

    Applied pi演算的优缺点:Applied pi演算语义完备,协议会话数量或消息长度无需限制,不存在状态空间爆炸问题。虽然Applied pi演算与定理证明方法类似,都存在逻辑证明复杂的缺点,但能够借助于ProVerif工具实现对安全协议的自动化证明,这使得使用者无需具备极高的逻辑推理能力也能够完成安全协议的验证工作,极大地降低了工作的复杂度。定理证明方法一般可以用这种方法证明协议的正确性,难以用于发现协议的缺陷,而Applied pi不存在这个问题。ProVerif工具在验证安全协议时能够给出安全漏洞的攻击路径。在使用ProVerif验证安全协议时也存在不足,该工具能验证协议的正确性,并且能给出安全漏洞的攻击路径,但由于没有严格的时序,造成所返回的攻击是不合理的。针对这个问题,可以采用自动化验证与人工验证相结合的方法来解决,针对ProVerif返回的攻击路径采取人工方法再验证一遍,从而确保了安全协议验证的正确性[7-8]。

3 规约

    规约,通俗地讲就是系统所满足性质的一个描述,而形式化方法中的规约就是基于一定的数理模型对系统性质的描述。在pi演算中就巧妙地应用了规约与系统之间是否满足弱互模拟性来验证系统设计的正确性。文献[6]中列举了彩票机、加工车间等例子来说明定理规约≈系统在系统正确性验证中的应用。从这些例子中可以看到一个共同特点:一个有很多交互的系统与一个几乎没有交互的规约满足弱互模拟性,即两个内部相差较大的模型的外部表现是一样。下面以加工车间的例子来简要介绍一下其应用原理。

    两个工人在一条流水线上工作,他们从一个用i表示的传送带O上获得半成品,加工完成后放到传送带 上。半成品难度分成容易、中等和困难。第一个系统Agency:两个工人A处理起各个难度的半成品都同样得心应手,没有什么不同。第二个系统Jopshop:两个工人J能力稍差,需要使用铁锤才能加工困难的半成品,使用铁锤或者木槌才能处理中等(N)的半成品,且只有一个铁锤和一个木槌供两人共享。显而易见,两个系统存在较大区别,第二系统有更多交互,然而这两个系统却满足Agency≈Jobshop,也就是说,这两个系统的外部行为是一致的,这正是我们需要的,详细证明过程见文献[6]。对于一个安全协议,如果能证明其外部表现安全,那也就证明了其安全性,但这一点是困难的。

    在过去的二三十年中有关顺序系统和交互系统的严格规约已经有了大量的工作。通常的作法是用一个逻辑语言来定义规约,而系统则可以由像π演算这样的多种方式来描述。那么这种规约≈系统的验证方式在安全协议分析中是如何来应用的呢。在Applied pi演算中提出的观察等价和静态等价两种等价关系就是在pi演算弱互模拟性的一个扩展。在目前形式化验证安全协议的研究中,规约确实已经广泛应用,所采取的方式是给安全协议的认证性、数据完整性等安全性质的规约,而非完整的安全协议规约。这里根据所关注的性质对安全协议予以验证,大大减少了分析的难度,增强了可操作性。基于目前规约≈系统的方式在顺序系统和交互系统中已取得成果的基础上,可以看到的是随着形式化方法研究的不断深入,这种验证方式在安全协议的分析中大有可为,也具有极高的研究价值。

    基于规约证明的安全协议形式化验证主要可以归结为以下几个步骤:

    1)首先考虑安全协议不存在攻击者的情况,也就是协议的执行是绝对安全的,根据Applied pi演算的语法规则对其进行建模,将其作为规约。

    2)存在攻击者的情况,除了对安全协议本身建模以外,还需要对攻击者进行建模,并将两者结合作为系统。

    3)验证规约与系统是否满足弱互模拟性。如果有规约≈系统,则说明规约和系统的外部表现是一样的,也就是攻击者没有对协议的运行结果造成影响,从而证明了协议的安全性。

    基于等价的安全协议形式化验证的总体步骤和思路清晰明了,然而想要成功地验证安全协议的性能还需要注意以下几点:安全协议建模的准确性、攻击者能力刻画的全面性、等价证明的逻辑严密性。

4 结语

    作为安全协议研究的一个主要手段,形式化方法的重要性是无可替代的。但由于安全协议分析自身的困难性、算法的复杂性以及形式化方法存在的一些局限性,迄今为止还没有哪种方法能够完全证明一个协议是安全的。安全协议的形式化分析和自动化验证是一项具有相当复杂性和挑战性的工作,虽然出现了众多的形式化分析方法和验证技术,但目前还没有形成一套十分成熟的理论体系。随着形式化研究的不断深入,现有理论和方法会得到进一步的完善和扩充,形式化技术将会发挥更为重要的作用,这一作用的发挥还有赖于学术界研究人员的共同努力。

 

分享到:
合作伙伴: