出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

自动定理证明：十年回顾

本文主要介绍近十年来定理证明器的发展情况,同时讨论了与自动定理证明相关的一些问题。     

一阶谓词演算定理机器证明的余式方法

本文将一阶谓词泻算的证明转化为代数族的计算，从而获得了代数化的Ｈｅｒｂｒａｎｄ过程，双通过一阶多项式间的求余运算，给出了余式方法并评理服它的完备性。同时，我们证明了归结原理是余式方法的一种特例。     

基于能力系统的应用证明研究

通过对可信计算及其主要功能“远端证明”的分析，提出“应用证明”的概念及原理，并说明支持应用证明所需的安全机制。分析现有主流操作系统所使用的保护结构和访问控制模型，说明应用证明在当前的主流操作系统上是无法实现的。通过对能力系统EROS进行改进，使其充分支持应用证明，并提高系统的安全性及可信性。     

关于归纳证明的探讨

归纳定理证明是一种难度较大且较有前途的一种自动定理证明方法。较早的归纳定理证明器是Boyer一Moore于1979年提出的BM证明器,BM证明器采用的是传统的结构归纳法,对所证公式中的每个函数项都根据其所谓归纳模板提出相应的归纳方案,然后对这个归纳方案进行分析、比较和整理,得出整个     

基于属性的自证实模型及其安全协议

针对可信环境下被验证方需要向验证方发送其软硬件基本配置信息来证明其完整性而产生的攻击问题,给出一种基于虚拟机技术的属性自证实（PSA）模型及其安全协议,并对协议进行安全性分析。首先通过在被验证平台上建立一个可信虚拟机,然后由该虚拟机实现对被验证平台上其他组件的度量,并可靠地报告代表当前平台运行环境的安全属性给验证方。自证实方式可以提高通信的安全性,并且减少维护独立可信第三方时所需的开销;使用基于属性的远程证明方式,能够提高被验证方的安全性;安全协议引入了TPM的不可迁移密钥特性来防止假冒攻击的发生。     

子弹证明:一种区块链中的隐私保护技术

区块链的隐私保护技术自2008年比特币问世以来就成为研究热点之一。加密货币如门罗币(Monero)、大零币(ZCash)、达世币(Dash)等都是成功应用各类隐私保护技术的明星货币,而在诸多的隐私保护技术之中,零知识证明技术能实现最好的匿名性,因此也成为隐私保护研究领域的焦点技术之一。论文对最新的子弹证明技术进行系统性和原理性的阐述分析,并与Zksnarks和Zk-starks两类前沿零知识证明技术进行对比。最后,对区块链中的零知识证明技术的发展方向进行展望。     

基于高阶逻辑的定理证明方法及其对策的应用

定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。     

基于自证明公钥和零知识证明的身份认证协议

在分析几种典型零知识身份认证协议的基础上,利用Girault自证明公钥原理、结合椭圆曲线公钥密码的优点提出一种基于自证明公钥和零知识证明的身份认证协议,并为协议增加了密钥协商功能。分析表明该方案具有较高的安全性,与同类方案相比,该方案对存储空间、网络通信量和计算开销的要求较低,有较高的效率。     

密码协议的秘密性证明

在Paulson的归纳方法基础上提出一种新的密码协议秘密性的证明方法，该方法在消息事件结构中引入会话标识符，给出协议满足秘密性的充要条件，大大简化了协议秘密性的证明，高效且适合机械化实现。     

一种可信终端运行环境远程证明方案

可信终端的远程证明无论是基于二进制的证明方案还是基于属性的证明方案,针对的均是终端的静态环境,反映的是终端的软件配置结构,并不能证明终端运行环境的真正可信.针对这一问题,提出了一种终端可信环境远程证明方案.针对静态环境,该方案考虑了满足可信平台规范的信任链以及相关软件配置的可信属性证明;针对动态环境,该方案考虑了终端行为的可信属性证明.并分别给出了信任链、平台软件配置和终端行为等属性证明的可信性判定策略和算法,以及终端运行环境远程证明的综合性判定策略和算法.另外,在Windows 平台上,设计和实现了该方案中的两个核心实体：证明代理和验证代理,并设计了证明代理和验证代理之间的通信协议.最后,介绍了该方案在Windows 平台上的一个典型应用案例以及证明代理在该应用实例中的性能开销.应用实例验证了该方案的可行性.     

