Internet services collect lots of information that users deem highly sensitive such as the browsing history and email addresses, often without users noticing this conduct. The collected information is used for personalizing services and it is monetized, e.g., in the form of targeted advertisements. Realizing modern web services that maintain their functionality and satisfy the seemingly conflicting properties of trustworthiness and privacy is challenging: in a social network, how to enforce that only friends can post comments, if users are unwilling to reveal their identity? in online behavioral advertising, how to serve personalized ads, if users insist on keeping their interests private? In this thesis, we propose techniques for the trustworthy and privacy-preserving processing of personal information. First, we present an API for the trustworthy and privacy-preserving release of personal information. The API enables the declarative specification of distributed systems that satisfy sophisticated security properties, including authorization, anonymity, and accountability. We use this API to implement an anonymous evaluation system, anonymous webs of trust, and a secure social network. Second, we present a methodology for the trustworthy and privacy-preserving retrieval of information. We exemplify our approach by presenting ObliviAd, an architecture for online behavioral advertising that provably protects user profiles and delivers highlypersonalized advertisements.

A credit network models trust between agents in a distributed environment and enables payments between arbitrary pairs of agents. With their flexible design and robustness against intrusion, credit networks form the basis of several Sybil-tolerant social networks, spam-resistant communication protocols, and payment systems. Existing systems, however, expose agents’ trust links as well as the existence and volumes of payment transactions, which is considered sensitive information in social environments or in the financial world. This raises a challenging privacy concern, which has largely been ignored by the research on credit networks so far. This paper presents PrivPay, the first provably secure privacypreserving payment protocol for credit networks. The distinguishing feature of PrivPay is the obliviousness of transactions, which entails strong privacy guarantees for payments. PrivPay does not require any trusted third party, maintains a high accuracy of the transactions, and provides an economical solution to network service providers. It is also general-purpose trusted hardwarebased solution applicable to all credit network-based systems. We implemented PrivPay and demonstrated its practicality by privately emulating transactions performed in the Ripple payment system over a period of four months.

Zero-knowledge (ZK) proofs have become a central building block for a variety of modern security protocols. Modern ZK constructions, such as the Groth-Sahai proof system, offer novel types of cryptographic flexibility: a participant is able to re-randomize existing ZK proofs to achieve, for instance, message unlink ability in anonymity protocols, she can hide public parts of a ZK proof statement to meet her specific privacy requirements, and she can logically compose ZK proofs in order to construct new proof statements. ZK proof systems that permit these transformations are called malleable. However, since these transformations are accessible also to the adversary, analyzing the security of these protocols requires one to cope with a much more comprehensive attacker model -- a challenge that automated protocol analysis thus far has not been capable of dealing with. In this work, we introduce the first symbolic abstraction of malleable ZK proofs. We further prove the computational soundness of our abstraction with respect to observational equivalence, which enables the computationally sound verification of privacy properties. Finally, we show that our symbolic abstraction is suitable for ProVerif, a state-of-the-art cryptographic protocol verifier, by verifying an improved version of the anonymous webs of trust protocol.

In an environment perturbed by malicious interference, establishing a reliable wireless connection without shared secrets typically relies on uncoordinated spread spectrum methods, such as UFHSS or UDSSS. These methods offer a lowthroughput channel for the exchange of key contributions with the goal to establish a shared secret. They, however, incur a significant delay when confronted with adversarial jamming, in particular when long public-key credentials must be exchanged. In this paper, we propose and evaluate a scheme that is orders of magnitude more efficient than prior proposals. Drawing on powerful identity-based (ID-based) cryptography and exploiting a-priori knowledge about the identities of the communication partners, the parties can immediately and without any communication derive a cryptographically strong seed (or key) for creating a highthroughput, jamming-resistant channel. Even without a-priori knowledge, our scheme still benefits from the certificate-free authentication offered by ID-based cryptography. Additionally, we define the notion of a secure seed establishment scheme for anti-jamming methods and prove that our protocol satisfies this definition. We further conduct an experimental evaluation of our approach to demonstrate its practicality: on mobile commodity hardware such as notebooks, tablet computers, and smart phones, a non-optimized implementation derives shared seeds in less than half a second.

