Constant-round zero-knowledge proofs of knowledge with strict polynomial-time extractors for NP

Barak and Lindell showed that there exist constant-round zero-knowledge arguments of knowledge with strict polynomial-time extractors.This leaves the open problem of whether it is possible to obtain an analogous result regarding constant-round zero-knowledge proofs of knowledge for NP.This paper focuses on this problem and gives a positive answer by presenting a construction of constant-round zero-knowledge proofs of knowledge with strict polynomial-time extractors for NP.     

一种低运算量Ad-hoc网络匿名路由协议

Ad-hoc网络节点运算能力差,能量有限且移动速度高,而公钥运算量大,能耗高,运算周期长,所以公钥运算不适合于Ad-ho。网络。已提出的匿名路由协议却含有大量的公钥运算。为了降低公钥运算量,将双线性对和零知识证明应用于匿名路由协议中,提出一种新的匿名路由协议—低运算量的Ad-hoc网络匿名路由协议,该协议大幅降低了公钥运算量。实验结果表明,该协议建立匿名路由所消耗的能量少,时延低。     

Equational tree transformations

We define an equational relation as the union of some components of the least solution of a system of equations of tree transformations in a pair of algebras. We focus on equational tree transformations which are equational relations obtained by considering the least solutions of such systems in pairs of term algebras. We characterize equational tree transformations in terms of tree transformations defined by different bimorphisms. To demonstrate the robustness of equational tree transformations, we give equational definitions of some well-known tree transformation classes for which bimorphism characterizations also exist. These are the class of alphabetic tree transformations, the class of linear and nondeleting extended top-down tree transformations, and the class of bottom-up tree transformations and its linear and linear and nondeleting subclasses. Finally, we prove that a relation is equational if and only if it is the morphic image of an equational tree transformation.     

Algebraic proofs over noncommutative formulas

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege, yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analog of Frege proofs, different from that given in Buss et al. (1997) and Grigoriev and Hirsch (2003). We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short). Given some fixed linear order on variables, an arithmetic formula is ordered if for each of its product gates the left subformula contains only variables that are less-than or equal, according to the linear order, than the variables in the right subformula of the gate. We show that PC over ordered formulas (when the base field is of zero characteristic) is strictly stronger than resolution, polynomial calculus and polynomial calculus with resolution (PCR), and admits polynomial-size refutations for the pigeonhole principle and Tseitin?s formulas. We conclude by proposing an approach for establishing lower bounds on PC over ordered formulas proofs, and related systems, based on properties of lower bounds on noncommutative formulas (Nisan, 1991).The motivation behind this work is developing techniques incorporating rank arguments (similar to those used in arithmetic circuit complexity) for establishing lower bounds on propositional proofs.     

A non-interactive deniable authentication scheme based on designated verifier proofs

A deniable authentication protocol enables a receiver to identify the source of the given messages but unable to prove to a third party the identity of the sender. In recent years, several non-interactive deniable authentication schemes have been proposed in order to enhance efficiency. In this paper, we propose a security model for non-interactive deniable authentication schemes. Then a non-interactive deniable authentication scheme is presented based on designated verifier proofs. Furthermore, we prove the security of our scheme under the DDH assumption.     

An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps

This paper presents a completely formalized proof of a discrete form of the Jordan Curve Theorem. It is based on a hypermap model of planar subdivisions, formal specifications and proofs assisted by the Coq system. Fundamental properties are proven by structural or noetherian induction: Genus Theorem, Euler Formula, constructive planarity criteria. A notion of ring of faces is inductively defined and a Jordan Curve Theorem is stated and proven for any planar hypermap. This research is supported by the “white” project GALAPAGOS, French ANR, 2007.     

On Process Equivalence = Equation Solving in CCS

Unique Fixpoint Induction (UFI) is the chief inference rule to prove the equivalence of recursive processes in the Calculus of Communicating Systems (CCS) (Milner 1989). It plays a major role in the equational approach to verification. Equational verification is of special interest as it offers theoretical advantages in the analysis of systems that communicate values, have infinite state space or show parameterised behaviour. We call these kinds of systems VIPSs. VIPSs is the acronym of Value-passing, Infinite-State and Parameterised Systems. Automating the application of UFI in the context of VIPSs has been neglected. This is both because many VIPSs are given in terms of recursive function symbols, making it necessary to carefully apply induction rules other than UFI, and because proving that one VIPS process constitutes a fixpoint of another involves computing a process substitution, mapping states of one process to states of the other, that often is not obvious. Hence, VIPS verification is usually turned into equation solving (Lin 1995a). Existing tools for this proof task, such as VPAM (Lin 1993), are highly interactive. We introduce a method that automates the use of UFI. The method uses middle-out reasoning (Bundy et al. 1990a) and, so, is able to apply the rule even without elaborating the details of the application. The method introduces meta-variables to represent those bits of the processes’ state space that, at application time, were not known, hence, changing from equation verification to equation solving. Adding this method to the equation plan developed by Monroy et al. (Autom Softw Eng 7(3):263–304, 2000a), we have implemented an automatic verification planner. This planner increases the number of verification problems that can be dealt with fully automatically, thus improving upon the current degree of automation in the field. Partially supported by grants CONACyT-47557-Y and ITESM CCEM-0302-05. Partially supported by EPSRC GR/L/11724.     

ALOGTIME and a conjecture of S.A. Cook

Usingsequential, machine-independent characterization of theparallel complexity classesAC ^k andNC ^k , we establish the following conjecture of S.A. Cook. There is a free variable equational logicALV with the property thatif f, g are function symbols forALOGTIME computable functions for which f=g is provable inALV, then there are polynomial size Frege proofs for the infinite family {|f=g| _m ⁿ :n, m} of propositional tautologies. Here, the propositional formula |f=g| _m ⁿ expresses the equality off andg on inputs of length at mostn, provided that the function values are of length at mostm. We establish a related result with constant formula-depth polynomial size Frege proofs for a systemAV related to uniformAC ⁰ functions.Part of this research supported by NSF Grant # DCR-860615. Extended abstract of this paper appeared in theIEEE Proc. of Logic in Computer Science, Philadelphia (June 1990).     

Mathematical Induction in Otter-Lambda

Otter-lambda is Otter modified by adding code to implement an algorithm for lambda unification. Otter is a resolution-based, clause-language first-order prover that accumulates deduced clauses and uses strategies to control the deduction and retention of clauses. This is the first time that such a first-order prover has been combined in one program with a unification algorithm capable of instantiating variables to lambda terms to assist in the deductions. The resulting prover has all the advantages of the proof-search algorithm of Otter (speed, variety of inference rules, excellent handling of equality) and also the power of lambda unification. We illustrate how these capabilities work well together by using Otter-lambda to find proofs by mathematical induction. Lambda unification instantiates the induction schema to find a useful instance of induction, and then Otter's first-order reasoning can be used to carry out the base case and induction step. If necessary, induction can be used for those, too. We present and discuss a variety of examples of inductive proofs found by Otter-lambda: some in pure Peano arithmetic, some in Peano arithmetic with defined predicates, some in theories combining algebra and the natural numbers, some involving algebraic simplification (used in the induction step) by simplification code from MathXpert, and some involving list induction instead of numerical induction. These examples demonstrate the feasibility and usefulness of adding lambda unification to a first-order prover. Research supported by NSF grant number CCR-0204362.