基于后量子假设的高效范围证明方案

作为零知识证明的一种特殊应用,范围证明技术广泛地应用于密码货币、电子投票、匿名凭证等多个场景。这项技术使得证明者能够向验证者证明某一秘密整数属于一个给定的连续整数区间,除此之外不泄露其他任何信息。大部分现有的范围证明方案都是针对基于经典的数论假设的承诺方案构造的,在量子攻击下不能保证安全性。本文针对串承诺方案,提出了一种构造后量子范围证明方案的新思路,并分别基于Exact Learning Parity with Noise（xLPN）,Small Integer Solution（SIS）和Learning with Errors （LWE）等假设,给出了三类具体的范围证明方案。此外,文章还提出了一个批承诺方案,并针对该批承诺构造了适用于同时处理多个消息的批处理范围证明方案。该批处理范围证明方案中,对于多个秘密值分别属于不同整数区间的情况,证明者只需要产生一个证明。与对多个消息逐一生成证明的处理方式相比,批处理的方式有效地节约了生成证明过程中需要的随机数个数,明显地降低了双方的通信量和计算量。     

抗量子计算的多变量盲签名方案

盲签名是一种特殊的数字签名,可广泛应用于各种匿名场合.目前,大多数盲签名的安全性主要基于大整数分解问题或离散对数问题的难解性.然而,实用量子计算机的即将诞生会使得传统的盲签名不再安全,而且量子算法的出现对传统的盲签名亦提出了挑战.因此,构造能够防御量子计算攻击的盲签名方案具有重要的意义.多变量公钥密码是后量子密码的主要候选者之一.在多变量公钥密码和盲签名的理论基础上,设计了一种新颖的多变量公钥密码体制下的盲签名方案.该密码方案借助另一非线性可逆变换L：F^r→F^r将签名的公私钥分离,减少了公私钥之间的线性关系,提高了盲签名的安全性.分析表明：该密码方案不仅具有盲性、不可伪造性和不可追踪性,而且还具有计算复杂度低及抗量子计算攻击的优点.     

基于k-Lin假设的同态加密方案

作为数字货币的底层核心技术之一,区块链随着数字货币的快速发展而受到了广泛关注.由于区块链具有去中心化、防篡改、可追溯等性质,如今越来越多的企业和个人用户选择利用区块链技术来实现数据的传输和记录.区块链公开透明的特性,一方面充分保证了数据的可用性;但另一方面,又给用户的隐私信息带来了严重威胁.为了同时兼顾用户数据的机密性和可用性,同态加密常常被用到区块链的安全解决方案之中.然而,现实应用对于所部署的同态加密方案的安全强度要求也很可能会随着时间推移而有所变化.考虑到区块链应用场景的复杂多样性和分布式特点,同态加密方案一旦部署下去,之后,当随着时间推移需要调整安全性强度时,相应的工作量将会非常繁重.此外,在区块链的现实应用中,考虑到监管方面的需求,很多情况下（尤其是针对某些群组成员发布和传输的数据）需要允许某可信第三方（如监管方）能够对链上的相应密文数据进行解密.若采用传统的同态加密方案对数据进行加密,可信第三方需要存储所有用户的私钥,这将给密钥管理和存储带来巨大压力.针对当前的区块链应用场景和安全需求,提出了一个基于ZN2*（N=pq）上的判定性k-Lin假设的加法同态加密方案.该方案不仅在标准模型下能够满足IND-CCA1安全性,还具有3个特殊优势：（i）可以通过对参数k的调控细粒度地调节加密方案的安全性强度;（ii）加密方案具有双解密机制：存在两种私钥,一种由用户本人持有,另一种由可信第三方持有,其中,可信第三方的私钥可用于该加密体制所有用户的密文解密;（iii）加密方案可以极为便利地退化为IND-CPA安全的公钥加密方案,退化后的方案不仅其公私钥长度和密文长度变得更短,而且同样具有加法同态性和双解密机制.     

具有较短公钥的批处理整数上的全同态加密

Coron等人将批处理技术应用在整数上的全同态加密方案,可以在一个密文中同态地处理和加密一个明文向量,提高了原方案的效率,但它的公钥尺寸为O~（λ⁸）。为了减小该方案的公钥尺寸,结合公钥元素的二次形式与密文压缩技术,提出一种批处理整数上全同态加密算法的改进方案,改进后方案的公钥尺寸为O~（λ^5.5）,具有较小的公钥尺寸,并证明了该方案语义安全。     

基于比特承诺的计算安全量子密码协议