The privacy of users has rapidly become one of the most pervasive and stringent requirements in distributed computing. Designing and implementing privacy-preserving distributed systems, however, is challenging since these systems also have to fulfill seemingly conflicting security properties and system requirements: e.g., authorization and accountability require some form of user authentication and session management necessarily involves some form of user tracking. In this work, we present a solution based on declarative design. The core component of our framework is a logic-based declarative API for data processing that exports methods to conveniently specify the system architecture and the intended security properties, and conceals the cryptographic realization. Invisible to the programmer, the implementation of this API relies on a powerful combination of digital signatures, non-interactive zero-knowledge proofs of knowledge, pseudonyms, and reputation lists. We formally proved that the cryptographic implementation enforces the security properties expressed in the declarative specification. The systems produced by our framework enjoy interoperability and open-endedness: they can easily be extended to offer new services and cryptographic data can be shared and processed by different services, without requiring any extra bootstrapping phase or interaction among parties. We implemented the API in Java and conducted an experimental evaluation to demonstrate the practicality of our approach.

Online behavioral advertising (OBA) involves the tracking of web users' online activities in order to deliver tailored advertisements. OBA has become a rapidly increasing source of revenue for a number of web services, and it is typically conducted by third-party data analytics firms such as brokers, which track user behaviors across web-sessions using mechanisms such as persistent cookies. This practice raises significant privacy concerns among users and privacy advocates alike. Therefore, the task of designing OBA systems that do not reveal user profiles to third parties has been receiving growing interest from the research community. Nevertheless, existing solutions are not ideal for privacy preserving OBA: some of them do not provide adequate privacy to users or adequate targeting information to brokers, while others require trusted third parties that are difficult to realize. In this paper, we propose ObliviAd a provably secure architecture for privacy preserving OBA. The distinguishing features of our approach are the usage of secure hardware-based private information retrieval for distributing advertisements and high-latency mixing of electronic tokens for billing advertisers without disclosing any information about client profiles to brokers. ObliviAd does not assume any trusted party and provides brokers an economical alternative that preserves the privacy of users without hampering the precision of ads selection. We present the first formal security definitions for OBA systems (namely, profile privacy, profile unlink ability, and billing correctness) and conduct a formal security analysis of ObliviAd using ProVerif, an automated cryptographic protocol verifier, establishing the aforementioned security properties against a strong adversarial model. Finally, we demonstrated the practicality of our approach with an experimental evaluation.

We present G2C, a goal-driven specification language for distributed applications. This language offers support for the declarative specification of functionality goals and security properties. The former comprise the parties, their inputs, and the goal of the communication protocol. The latter comprise secrecy, access control, and anonymity requirements. A key feature of our language is that it abstracts away from how the intended functionality is achieved, but instead lets the system designer concentrate on which functional features and security properties should be achieved. Our framework provides a compilation method for transforming G2C specifications into symbolic cryptographic protocols, which are shown to be optimal. We provide a technique to automatically verify the correctness and security of these protocols using ProVerif, a state-of-the-art automated theorem-prover for cryptographic protocols. We have implemented a G2C compiler to demonstrate the feasibility of our approach.

Proof-carrying authorization (PCA) is one of the most popular approaches for the enforcement of access control policies. In a nutshell, the idea is to formalize a policy as a set of logical rules and to let the requester construct a formal proof showing that she has permissions to access the desired resource according to the provider’s policy. This policy may depend on logical formulas that are assumed by other principals in the system. The validity of these formulas is witnessed by digital signatures. The usage of digital signatures, however, has a serious drawback, i.e., sensitive data are leaked to the verifier, which severely limits the applicability of PCA. In this paper, we introduce the notion of privacy-aware proof-carrying authorization, an extension of PCA based on a powerful combination of digital signatures and zero-knowledge proofs of knowledge of such signatures. The former are used to witness the validity of logical formulas, the latter to selectively hide sensitive data. Our framework supports a variety of privacy properties, such as data secrecy and user anonymity. We conducted an experimental evaluation to demonstrate the feasibility of our approach.

