Strongly simulation-extractable leakage-resilient NIZK

This paper defines strongly simulation-extractable (sSE) leakage resiliency (LR), which is a new notion for non-interactive zero-knowledge (NIZK) proof system. For an sSE-NIZK proof system, there exists a probabilistic polynomial-time extractor that can always extract a correct witness from any valid proof generated by the adversary, who can obtain proofs of true statements previously given by the simulator. The proof generated by the adversary may depend on a statement–tag pair which has already been used by the simulator. Furthermore, if the adversary can also learn leakage on witnesses and randomness which can explain the proofs generated by the simulator, then the sSE-NIZK proof system is said to satisfy the property of LR. In ASIACRYPT 2010, Dodis, Haralambiev, López-Alt, and Wichs proposed the definitions of true simulation-extractable (tSE) NIZK proof system and sSE-NIZK proof system and gave their constructions. The tSE-NIZK proof system is the same as the sSE-NIZK proof system except that the proof generated by the adversary cannot depend on a statement–tag pair which was used by the simulator. As an extension of the tSE-NIZK proof system, Garg, Jain, and Sahai defined a new notion for NIZK proof system called tSE-LR in CRYPTO 2011 and provided the construction of tSE-LR-NIZK proof system. We extend the notion of tSE-LR-NIZK proof system and construct it by improving the construction of tSE-LR-NIZK proof system. An sSE-LR-NIZK proof system is applicable to construct a fully leakage-resilient signature scheme which is strongly existentially unforgeable, while a tSE-LR-NIZK proof system is applicable to construct one which just satisfies the weak existentially unforgeability. Although there has already been a great deal of research proposed for cryptographic primitives in the leakage models, as far as we know, this is the first fully leakage-resilient signature scheme that is strongly existentially unforgeable.     

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.     

一种构造代码安全性证明的方法

提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.     

终止证明方法在形式化建模中的应用

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.     

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.     

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.”     

Translation of resolution proofs into short first-order proofs without choice axioms

We present a way of transforming a resolution-style proof containing Skolemization into a natural deduction proof without Skolemization. The size of the proof increases only moderately (polynomially). This makes it possible to translate the output of a resolution theorem prover into a purely first-order proof that is moderate in size.     

On the Comparison of Proof Planning Systems: , Ωmega and IsaPlanner

We present a framework for describing proof planners. This framework is based around a decomposition of proof planners into planning states, proof language, proof plans, proof methods, proof revision, proof control and planning algorithms.We use this framework to motivate the comparison of three recent proof planning systems, λCLaM, Ωmega and IsaPlanner, and demonstrate how the framework allows us to discuss and illustrate both their similarities and differences in a consistent fashion. This analysis reveals that proof control and the use of contextual information in planning states are key areas in need of further investigation.     

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

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