实例化空间:一种新的安全协议验证逻辑的语义模型

给出了一个称为“实例化空间（instantiation space）”的安全协议验证逻辑的语义模型．该语义模型是建立在一种自然的加密信息交换（cryptographical message exchange）模型上的．在此语义模型基础上，文章提出了一系列与安全属性相关的验证公理，由此可以证明它们在此语义模型下的正确性．更重要的是，在此语义下的公理集在算法上是完全可以实现的，其对应的工具SPV（Security Protocol Verifier）已经开发成功，并且可以验证复杂的协议．在这套安全协议验证模型理论下，可以很方便地处理包括公钥、私钥、共享密钥和Hash函数组成的复杂信息格式．而且，在此语义基础上的公理集是纯命题逻辑的，因此所需要的验证目标可以很方便地转化成可满足性问题（SAT），从而可以利用工业上快速高效的SAT求解器实现．     

SET证书申请协议在SPV下的自动化验证及改进

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.     

数学形态学在图像处理中的应用与展望

阐述数学形态学的产生及其与图像处理的结合过程,讨论其由二值形态学、灰度形态学、软形态学到模糊形态学、模糊软形态学、形态小波的发展,分析了数学形态学在图像处理中的发展趋势并对其应用前景进行探讨与展望.     

一种规约于可满足性问题(SAT)的知识推理算法

传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[1]中,给出了一个实用而紧致的知识的语义模型——知识结构(knowledge struc- ture),并给出相应的利用BDD(Binary Decision Diagram)的符号化计算方法,实验表明这种基于BDD的算法比传统方法有很大的优势,但这种基于BDD的方法在计算规模大的例子时仍存在明显的组合爆炸。文章在知识结构(knowledge structure)的语义基础上,通过挖掘知识结构语义中各元素的关系,把知识的计算规约于可满足性问题(SAT),因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD。实验结果证实了这种方法的有效性。     

基于BDD的增量启发式搜索

增量搜索是一种利用先前的搜索信息提高本次搜索效率的方法,通常可以用来解决动态环境下的重规划问题.在人工智能领域,一些实时系统常常需要根据外界环境的变化不断修正自身,这样就会产生一系列变化较小的相似问题,此时应用增量搜索将会非常有效.另外,基于BDD(binary decision diagram)的启发式搜索,结合了基于BDD的搜索和启发式搜索这两种方法的优点.它既用BDD这一紧凑的数据结构来表示系统的状态空间,又通过使用启发信息来进一步压缩搜索树的大小.在介绍基于BDD的启发式搜索和增量搜索之后,结合这两种方法给出了基于BDD的增量启发式搜索算法--BDDRPA*.大量的实验结果表明,BDDRPA*算法是非常有效的,它可以被广泛地应用到智能规划、移动机器人问题等领域中.