Cryptographic and Physical Zero-Knowledge Proof Systems for Solutions of Sudoku Puzzles

We consider cryptographic and physical zero-knowledge proof schemes for Sudoku, a popular combinatorial puzzle. We discuss methods that allow one party, the prover, to convince another party, the verifier, that the prover has solved a Sudoku puzzle, without revealing the solution to the verifier. The question of interest is how a prover can show: (i) that there is a solution to the given puzzle, and (ii) that he knows the solution, while not giving away any information about the solution to the verifier. In this paper we consider several protocols that achieve these goals. Broadly speaking, the protocols are either cryptographic or physical. By a cryptographic protocol we mean one in the usual model found in the foundations of cryptography literature. In this model, two machines exchange messages, and the security of the protocol relies on computational hardness. By a physical protocol we mean one that is implementable by humans using common objects, and preferably without the aid of computers. In particular, our physical protocols utilize items such as scratch-off cards, similar to those used in lotteries, or even just simple playing cards. The cryptographic protocols are direct and efficient, and do not involve a reduction to other problems. The physical protocols are meant to be understood by “lay-people” and implementable without the use of computers. Research of R. Gradwohl was supported by US-Israel Binational Science Foundation Grant 2002246. Research of M. Naor was supported in part by a grant from the Israel Science Foundation. Research of B. Pinkas was supported in part by the Israel Science Foundation (grant number 860/06). Research of G.N. Rothblum was supported by NSF grant CNS-0430450 and NSF grant CFF-0635297.     

自计票电子投票方案的分析与改进

Kiayias和Yung首次提出了自计票电子投票方案,使得小规模电子选举不需要任何可信第三方参与,选举的行为公开可验证,有力地保证了选举的秘密性,Groth在此基础上做了改进,使得方案更简洁、高效;然而Groth方案仍只用于双候选人选举,且不允许两个选民同时投票.简要介绍并分析了Groth方案,针对上述两点不足给出改进建议,使新方案更高效且用于多候选人选举.     

共享的安全群签名方案

可在不同群组间共享的、满足安全性要求的、有效的群签名方案是近来群签名研究的一个重要方面。基于离散对数的群签名方案允许不同群组可以共享系统公开参数,使用零知识证明的主要思想,充分保证了方案的安全性和有效性。共享方案可为不同群组间建立一个统一的安全的体系结构提供理论支持,有利于群签名方案的应用和管理。     

基于Brands体制的强不可伪造电子货币系统

针对Brands电子支付体制在电子货币被重复使用时所存在的安全漏洞,即获取同一电子货币不同支付信息的攻击者可以以用户的身份重复使用该货币,通过引入知识的零知识证明以及概率加密等工具,提出了一个新的公正电子货币系统的设计方案,实现了在货币被重复使用时的强不可伪造性。同时该系统即使在银行或用户密钥被泄露时,仍然可以保证整个系统的安全性。其安全性基于随机Oracle模型和限制性盲签名假设。     

一种简单的无收据电子投票系统

在现有的电子投票系统中,无收据行（receipt—freeness）与可验证性（verifiability）是电子投票协议中一对十分重要而又矛盾的属性。无收据性要求任何人不能得到或生成能证明选票内容的证据,其往往以牺牲可验证性为代价;可验证性提供给对选票及选举结果的验证,提供给投票人与选票的某种联系,这又经常被用来作为证明选票的收据。选择常用的Mix-net模式,利用TRR和1-out—of—L加密证据,re—encryption ELGamal同时实现无收据型与实现可验证性,避免了在投票人与管理机构有特殊的信道假设,减少了系统的通信代价。     

Dependability in open proof software with hardware virtualization—The railway control systems perspective

Using the openETCS initiative as a starting point, we describe how open software can be applied in combination with platform-specific, potentially closed-source extensions, in the development, verification, validation and certification of safety-critical railway control systems. To achieve certification credit for safety-critical system developments, evidence about numerous development, verification and validation artifacts has to be provided. Our focus is therefore on open models, and a model-driven development approach ensures that a large portion of the artifacts is automatically generated from the model. This strategy is illustrated by means of the ETCS standard, as far as applicable to the ETCS on-board computer managing train control and train protection. We show that a domain-specific language is suitable to cover all modeling aspects for this computer, starting from the ETCS standard itself and ending at supplier-specific adaptations extending the re-usable core model in concrete developments. In order to re-use certification credits once achieved for the re-usable core model, we suggest virtualization of run-time environments, so that suppliers can embed re-usable core components as binary code into their ETCS target platforms. A detailed analysis is provided, indicating how future changes in the standard and project-specific adaptations, extensions and restrictions, can be accounted for in a new ETCS development, while minimizing the re-certification effort. It is shown for all phases of the development life cycle how the peer-reviewing capacity of the openETCS community may contribute to the correctness of the phases’ outputs, thereby increasing overall system dependability, with special emphasis on safety and security.     

云计算下的数据存储安全可证明性综述

云计算的数据服务外包可以减少数据所有者本地的存储和维护压力,然而用户会因此失去对数据可靠性和安全的物理控制。于是如何确保云中数据的安全就成为了非常有挑战性的任务和难题。在全面研究云计算数据存储安全现有成果的基础上,介绍了云计算数据存储的基本架构,并从可检索证明和可证明数据拥有两个角度分析了相关研究方案的发展,从公共认证、同态认证、数据动态化、隐私保护、批审计和多服务器环境得方面讨论了协议的功能设计,并且列表进行了功能和开销对比,在此基础上提出了一个比较完备的云计算环境下的协议框架。最后总结并阐述了后续工作。     

Unification under associativity and idempotence is of type nullary

It is shown, that there exist a unification problem〈s=t〉 _AI , for which the set of solutions under associativity and idempotence is not empty. But , the complete and minimal subset of this set of solutions does not exist, i.e.A+I is of type nullary. This is the first known standard first order theory with this unpleasant feature. This work is supported by the Deutsche Forschungsgemeinschaft, National Research Schema ‘Artificial Intelligence and Knowledge Based Systems’, SFB 314.     

Recursive 4SID algorithms using gradient type subspace tracking

Sometimes we obtain some prior information about a system to be identified, e.g., the order, model structure etc. In this paper, we consider the case where the order of a MIMO system to be identified is a priori known. Recursive subspace state-space system identification algorithms presented here are based on the gradient type subspace tracking method used in the array signal processing. The algorithms enable us to estimate directly the subspace spanned by the column vectors of the extended observability matrix of the system to be identified without performing the singular value decomposition. Also, a new convergence proof of the gradient type subspace tracking is given in this paper. Under the condition of a step size between 0 and 1, we prove the convergence property of the recursive equation of the gradient type subspace tracking. A numerical example illustrates that our algorithm is more robust with respect to the choice of the initial values than the corresponding PAST one.