比特承诺是重要的密码学元素,在复杂密码协议设计（如：零知识证明）中扮演着重要角色．Mayers,Lo和Chau分别独立证明了所有无条件安全的量子比特承诺方案都是不安全的,即著名的Mayers-Lo-Chau不可行定理．但这并不排除存在计算安全的量子比特承诺．2000年,Dumais等人给出了一个基于计算假设的量子单向置换可以用于构造计算安全的比特承诺方案．利用纠错码的方法,把量子比特承诺扩展成量子多比特承诺方案,并证明了所给方案的隐蔽性质和约束性质．以比特承诺方案为基础,给出了量子数字签名和量子加密认证方案的设计方法,并给出了协议的安全性证明．     

一类有限域丢番图方程的解及其应用

对一类有限域线性丢番图方程c≡x+by(mod N)进行了研究,求出了其通解及域中有效解的对数,并证明其能将部分曲线密码方案求解用户私钥的计算量降低为N/z, z为子群<-b>的最小非零元.指出了5个应用该类型方程曲线密码方案,最后以一个环Z_n上广义圆锥曲线多重数字签名方案私钥的求解为例进行说明.     

不需要可信任方的门限不可否认签名方案

在1992年澳大利亚密码会议上, Harn and Yang 第一次提出了(t,n)门限不可否认签名的概念.其中,只有成员个数不少于t的子集才能代表群体产生、确认和否认签名.随后,一些研究者又提出了几个方案,但这些方案都是不安全的.因此,到目前为止,怎样设计一个安全的(t,n)门限不可否认签名方案仍然是个公开问题.提出了一个基于离散对数密码系统的(t,n)门限不可否认签名方案.该方案不仅安全、高效,而且不需要可信任方.另外,方案还具有一个很好的性质,即成员的诚实性是可以验证的.这是由于在分发密钥时,采用了Schoenmakers在1999年美洲密码会议上提出的可公开验证秘密共享方案和两个用来提供正确性证据的离散对数恒等式协议.     

关于并发系统分支互模拟关系发散性保持的研究

带发散性说明的分支互模拟是van Glabbeek和Weijland提出的一个概念,并被用来定义等价关系.该等价关系应该是最弱的一个发散性保持的并且满足分支互模拟性质的等价关系.然而在概念提出时并没有提供这些重要性质的证明,并且我们认为在原定义的基础上这个证明是不显然的.本文通过co-induction的手段利用染色迹的概念定义了着色完全迹等价,并证明该等价关系是最弱的一个保持发散的并且满足分支互模拟性质的等价关系.然后我们证明了着色完全迹等价关系和≈_b^△是相同的,因而补充了van Glabbeek和Weijland的工作,即证明了≈_b^△是最弱的一个保持发散的并且是满足分支互模拟性质的等价关系.     

可行的证明整数是Blum数的零知识证明系统

Blum数是形如pk11qk21(p1和q1是模4余3的不同素数,且k1和k2是奇整数)的整数.目前,该类整数在密码学领域中得到了广泛的应用.尽管证明一个秘密整数是Blum整数的零知识证明系统已经存在,但是,怎样构造一个证明秘密整数是具有p1q1形式的Blum整数的零知识证明系统是未知的.基于Σ-协议,构造了证明秘密整数是具有p1q1形式的Blum整数的零知识证明系统,而且,也构造了证明秘密整数是具有pk11qk21(其中k1和k2至少有一个大于1)形式的Blum整数的零知识证明系统.     

具有短密文的多身份全同态加密构造框架

类似于多密钥全同态加密（Multi-key Fully Homomorphic Encryption,MFHE）,多身份全同态加密（Multi-id Identity-basedFully Homomorphic Encryption,MIBFHE）允许对不同用户的密文进行关于任意函数的同态计算,且后者因具有加密密钥易获取、密钥托管和密钥撤销易实现等特点,具有更深远的应用前景。
Canetti等人在PKC 2017上给出了一个框架,可将身份加密方案（Identity-based Encryption,IBE）和MFHE方案转换成MIBFHE方案。若用基于DLWE假设的IBE方案和Brakerski与Perlman的全动态^①MFHE方案（以下简称BP方案）,可得到全动态的MIBFHE方案,但密文规模较大,为O（n⁵log⁵q）,这里n,q是DLWE假设的参数,且紧致性相比于MFHE方案变弱。因密文规模是影响通信效率的主要因素,本文构造了一个密文规模较小和紧致性较强的MIBFHE方案框架,且仅用了MFHE这一个构件,然后用BP方案去实例化,得到了全动态的、选择性安全的MIBFHE方案,其密文规模为O（nlogq）.     

Memorizable interactive proof and zero-knowledge proof systems

