27685496
An Open Framework for Remote Electronic Elections
We propose a framework for remote electronic elections with an independent, trustworthy authorization proxy. Unlike existing voting systems, voter authorization is separated from particular elections in our scheme, and is done through reusable credentials granted by the proxy. Moreover, different types of elections can fit in the framework, with different sets of legitimate voters and even different designs of voting and tabulation. We also define a cryptographic protocol for the credential generation and the election registration.
12359586
Verifying Anonymous Credential Systems in Applied Pi Calculus
Anonymous credentials are widely used to certify properties of a credential owner or to support the owner to demand valuable services, while hiding the user's identity at the same time. A credential system (a.k.a. pseudonym system) usually consists of multiple interactive procedures between users and organizations, including generating pseudonyms, issuing credentials and verifying credentials, which are required to meet various security properties. We propose a general symbolic model (based on the applied pi calculus) for anonymous credential systems and give formal definitions of a few important security properties, including pseudonym and credential unforgeability, credential safety, pseudonym untraceability. We specialize the general formalization and apply it to the verification of a concrete anonymous credential system proposed by Camenisch and Lysyanskaya. The analysis is done automatically with the tool ProVerif and several security properties have been verified.
35901095
The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmann's SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. We in particular define rules that justify directly the computational indistinguishability between programs and prove that these rules are sound with respect to the set-theoretic semantics, hence the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali's construction of pseudorandom generator.
7761771
Access control in peer-to-peer collaborative systems
As an emerging model of communication and computation, peer-to-peer networking represents a fully distributed, cooperative network design, and has recently gained significant acceptance. Peer groups share the properties of peer-to-peer overlay network, including full decentralization, symmetric abilities, and dynamism, which make security problems more complicated. In this paper, we propose a fine-grained and attribute-based access control framework for peer-to-peer systems. This design employs a novel policy model, which extends role-based trust management language RT to satisfy security requirements of peer groups. Intend for a pure decentralized model without centralized server, our framework presents distributed delegation authorization mechanism, which could avoid single point of failure. We also introduce our implementation experience.
27426921
Cryptographic logical relations
Using contextual equivalence (a.k.a. observational equivalence) to specify security properties is an important idea in the field of formal verification of cryptographic protocols. While contextual equivalence is difficult to prove directly, one is usually able to deduce it using the so-called logical relations in typed @l-calculi. We apply this technique to the cryptographic metalanguage-an extension of Moggi's computational @l-calculus, where we use Stark's model for name creation to explore the difficult aspect of dynamic key generation. The categorical construction of logical relations for monadic types (by Goubault-Larrecq et al.) then allows us to derive logical relations over the category Set^I. Although Set^I is a perfectly adequate model of dynamic key generation, it lacks in some aspects when we study relations between programs in the metalanguage. This leads us to an interesting exploration of what should be the proper category to consider. We show that, to define logical relations in the cryptographic metalanguage, a better choice of category is Set^I^^^-> that we proposed in [Y. Zhang, D. Nowak, Logical relations for dynamic name creation, in: Proceedings of the 17th International Workshop of Computer Science Logic and the 8th Kurt Godel Colloqium, CSL & KGL, in: Lecture Notes in Computer Science, vol. 2803, Springer-Verlag, 2003, pp. 575-588]. However, this category is still lacking in some subtler aspects and we propose a refined category Set^P^I^^^-> to fix the flaws, but our final choice is Set^I^x^I, which is equivalent to Set^P^I^^^->. We define the contextual equivalence based on Set^I^x^I and show that the cryptographic logical relation derived over Set^I^x^I is sound and can be used to verify protocols in practice.
9609952
A survivable routing algorithm with differentiated domain protection based on a virtual topology graph in multi-domain optical networks
In this paper, we propose a novel differentiated domain protection (DDP) scheme to address survivability in multi-domain optical networks. Survivable routing in multi-domain networks is a challenging algorithmic problem because it requires choosing links that provide adequate protection both between domains and within domains that may offer different protection services. To satisfy the survivability requirements of different domains, DDP considers differentiated protection schemes, i.e., dedicated protection, shared protection, or no protection in different domains. In order to respect the principle of transparent management in multiple domains, DDP abstracts a multi-domain optical network to a virtual topology graph (VTG) for solving routing between domains. Simulation results show that DDP, unlike traditional schemes, can provide trade-off between protection methods and also allows better resource utilization.
17285338
A reputation-chain trust model for the semantic Web
Trust plays a central role for efficient and secure interactions on the semantic Web. Nowadays, more and more research has focused on this topic. In this paper, we introduce RCSW, a reputation-chain trust model for the semantic Web. We illustrate the basic definitions and mechanisms of RCSW and present the algorithm to calculate trust ratings through the chain of the trust network. RCSW incorporates pairwise trust values and reliable factors of acquaintances and constructs an edge-weighted graph to calculate trust ratings. We also define classes of trust functions to allow users to individualize their trust calculation. Our proposed model can deal with trust management effectively and can quickly adapt to the changing environment.
29024953
Mixed diamond, hexagon, and cross search fast motion estimation algorithm for H.264
The block motion estimation process is a very time consuming part in the H.264 video coding standard and thus hinders its real-time applications. Therefore, a new fast block motion estimation algorithm is proposed in this paper. In this algorithm, it first determines the current block as a quasi-stationary, slow motion, or fast motion block. Then, according to the different motion types, different search patterns and strategies are intelligently employed. Experimental results demonstrate that the proposed algorithm has much less execution time than the existing FS, UMHexagonS, and EPZS algorithms, with about the same accuracy.