一个出具证明编译器原型系统的实现

出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具,它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。     

一种基于属性证书的动态可信证明机制

基于可信计算的远程证明的方法中,二进制证明方法能反映系统平台当前配置的完整性状态,是动态的,但容易暴露隐私,而基于属性证书的证明将系统平台的配置信息隐藏,具有匿名性,但是静态的.将二进制方法嵌入到属性证书方法中,提出了一种动态属性可信证明(Dynamic Property Trusted Attestation DPTA)的协议.验证者通过模拟计算PCR值,并与证书中的PCR值进行比较,证明示证者的当前平台满足一定的安全属性,解决了暴露隐私和静态问题.实验表明这种证明方法能保护平台隐私,克服基于属性证书的静态特点,兼有实时性和保密性的特点.     

基于能力系统的应用证明研究

通过对可信计算及其主要功能“远端证明”的分析,提出“应用证明”的概念及原理,并说明支持应用证明所需的安全机制。分析现有主流操作系统所使用的保护结构和访问控制模型,说明应用证明在当前的主流操作系统上是无法实现的。通过对能力系统EROS进行改进,使其充分支持应用证明,并提高系统的安全性及可信性。     

机器证明的困难所在

机器证明是人工智能的一个重要课题,即用计算机来证明定理,亦称自动证明或定理的机械化证明,其基础是由 Hibert 在1930年奠定的,60多年来历程艰苦,困难在于传统逻辑、三段论、充分条件、同理可证、直觉思维的局限性。如果我们正视这些困难,利用专家系统,机器学习等技术,机器证明将进入一个崭新的局面。     

基于双重离散对数DAA协议的设计*

TCG 规范中的DAA(direct anonymous attestation)方案以CL 数字签名(Camenisch and Lysyanskaya signature scheme)为基础,结合了群签名和零知识证明等技术来实现直接匿名证明,其安全性是基于大数分解难解问题。随着计算机性能的提高和密码学的发展,基于大数分解难题问题很可能被攻击,相应的DAA方案也就变得不再安全,而基于椭圆曲线上的离散对数和素数域上的离散对数（双重离散对数）的算法可以使用较短的密钥,实现较高的安全性。正是基于双重离散对数     

Automatic and Hierarchical Verification for Concurrent Systems

Proving correctness of concurrent systems is quite difficult because of the high level of nondeterminism,especially in large and complex ones.AMC is a model checking system for verifying asynchronous concurrent systems by using branching time temporal logic.This paper introduces the techniques of the modelling approach,especially how to construct models for large concurrent systems with the concept of hierarchy,which has been proved to be effective and practical in verifying large systems without a large growth of cost.     

一类构造性几何不等式的机器证明

阐述了一个基于胞腔分解的不等式证明算法．据此算法编制的Maple通用程序能有效地处理含有根式的不等式型定理,对于Bottema等所著《几何不等式》一书中的大部分不等式定理的验证尤其高效．     

一种基于PCA的远程匿名证明改进方案

远程证明是可信计算的关键技术之一,可以验证平台身份和配置信息的可信性,而现有远程证明方案存在一定的缺陷。本文在分析现有基于匿名属性证书的远程匿名证明方案的基础上,提出了改进方案。针对原方案中存在的在匿名属性证书申请过程中未验证证书颁发实体的问题,对证书申请方案进行了改进,采用会话密钥对PCA签名,保证了证书颁发实体的真实性;针对远程证明协议存在恶意用户接入的问题,在改进方案中引入假名机制,即保证了用户身份的匿名性,又防止了具有不良历史记录用户的非法接入。     

相干命题逻辑自然推理系统NR的自动证明*

给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列。对系统NR的大部分定理证明取得了良好的效果,算法生成的演绎序列清晰可读,接近手工推理。