Interactive proof and zero-knowledge proof systems are two important concepts in cryptography and complexity theory. In the past two decades, a great number of interactive proof and zero-knowledge proof protocols have been designed and applied in practice. In this paper, a simple memorizable zero-knowledge protocol is proposed for graph non-isomorphism problem, based on the memorizable interactive proof system,which is extended from the original definition of interactive proof and is more applicable in reality.     

A Comparison of Mizar and Isar

The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also differs in many other respects from most current systems. John Harrison has shown that one can have a Mizar mode on top of a tactical prover, allowing one to combine a mathematical proof language with other styles of proof checking. Currently the only fully developed Mizar mode in this style is the Isar proof language for the Isabelle theorem prover. In fact the Isar language has become the official input language to the Isabelle system, even though many users still use its low-level tactical part only. In this paper we compare Mizar and Isar. A small example, Euclid's proof of the existence of infinitely many primes, is shown in both systems. We also include slightly higher-level views of formal proof sketches. Moreover, a list of differences between Mizar and Isar is presented, highlighting the strengths of both systems from the perspective of end-users. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system.     

济钢105000Nm3/h空压机防喘振控制设计及应用

介绍了空压机的防喘振控制功能的设计与应用。防喘振控制是空压机整个控制系统中核心控制部分，控制复杂，精度高，本设计思路也适用于压缩机系统自动控制的设计与实现。     

Using hints to increase the effectiveness of an automated reasoning program: Case studies

In this article we consider the use of hints to help guide the search for a proof. Under the hints strategy, the value of a generated clause is determined, in part, by whether or not the clause subsumes or is subsumed by a user-supplied hint clause. We have implemented the hints strategy and have experimented with it extensively. We summarize our experiences for a variety of reasoning tasks, including proof checking, proof completion, and proof finding. We conclude that the hints strategy has value beyond simply “giving the proof to find the proof.”     

An Introduction to IN CAPS System

INCAPS，a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System,The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program‘s correctness which are supported respectively by the mechanized logics-FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system:the rules,implementation,tactics,forward proof and backward proof.It also gives several typical examples for demonstration of INCAPS‘ working principle.The achievement to data in that we have now accomplished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.     

An Integrated Approach to High Integrity Software Verification

Using automated reasoning techniques, we tackle the niche activity of proving that a program is free from run-time exceptions. Such a property is particularly valuable in high integrity software, for example, safety- or security-critical applications. The context for our work is the SPARK Approach for the development of high integrity software. The SPARK Approach provides a significant degree of automation in proving exception freedom. Where this automation fails, however, the programmer is burdened with the task of interactively constructing a proof and possibly also having to supply auxiliary program annotations. We minimize this burden by increasing the automation, through an integration of proof planning and a program analysis oracle. We advocate a ‘cooperative’ integration, where proof-failure analysis directly constrains the search for auxiliary program annotations. The approach has been successfully tested on industrial data.     

Autarkic Computations in Formal Proofs

Formal proofs in mathematics and computer science are being studied because these objects can be verified by a very simple computer program. An important open problem is whether these formal proofs can be generated with an effort not much greater than writing a mathematical paper in, say, LATEX. Modern systems for proof development make the formalization of reasoning relatively easy. However, formalizing computations in such a manner that the results can be used in formal proofs is not immediate. In this paper we show how to obtain formal proofs of statements such as Prime(61) in the context of Peano arithmetic or (x+1)(x+1)=x ²+2x+1 in the context of rings. We hope that the method will help bridge the gap between the efficient systems of computer algebra and the reliable systems of proof development.     

Proof planning for strategy development

Proof planning extends the tactic-based theorem proving paradigm through the explicit representation of proof strategies. We see three key benefits to the proof planning approach to the development of proof strategies: flexibility, re-usability and synergy. Here we demonstrate these benefits in terms of reasoning about imperative programs where we reuse strategies developed previously for proof by mathematical induction. In particular, we focus upon strategies for automating the discovery of loop invariants. Our approach tightly couples the discovery of invariants with the process of patching proof strategy failures. This revised version was published online in June 2006 with corrections to the Cover Date.     

Existence of 3-round zero-knowledge proof systems for NP

This paper considers the existence of 3-round zero-knowledge proof systems for NP. Whether there exist 3-round non-black-box zero-knowledge proof systems for NP language is an open problem. By introducing a new interactive proof model, we construct a 3-round zero-knowledge proof system for graph 3-coloring under standard assumptions. Our protocol is a non-black-box zero-knowledge proof because we adopt a special strategy to prove the zero-knowledge property. Consequently, our construction shows the existence of 3-round non-black-box zero-knowledge proof for all languages in NP under the DDH assumption.