We present a cryptographic framework to achieve access control, privacy of social relations, secrecy of resources, and anonymity of users in social networks. We illustrate our technique on a core API for social networking, which includes methods for establishing social relations and for sharing resources. The cryptographic protocols implementing these methods use pseudonyms to hide user identities, signatures on these pseudonyms to establish social relations, and zero-knowledge proofs of knowledge of such signatures to demonstrate the existence of social relations without sacrificing user anonymity. As we do not put any constraints on the underlying social network, our framework is generally applicable and, in particular, constitutes an ideal plug-in for decentralized social networks. We analyzed the security of our protocols by developing formal definitions of the aforementioned security properties and by verifying them using ProVerif, an automated theorem prover for cryptographic protocols. Finally, we built a prototypical implementation and conducted an experimental evaluation to demonstrate the efficiency and the scalability of our framework.

Proof-carrying authorization (PCA) is one of the most popular approaches for the enforcement of access control policies. In a nutshell, the idea is to formalize a policy as a set of logical rules and to let the requester construct a formal proof showing that she has permissions to access the desired resource according to the provider’s policy. This policy may depend on logical formulas that are assumed by other principals in the system. The validity of these formulas is witnessed by digital signatures. The usage of digital signatures, however, has a serious drawback, i.e., sensitive data are leaked to the verifier, which severely limits the applicability of PCA. In this paper, we introduce the notion of privacy-aware proof-carrying authorization, an extension of PCA based on a powerful combination of digital signatures and zero-knowledge proofs of knowledge of such signatures. The former are used to witness the validity of logical formulas, the latter to selectively hide sensitive data. Our framework supports a variety of privacy properties, such as data secrecy and user anonymity. We conducted an experimental evaluation to demonstrate the feasibility of our approach.

We present a cryptographic framework to achieve access control, privacy of social relations, secrecy of resources, and anonymity of users in social networks. The main idea is to use pseudonyms to hide user identities, signatures on pseudonyms to establish social relations, and zero-knowledge proofs on these signatures to demonstrate the existence of the corresponding social relations without sacrificing user anonymity. Our framework is generally applicable and, in particular, constitutes an ideal plug-in for decentralized social networks.We formally verified the aforementioned security properties using ProVerif, an automated theorem prover for cryptographic protocols. We also conducted an experimental evaluation to demonstrate the efficiency and the scalability of our framework.

We present a cryptographic framework to achieve access control, privacy of social relations, secrecy of resources, and anonymity of users in social networks. The main idea is to use pseudonyms to hide user identities, signatures on pseudonyms to establish social relations, and zero-knowledge proofs on these signatures to demonstrate the existence of the corresponding social relations without sacrificing user anonymity. Our framework is generally applicable and, in particular, constitutes an ideal plug-in for decentralized social networks. We formally verified the aforementioned security properties using ProVerif, an automated theorem prover for cryptographic protocols. We also conducted an experimental evaluation to demonstrate the efficiency and the scalability of our framework.

In this paper, we present a framework for achieving anonymity and trust, two seemingly contradictory properties, in distributed systems. Our approach builds on webs of trust, a well-established and widely deployed decentralized infrastructure for establishing the authenticity of the binding between public keys and users, and more generally, trust relationships among users. We introduce the concept of anonymous webs of trust - an extension of webs of trust where users can authenticate messages and determine each other's trust level without compromising their anonymity. Our framework comprises novel cryptographic protocols based on zero-knowledge proofs for achieving anonymity in webs of trust and a prototype implementation based on GnuPG. We conduct an automated analysis to formally verify the security of our protocol and an experimental evaluation to demonstrate the effectiveness of our approach.

Webs of trust constitute a decentralized infrastructure for establishing the authenticity of the binding between public keys and users and, more generally, trust relationships among users. This paper introduces the concept of anonymous webs of trust an extension of webs of trust where users can authenticate messages and determine each other's trust level without compromising their anonymity. Our framework comprises a novel cryptographic protocol based on zero-knowledge proofs, a symbolic abstraction and formal verification of our protocol, and a prototypical implementation based on the OpenPGP standard. The framework is capable of dealing with various core and optional features of common webs of trust, such as key attributes, key expiration dates, existence of multiple certificate chains, and trust measures between different users.

CASPA constitutes a push-button tool for automatically proving secrecy and authenticity properties of cryptographic protocols. The tool is grounded on a novel technique for causality-based abstraction of protocol executions that allows establishing proofs of security for an unbounded number of concurrent protocol executions in an automated manner. We demonstrate the expressiveness and efficiency of the tool by drawing a comparison with T4ASP, the static analyzer for secrecy properties offered by the AVISPA tool. CASPA is capable of coping with a substantially larger set of protocols, and excels in performance.