陈铁明[1]2004年在《复杂安全协议的形式化分析、设计与验证研究》文中研究说明保障网络通信安全的一个极其重要的环节是安全协议，安全协议的形式化分析方法已成为近年来安全领域研究的热点之一。同时，PKI体系作为一个强有力的网络安全保障系统已被广泛地应用于各种商业网络环境，各种基于PKI应用的复杂安全协议也成为研究和发展热门，其中以SSL协议的应用最为成功。目前，试图用简单的推理构造逻辑方法分析诸如SSL的复杂安全协议其效果不尽人意，因此，本文的研究重点就在于提出一种新的形式化分析思路来分析和设计复杂的安全协议。 复杂安全协议本质上就是由简单的协议模型不断进化而得，因此本文采用基于代数规范的方法提出一个安全协议的进化模型框架，安全协议的主体均可采用该框架得以形式化描述，并通过进化模型的扩展达到安全协议进化的目的。本文采用着名的信念逻辑GNY逻辑系统及其相关的形式化工具SPEARⅡ，以SSL协议为分析实例，详细阐述了从初始协议模型到各个进化协议模型的分析过程，并将最终的进化模型与SSL协议作比较，给出SSL协议的安全分析，同时在分析过程中以协议模型为基础设计了两个实用的安全认证方案。因此，本文提出的进化协议思路不仅有助于对复杂协议的分析，还不失为一种复杂协议的设计方法。另外，本文在使用GNY逻辑的分析过程中，提出叁条实用的GNY扩展规则，而在文章最后，对基于攻击逻辑的安全协议验证方法作了初步研究，提出了将该协议攻击验证技术融入协议自动分析工具的设计框架。
周倜[2]2008年在《复杂安全协议的建模与验证》文中认为随着网络的发展,互联网络的安全问题变得越来越棘手,越来越重要,安全协议的安全性质也受到越来越多的挑战。安全协议是解决互联网络安全问题最有效的手段之一,使用安全协议在开放的互联网络上可以实现身份认证等多项安全功能。由于在计算机网络中,相互通信的双方不能通过生物特征识别对方,因而彼此的认证需要建立在密码体制的基础上。安全协议是建立在密码体制基础上的一种通信协议,它运行在计算机网络或分布式系统中,借助于密码算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定任务的执行步骤和执行规则。安全协议的正确性对网络应用的安全至关重要。然而,设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明的安全性质。许多协议在应用了很长一段时间后被发现存在安全漏洞。设计和开发高效的安全协议建模与验证的方法和工具是安全协议形式化研究领域的一个研究热点,也是验证复杂安全协议的关键环节。本文以Bruno Blanchet提出的Horn逻辑模型为基础,对反例构造算法和复杂协议验证方法进行了系统、深入的研究,主要工作包括以下几个方面:1.基于Horn逻辑的安全协议反例的自动构造算法。Bruno Blanchet提出了基于Horn逻辑的安全协议模型,该模型可高效地验证安全协议。为了将消息的角色信息保留在模型中,本文设计了相关的数据结构,给出了反例自动构造的算法实现,使验证工具能从不满足安全性质的消解序列中自动地构造出标准形式的反例,从而方便人们使用基于Horn逻辑的验证工具验证协议。2.不动点计算的不停机性预测。安全协议验证的不停机性源于不动点计算的不停机性。通过研究安全协议逻辑程序解形式不动点计算不终止的特征,本文给出了不动点计算不终止的预测方法。基于此方法,可以在协议验证时自适应地选择(精确或抽象)验证方法验证(停机或不停机的)安全协议。3.抽象与精化迭代验证框架。安全协议的正确性验证问题是不可判定的,使用抽象解释理论能够有效地验证安全协议。通过研究Horn逻辑模型中协议验证的特点,给出了安全协议基于抽象-精化的迭代验证理论框架。抽象验证保证停机,而精化过程可有效地去除虚假反例。因此,抽象-精化迭代框架可对Horn逻辑模型中验证过程不停机的安全协议进行有效验证。为了提高抽象模型的精度,本文进一步提出了局部抽象-精化迭代验证的理论框架。局部抽象可以提高整个验证过程的验证效率,为复杂协议的验证提供了有效的途径。4.时间敏感安全协议的建模与验证。通过将描述时间的事件加入到进程代数模型中,使得时间戳能方便有效地在协议模型中描述出来。将时间元素的线性约束加入到基于Horn逻辑的安全协议模型中,使得Horn逻辑模型能有效地处理时间约束信息。通过研究规则中各时间元素与消解的关系,找到了确定时间相关元素的时间先后关系的办法,提出了两阶段验证方法。一条规则是否可用,此时还需考察其所对应的约束系统是否可满足。因此,本文对该模型下的约束系统进行了研究,提出了一个高效判断其可满足性的判定算法,并证明了该算法是多项式时间算法。由于约束系统中存在大量冗余的不等式,本文还深入研究了该系统,针对其本身的特性,提出了约束的抽象理论简化约束系统,该方法能有效地降低时空开销。5.设计并实现了一个高效的安全协议验证工具SPVT-II。本文提出了不停机性预测和抽象-精化迭代验证框架的实现算法,在安全协议自动分析工具SPVT的基础上,结合抽象-精化迭代验证框架,设计并实现了一个自适应选择验证方法的高效的协议验证工具SPVT-II。该工具既能发现协议中可能的反例,也能尽可能地减少虚假反例的产生。6. Kerberos协议协议的分析与验证。本文通过对Kerberos协议进行分析,将公钥Kerberos协议的认证服务交换阶段进行了建模,并用SPVT-II对协议模型进行了自动化的验证。实验结果表明SPVT-II能自动发现PKINIT-26中认证服务阶段的攻击。
边瑞昭[3]2007年在《3G的安全增强研究及认证与密钥协商协议设计》文中提出本文深入研究了3GPP接入安全机制,重点分析了认证与密钥协商协议3GPP-AKA。该机制存在用户永久身份信息易被窃取、终端与服务网络双向认证不完全、序列号操作困难等缺陷,使其不能满足特殊部门高级别的安全需求。为使移动终端更安全地接入3G网络,提出了能够指导3G安全保密系统建设的叁维体系框架,设计了安全增强的认证与密钥协商协议SE-AKA,包括漫游时完全认证与密钥协商、漫游时快速重认证与密钥协商、非漫游时完全认证与密钥协商和非漫游时快速重认证与密钥协商四个子协议。首先用SVO逻辑对协议的安全需求进行了形式化描述。然后,研究了协议的密钥建立框架和认证框架,确定了协议中认证与密钥协商的顶层抽象模型。依此模型,分别设计了四个子协议。最后,选择SE-AKA中最复杂的子协议(漫游时完全认证与密钥协商协议),对其安全性作了基于SVO逻辑的形式化分析,并将SE-AKA协议与3GPP-AKA协议的安全性进行了比较。结果表明,SE-AKA协议在永久身份保密、双向认证、不可否认性等方面的安全性都优于3GPP-AKA协议,使UMTS接入网络能够抵抗改向攻击和主动攻击。而且协议中消除了重同步机制,避免了序列号操作困难带来的危害。这些安全功能满足了3G环境下特殊部门高级别的安全需求。
王强[4]2012年在《安全协议形式化验证方法研究》文中研究指明随着计算机网络技术的不断发展，网络信息安全已经成为信息时代的一个至关重要的问题。安全协议作为网络安全通信的基础技术，是确保网络信息安全的有效手段之一。然而实践表明，设计正确可靠的安全协议是一项十分困难的工作，许多广泛使用的安全协议被指出存在各种安全漏洞。因而，分析和验证协议的安全性具有重要的应用价值。目前，研究人员主要采用形式化方法来分析和验证协议的安全性。本文以符号模型下安全协议的形式化验证方法为研究内容，主要分析和拓展了基于应用Pi演算的安全协议建模和关键安全属性的自动化验证技术，取得了一系列有价值的研究成果。主要研究内容和成果体现在：（1）基于应用Pi演算的安全协议建模和验证方法研究。首先分析了应用Pi演算框架下安全协议及其安全属性的建模方法，其次分析了两类不同的安全属性形式化验证技术：基于协议迹的可达性分析技术和基于协议进程观测等价的互模拟验证技术，指出了上述两种技术方法的优缺点和存在的挑战，给出了进一步改进的思路。（2）基于约束系统的保密性验证方法和约束求解算法研究。针对可达性分析技术存在的不可判定的缺点，首先提出了基于约束系统的安全协议建模与验证方法。约束系统是对协议执行迹的符号化表示，将无穷的协议迹抽象为有限的约束系统，并将安全性验证问题转换为带安全属性公式的约束系统的可满足性判定问题；其次深入研究了HubertComon-Lundh的约束求解算法，分析了该算法的正确性、完备性和停机性。该算法可以实现安全协议的自动化验证，但存在时间复杂度较高的不足。（3）改进的协议进程迹等价判定算法研究与实现。针对应用Pi演算中观测等价性不可判定的不足，研究了应用Pi演算的可判定子集—简单进程的迹等价判定算法。首先深入分析了Vincent Cheval的不含异或算子的迹等价判定算法，对原算法进行了适当改进，降低了复杂度，给出了该算法Ocaml语言实现；其次，首次提出了含异或算子的迹等价判定算法，该算法可以用于简单进程的自动化迹等价判定，也可用于安全协议的复杂安全属性的形式化验证。由于简单进程的迹等价和观测等价是一致的，该算法也可用于观测等价性的判定。
鲁来凤[5]2012年在《安全协议形式化分析理论与应用研究》文中指出安全协议是一种运行在计算机网络或分布式系统中、借助于密码算法来达到密钥分配和身份认证等安全目标的通信协议,是解决计算机网络和分布式系统中安全问题的必要手段。然而，安全协议未必是安全的，它的安全性分析一直是一个复杂而困难的问题，对安全协议的研究已成为世界上信息与网络安全方面的一个重要研究方向。实践证明，形式化方法是安全协议安全性分析更为可靠和有效的途径。本文以安全协议作为研究对象，以DDMP理论为研究工具，对安全协议形式化分析方法从理论和应用两个层面展开研究，所取得的研究成果主要有：（1）设计了安全协议形式化分析模型。给出了安全协议的系统模型，设计了安全协议形式化分析的一般模型SPFAM和基于DDMP理论的安全协议形式化分析模型DDMP-SPFAM。在模型图的基础上，给出了相应的模型算法，具体阐述了形式化分析遵循的步骤，对安全协议的形式化分析和设计提供了宏观指导。（2）研究了基于协议组合逻辑（PCL）的形式化分析方法。给出了基于PCL证明协议安全属性的一般方法，选取国际标准ISO/IEC DIS11770-3中提出的重要认证协议Helsinki作为研究对象，讨论了该协议存在的缺陷及受到的攻击，改进协议，利用PCL对改进的协议方案进行形式化建模，并进行安全性证明。改进型的Helsinki协议基于PCL是安全的。（3）研究了安全协议的组合性问题。讨论了基于符号和基于计算复杂性的形式化分析领域中协议组合分析工具的代表PCL与UC，选取PCL作为协议组合分析的工具；详细阐述了PCL进行组合分析的过程；选择典型的包含可信第叁方的密钥交换协议Otway-Rees展开讨论，分析了协议本身的缺陷及其遭遇到的攻击形式，提出了改进方案（AOR协议）；扩展PCL，利用PCL对改进后的AOR协议进行了形式化建模和模块化安全性证明。AOR协议能满足密钥保密属性。（4）从非形式化和形式化两个方面研究了安全协议设计方法。在非形式化方面，针对安全协议设计规范、原则展开讨论；在形式化方面，阐述了协议演绎系统PDS的设计思路和具体方法，针对现有PDS主要基于无可信第叁方参与的公钥密码体制下的安全协议演绎现状，设计出新的协议组件和操作集合，扩展了PDS系统，设计了一系列安全协议。
汪卫[6]2012年在《形式化验证安全协议Java代码的安全性》文中认为安全协议分析和验证在信息安全领域占有重要地位。目前，安全协议形式化方法分析和验证主要集中在对实用性较差的安全协议抽象规范分析和验证方面，对注重实用性的安全协议代码分析和验证涉及比较少；而静态程序验证技术的应用主要集中在程序正确性等方面，很少涉及代码的密码学安全性。因此本文将结合安全协议形式化分析与验证和静态程序验证技术来分析和验证安全协议Java代码密码学安全性。本研究成果具有较强的理论意义和一定的应用价值。本文主要工作如下：1.对安全协议分析和验证做了一个完整的概述，说明了进行形式化分析的必要性，介绍了形式化分析的模型并详细描述了形式化分析和验证的方法。2.探讨了Java语言的形式化描述，具体介绍了Java语句和表达式到应用PI演算语句的映射。同时，介绍了程序静态分析方法，研究了如何利用抽象语法树对程序进行预处理。3.首先探索Java代码抽象模型抽取方法和从Java代码到应用PI演算的映射；然后应用一阶定理证明器ProVerif分析与验证Needham-Schroeder协议Java代码的密码学安全性。
左向晖[7]2011年在《可信信道协议的设计与形式化验证》文中提出目前绝大多数的网络安全通过建立安全信道来保护信息的安全传播,例如SSH、IPSec。然而,随着恶意用户的攻击手段越来越高明,现有的计算机系统很容易遭受恶意代码攻击、信息非法窃取等安全威胁,即通过损害终端平台来实施攻击。可信计算技术可以通过提高平台安全性来提高安全通道技术的安全强度。可信计算技术从一个可信根开始,按照系统控制权的转换顺序逐级进行完整性度量并形成可信链；最后分析可信链以判断该计算平台是否可信。本文提出了基于SSH协议的可信信道协议,旨在通过将可信计算的远程证明与安全信道连接建立这两个过程进行有机整合,在保证数据安全传输的前提下,加强了数据在通信端点的安全性。本文首先研究了可信计算基础理论,尤其是可信度量机制和远程证明技术。重点分析了开源OpenSSH软件的握手连接过程,结合远程认证的直接证明模式与OpenSSH软件的会话密钥协商方法,设计了可信安全连接的建立过程和密钥交换环节的步骤。为了证明所提出的方案满足一定的安全特性,本文研究了安全协议的形式化分析技术,使用符号化模型检测工具NuSMV验证了两个抽象化的可信信道协议。检测结果表明,第一个协议没有达到既定的安全目标,尚不具备必要的安全属性。通过分析NuSMV输出的反例,改进后的第二个协议通过了安全属性验证。最后提出了可信信道协议的基本框架,该框架实现了远程证明过程对密钥交换算法的透明性,以及平台信息在网络传输过程中的秘密性。
石曙东[8]2009年在《网络协议安全性分析中的逻辑化方法研究》文中提出安全协议是建造网络安全环境的重要基石,是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性,成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法,对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击,但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善,存在一定的局限性,不能分析和验证某些类型安全协议的安全性:有些只能分析安全协议的不安全性,不能给出协议安全性的精确证明。在总结安全协议现存各种缺陷的基础上,根据缺陷产生各种原因将缺陷分为:过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为:重放消息型攻击、猜测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定型攻击等六类。Burrows,Abadi和Needham提出的BAN逻辑开创了用逻辑化方法分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象,逻辑处理的符号集是对现实具体协议的抽象;其初始假设、断言集合等均是从现实世界中抽象出来的要素。因此,其狭窄的符号集合定义也就决定了该方法存在不能分析某些类型协议安全性的缺陷,如:不能发现由于时间同步问题而导致的协议缺陷。另外使用BAN逻辑对安全协议分析时,很多初始假设是不合理的,如消息不可伪造假设就非常不合理,这些假设的不合理,妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷;语义不清晰缺陷;非严密的环境模型缺陷和无法有效预测对协议存在的攻击等缺陷。1995年由Raiashekar Kailar提出的Kailar逻辑主要用于描述和分析电子商务协议,但是它只能分析电子商务协议的可追究性,无法分析电子商务协议的另一个重要特性——公平性。与BAN逻辑一样,使用Kailar逻辑分析协议之前同样需要引入一些初始假设,而初始假设的引入仍然是一个非形式化的过程,具有一定的人为性,其不准确会导致安全协议分析的失败。另外,用Kailar逻辑解释协议语义时,只能解释签名的明文消息,这样限制了其使用范围,对某些安全协议不能分析。针对BAN类逻辑和Kailar逻辑的弱点,设计了一种新的安全协议分析逻辑CPL(Cryptographic Protocols Logic),CPL不但可用于分析协议的安全性,还可用来设计安全协议,即CPL逻辑把分析和设计安全协议纳入同一个逻辑体系中,消除了用不同方法分别设计和分析安全协议,将导致结果不一致性的缺陷,同时也简化了分析和设计安全协议时对初始条件和安全协议最终目标分别进行形式化的过程和步骤,提高了分析和设计安全协议的效率。定义了CPL逻辑的基本符号、给出了CPL逻辑用于分析协议安全性的六类二十五条逻辑分析规则和用于设计安全协议的二十九条逻辑设计规则。分析规则和设计规则可分别用于安全协议的分析和安全协议的设计。给出了基于Kripke的CPL逻辑的语义,并利用逻辑语义对CPL系统自身的正确性进行了详细证明。运用新逻辑的分析规则和协议运行的初始条件以及安全协议的执行步骤分析安全协议的安全性。运用新逻辑的设计规则和协议运行的初始条件以及协议的最终目标设计出满足安全要求的安全协议。使用新逻辑分析了两个不同类型协议的安全性——密钥建立协议和身份认证协议。
虞震波[9]2015年在《基于CSP模型检测的无线传感网安全协议形式化验证》文中研究指明由于协议开发过程中,复杂的协议流程和协议应用场景可能会导致协议描述出现逻辑漏洞,致使整个系统产生逻辑冲突。协议的安全性和可靠性对协议是否能够安全有效的运行有很大影响,因此安全性分析和验证一直是协议设计的重点和难点。基于通信顺序进程(Communicational Sequential Processes,CSP)的安全协议形式化分析验证已成为当前一个研究热点,基于CSP的安全协议模型可有效提高形式化分析和验证的效率。另一方面,随着无线传感网络(Wireless Sensor Networks,WSN)应用的日益广泛,其安全问题也逐渐突出。因此,将CSP方法应用到WSN安全协议的形式化分析和验证,在协议设计阶段及时发现协议存在的漏洞,可有效保证安全需求逻辑的正确性。本文在研究WSN安全协议安全问题的基础上,采用当前比较公认的CSP形式化分析方法,对WSN安全协议的形式化分析和验证进行研究。首先,给出了一种基于CSP建模层的PAT工具扩展方法,扩展CSP建模模块,使其适用于WSN安全协议的建模和分析,实现对WSN安全协议的快速形式化描述;其次,根据传感器节点的可移动性,扩展Dolev-Yao模型,使其适用于节点可移动的攻击者建模;然后,分析WSN安全协议的安全需求,提出一种线性时序逻辑(Linear Temporary Logic,LTL)刻画性质的方法;最后,通过两个案例分析说明CSP方法在WSN安全协议和WBAN安全认证协议分析过程中的可行性和正确性。
高悦翔[10]2013年在《电子商务安全协议的设计与形式化分析》文中进行了进一步梳理随着计算机网络的飞速发展,电子商务逐渐成为人们进行商务活动的新模式。电子商务安全协议是构建电子商务安全环境的基础,是保障电子商务顺利应用与发展的关键技术。电子商务安全协议是以密码学为基础的消息交换协议,参与者采取的一系列步骤去完成某一任务,其目的是在网络信道不可靠的情况下,确保通信安全以及传输数据的安全。电子商务安全协议除了需满足传统安全协议所需满足的认证性、保密性和完整性外,还需满足可追究性、公平性、时限性及匿名性等安全属性。因此电子商务安全协议的设计与分析面临着诸多困难和挑战,也成为了信息安全领域中的一个重要课题,具有重要的理论意义和现实应用价值。本文主要围绕电子商务安全协议的设计以及形式化分析技术展开研究,取得了些研究成果。对电子商务安全协议的基本概念、分类及其安全属性进行了综述和分析,对电子商务安全协议安全性设计及形式化分析方法进行综述性研究,讨论各种方法的优缺点及其存在的问题。指出了一个认证电子邮件协议在可追究性和公平性上存在的安全缺陷,在此基础上提出了一种基于在线第叁方的认证电子邮件协议,以满足认证电子邮件的一般安全特性。利用扩展Kailar逻辑对该协议进行分析,说明该协议满足不可否认性及公平性,并具有抗篡改、重放等攻击、及第叁方无法获得邮件内容等优点。采用组合协议分析方法及PCL逻辑分析了ECS2协议的弱公平性。指出了ZZW协议存在不满足保密性、可追究性和公平性的安全缺陷,并提出了改进方案。提出一种结合组合协议分析以及Kailar逻辑的分析思路,用于分析基于离线第叁方的电子商务安全协议的可追究性及公平性,并分析了改进后的ZZW协议,证明了该协议能够弥补原协议的安全隐患。针对移动环境中网络及计算条件受限的情况,在考虑有效性和支付效率的基础上,设计了一个适应于移动环境的公平移动支付协议。该协议由认证、支付、恢复、结算四个子协议构成。在认证协议中通过基于Hash函数的动态ID机制满足了双向认证、有限的匿名性和不可追踪性,并获取不可伪造性的、可重用的支付证书。在支付过程中基于变色龙Hash函数和双Hash链,实现了交易的匿名性、可追究性和公平性。最后利用Kailar逻辑对协议的可追究性和公平性进行了形式化分析,结果表明,协议在保持较高执行效率的同时能满足可追究性和公平性,适用于在移动环境以及类似的通信、计算条件受限的环境中使用。针对一般信念逻辑难于分析乐观公平交换协议的公平性和时限性的现状,将乐观公平交换协议定义为类似于Kripke结构的状态转换系统,对扩展Kailar逻辑增加了时间限定条件及状态转换分析。在分析不可否认证据有效性的基础上,通过考察主体认知及信仰的转换过程,达到分析乐观公平交换协议的公平性和时限性的目的。同时,对一个典型的乐观公平交换协议进行了分析,发现了该协议存在的两个安全缺陷,并给出了改进方案。指出了一个典型的多方认证邮件协议存在不满足公平性、可追究性以及个别不诚实参与方行为会导致整个协议执行失败等安全隐患。基于签密方案,对该协议进行了改进,并利用Kailar逻辑对改进后的协议的安全属性进行了分析。研究结果表明,该协议能够满足保密性、不可否认性及公平性,并具有抗篡改、重放、合谋等攻击的特点。本文的研究工作对于电子商务安全协议的设计以及形式化分析技术有一定的理论和实用意义,同时对于提高电子商务活动的安全性也具有一定的价值。
参考文献：
[1]. 复杂安全协议的形式化分析、设计与验证研究[D]. 陈铁明. 浙江工业大学. 2004
[2]. 复杂安全协议的建模与验证[D]. 周倜. 国防科学技术大学. 2008
[3]. 3G的安全增强研究及认证与密钥协商协议设计[D]. 边瑞昭. 解放军信息工程大学. 2007
[4]. 安全协议形式化验证方法研究[D]. 王强. 国防科学技术大学. 2012
[5]. 安全协议形式化分析理论与应用研究[D]. 鲁来凤. 西安电子科技大学. 2012
[6]. 形式化验证安全协议Java代码的安全性[D]. 汪卫. 中南民族大学. 2012
[7]. 可信信道协议的设计与形式化验证[D]. 左向晖. 北京交通大学. 2011
[8]. 网络协议安全性分析中的逻辑化方法研究[D]. 石曙东. 华中科技大学. 2009
[9]. 基于CSP模型检测的无线传感网安全协议形式化验证[D]. 虞震波. 浙江工业大学. 2015
[10]. 电子商务安全协议的设计与形式化分析[D]. 高悦翔. 西南交通大学. 2013
标签：互联网技术论文; 安全协议论文; 逻辑模型论文; 形式化方法论文; 逻辑框架论文; 关系逻辑论文; 电子商务分析论文; 信息安全论文; 建模软件论文;