Probabilistic Escrow of Financial Transactions with Cumulative Threshold Disclosure
With Stanisław Jarecki.
To appear in Proc. of 9th International Conference on Financial Cryptography and Data Security, Roseau, Dominica, March 2005.

Abstract:
We propose a scheme for privacy-preserving escrow of financial transactions. The objective of the scheme is to preserve privacy and anonymity of the individual user engaging in financial transactions until the cumulative amount of all transactions in a certain category, for example all transactions with a particular counterparty in any single month, reaches a pre-specified threshold. When the threshold is reached, the escrow agency automatically gains the ability to decrypt the escrows of all transactions in that category (and only that category).

Our scheme employs the probabilistic polling idea of Jarecki and Odlyzko [JO97], amended by a novel robustness mechanism which makes such scheme secure for malicious parties. When submitting the escrow of a transaction, with probability that is proportional to the amount of the transaction, the user reveals a share of the key under which all his transactions are encrypted. Therefore, the fraction of shares that are known to the escrow agency is an accurate approximation of the fraction of the threshold amount that has been transacted so far. When the threshold is reached, with high probability the escrow agency possesses all the shares that it needs to reconstruct the key and open the escrows. Our main technical contribution is a novel tool of robust probabilistic information transfer, which we implement using techniques of optimistic fair 2-party computation.

Abstract:
We present three case studies, investigating the use of probabilistic model checking to automatically analyse properties of probabilistic contract signing protocols. We use the probabilistic model checker PRISM to analyse three protocols: Rabin's probabilistic protocol for fair commitment exchange; the probabilistic contract signing protocol of Ben-Or, Goldreich, Micali, and Rivest; and a randomised protocol for signing contracts of Even, Goldreich, and Lempel. These case studies illustrate the general methodology for applying probabilistic model checking to formal verification of probabilistic security protocols.

For the Ben-Or et al. probabilistic contract signing protocol, we demonstrate the difficulty of combining fairness with timeliness. If, as required by timeliness, the judge responds to participants' messages immediately upon receiving them, then there exists a strategy for a misbehaving participant that brings the protocol to an unfair state with arbitrarily high probability, unless unusually strong assumptions are made about the quality of the communication channels between the judge and honest participants. We quantify the tradeoffs involved in the attack strategy, and discuss possible modifications of the protocol that ensure both fairness and timeliness.

For the Even et al. probabilistic contract signing protocol, we demonstrate that the responder enjoys a distinct advantage. With probability 1, the protocol reaches a state in which the responder possesses the initiator's commitment, but the initiator does not possess the responder's commitment. We then analyse several variants of the protocol, exploring the tradeoff between fairness and the number of messages that must be exchanged between participants.

Abstract:
We present a practical scheme for Internet-scale collaborative analysis of information security threats which provides strong privacy guarantees to contributors of alerts. Wide-area analysis centers are proving a valuable early warning service against worms, viruses, and other malicious activities. At the same time, protecting individual and organizational privacy is no longer optional in today's business climate. We propose a set of data sanitization techniques that enable community alert aggregation and correlation, while maintaining privacy for alert contributors. Our approach is practical, scalable, does not rely on trusted third parties or secure multiparty computation schemes, and does not require sophisticated key management.

Abstract:
The variety of possible anonymity network topologies has spurred much debate in recent years. In a synchronous batching design, each batch of messages enters the mix network together, and the messages proceed in lockstep through the network. We show that a synchronous batching strategy can be used in various topologies, including a free-route network, in which senders choose paths freely, and a cascade network, in which senders choose from a set of fixed paths. We show that free-route topologies can provide better anonymity as well as better message reliability in the event of partial network failure.

Abstract:
We propose a practical abuse-resilient transaction escrow scheme with applications to privacy-preserving audit and monitoring of electronic transactions. Our scheme ensures correctness of escrows as long as at least one of the participating parties is honest, and it ensures privacy and anonymity of transactions even if the escrow agent is corrupt or malicious. The escrowed information is secret and anonymous, but the escrow agent can efficiently find transactions involving some user in response to a subpoena or a search warrant. Moreover, for applications such as abuse-resilient monitoring of unusually high levels of certain transactions, the escrow agent can identify escrows with particular common characteristics and automatically (ie, without a subpoena) open them once their number has reached a pre-specified threshold.

Our solution for transaction escrow is based on the use of Verifiable Random Functions. We show that by tagging the entries in the escrow database using VRFs indexed by users' private keys, we can protect users' anonymity while enabling efficient and, optionally, automatic de-escrow of these entries. We give a practical instantiation of a transaction escrow scheme utilizing a simple and efficient VRF family secure under the DDH assumption in the Random Oracle Model.

Abstract:
Several related research efforts have led to three different ways of specifying protocol security properties by simulation or equivalence. Abstracting the specification conditions away from the computational frameworks in which they have been previously applied, we show that when asynchronous communication is used, universal composability, black-box simulatability, and process equivalence express the same properties of a protocol. Further, the equivalence between these conditions holds for any computational framework, such as process calculus, that satisfies certain structural properties. Similar but slightly weaker results are achieved for synchronous communication.

Abstract:
We demonstrate that the symbolic trace reachability problem for cryptographic protocols is decidable in the presence of an Abelian group operator and modular exponentiation from arbitrary bases. We represent the problem as a sequence of symbolic inference constraints and reduce it to a system of linear Diophantine equations. For a finite number of protocol sessions, this result enables fully automated, sound and complete analysis of protocols that employ primitives such as Diffie-Hellman exponentiation and modular multiplication without imposing any bounds on the size of terms created by the attacker, but taking into account the relevant algebraic properties.

Abstract:
We demonstrate that for any well-defined cryptographic protocol, the symbolic trace reachability problem in the presence of an Abelian group operator (eg, multiplication) can be reduced to solvability of a decidable system of quadratic Diophantine equations. This result enables complete, fully automated formal analysis of protocols that employ primitives such as Diffie-Hellman exponentiation, multiplication, and XOR, with a bounded number of role instances, but without imposing any bounds on the size of terms created by the attacker.

Abstract:
We propose a formal model for reputation-based trust management. In contrast to credential-based trust management, in our framework an agent's reputation serves as the basis for trust. For example, an access control policy may consider the agent's reputation when deciding whether to offer him a license for accessing a protected resource. The underlying semantic model is an event semantics inspired by the actor model, and assumes that each agent has only partial knowledge of the events that have occurred. Restrictions on agents' behavior are formalized as licenses, with ``good'' and ``bad'' behavior interpreted as, respectively, license fulfillment and violation. An agent's reputation comprises four kinds of evidence: completely fulfilled licenses, ongoing licenses without violations or misuses, licenses with violated obligations, and misused licenses. This approach enables precise formal modeling of scenarios involving reputations, such as financial transactions based on credit histories and information sharing between untrusted agents.

Abstract:
We use the probabilistic model checker PRISM to analyze the Crowds system for anonymous Web browsing. This case study demonstrates how probabilistic model checking techniques can be used to formally analyze security properties of a peer-to-peer group communication system based on random message routing among members. The behavior of group members and the adversary is modeled as a discrete-time Markov chain, and the desired security properties are expressed as PCTL formulas. The PRISM model checker is used to perform automated analysis of the system and verify anonymity guarantees it provides. Our main result is a demonstration of how certain forms of probabilistic anonymity degrade when group size increases or random routing paths are rebuilt, assuming that the corrupt group members are able to identify and/or correlate multiple routing paths originating from the same sender.

Abstract:
We propose a new specification framework for information hiding properties such as anonymity and privacy. The framework is based on the concept of a function view, which is a concise representation of the attacker's partial knowledge about a function. We describe system behavior as a set of functions, and formalize different information hiding properties in terms of views of these functions. We present an extensive case study, in which we use the function view framework to systematically classify and rigorously define a rich domain of identity-related properties, and to demonstrate that privacy and anonymity are independent.

The key feature of our approach is its modularity. It yields precise, formal specifications of information hiding properties for any protocol formalism and any choice of the attacker model as long as the latter induce an observational equivalence relation on protocol instances. In particular, specifications based on function views are suitable for any cryptographic process calculus that defines some form of indistinguishability between processes. Our definitions of information hiding properties take into account any feature of the security model, including probabilities, random number generation, timing, etc., to the extent that it is accounted for by the formalism in which the system is specified.

Abstract:
A contract signing protocol lets two parties exchange digital signatures on a pre-agreed text. Optimistic contract signing protocols enable the signers to do so without invoking a trusted third party. However, an adjudicating third party remains available should one or both signers seek timely resolution. We analyze optimistic contract signing protocols using a game-theoretic approach and prove a fundamental impossibility result: in any fair, optimistic, timely protocol, an optimistic player yields an advantage to the opponent. The proof relies on a careful characterization of optimistic play that postpones communication to the third party. Since advantage cannot be completely eliminated from optimistic protocols, we argue that the strongest property attainable is the absence of provable advantage, i.e., abuse-freeness in the sense of Garay-Jakobsson-MacKenzie.

Abstract:
We present decidability results for the verification of cryptographic protocols in the presence of equational theories corresponding to XOR and Abelian groups. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties such as XOR, we extend the conventional Dolev-Yao model by permitting the intruder to exploit these properties. We show that the ground reachability problem in NP for the extended intruder theories in the cases of XOR and Abelian groups. This result follows from a normal proof theorem. Then, we show how to lift this result in the XOR case: we consider a symbolic constraint system expressing the reachability (eg, secrecy) problem for a finite number of sessions. We prove that such constraint system is decidable, relying in particular on an extension of combination algorithms for unification procedures. As a corollary, this enables automatic symbolic verification of cryptographic protocols employing XOR for a fixed number of sessions.

Abstract:
Exponential growth in digital information gathering, storage, and processing capabilities inexorably leads to conflict between well-intentioned government or commercial datamining, and fundamental privacy interests of individuals and organizations. This paper proposes a mechanism that provides cryptographic fetters on the mining of personal data, enabling efficient mining of previously-negotiated properties, but preventing any other uses of the protected personal data. Our approach does not rely on complete trust in the analysts to use the data appropriately, nor does it rely on incorruptible escrow agents. Instead, we propose conditional data escrow where the data generators, not the analysts, hold the keys to the data, but analysts can verify that the pre-negotiated queries are enabled. Our solution relies on verifiable, anonymous, and deterministic commitments which play the role of tags that mark encrypted entries in the analyst's database. The database owner cannot learn anything from the encrypted entries, or even verify his guess of the plaintext on which these entries are based. On the other hand, the verifiable and deterministic property ensures that the entries are marked with consistent tags, so that the database manager learns when the number of entries required to enable some query reaches the pre-negotiated threshold.

Abstract:
We consider the so called "cryptographic protocols" whose aim is to ensure some security properties when communication channels are not reliable. Such protocols usually rely on cryptographic primitives. Even if it is assumed that the cryptographic primitives are perfect, the security goals may not be achieved: the protocol itself may have weaknesses which can be exploited by an attacker. We survey recent work on decision techniques for the cryptographic protocol analysis.

Abstract:
Optimistic contract signing protocols allow two parties to commit to a previously agreed upon contract, relying on a third party to abort or confirm the contract if needed. These protocols are relatively subtle, since there may be interactions between the subprotocols used for normal signing without the third party, aborting the protocol through the third party, or requesting confirmation from the third party. With the help of Murphi, a finite-state verification tool, we analyze two related contract signing protocols: the optimistic contract signing protocol of Asokan, Shoup, and Waidner, and the abuse-free contract signing protocol of Garay, Jakobsson, and MacKenzie. For the first protocol, we discover that a malicious participant can produce inconsistent versions of the contract or mount a replay attack. For the second protocol, we discover that negligence or corruption of the trusted third party may allow abuse or unfairness. In this case, contrary to the intent of the protocol, the cheated party is not able to hold the third party accountable. We present and analyze modifications to the protocols that avoid these problems and discuss the basic challenges involved in formal analysis of fair exchange protocols.

Abstract:
The reachability problem for cryptographic protocols with non-atomic keys can be solved via a simple constraint satisfaction procedure.

Abstract:
We develop an imperative calculus that provides a formal model for both single and mixin inheritance. By introducing classes and mixins as the basic object-oriented constructs in a lambda-calculus with records and references, we obtain a system with an intuitive operational semantics. New classes are produced by applying mixins to superclasses. Objects are represented by records and produced by instantiating classes. The type system for objects uses only functional, record, and reference types, and there is a clean separation between subtyping and inheritance.

Abstract:
We present an imperative calculus for a class-based language. By introducing classes as the basic object-oriented construct in a lambda-calculus with records and references, we obtain a system with an intuitive operational semantics. Objects are instantiated from classes and represented by records. The type system for objects uses only functional, record, and reference types, and there is a clean separation between subtyping and inheritance. We demonstrate that the calculus is sound and sufficiently expressive to model advanced language features such as inheritance with method redefinition, multi-level encapsulation, and modular object construction.

Abstract:
We describe two state reduction techniques for finite-state models of security protocols. The techniques exploit certain protocol properties that we have identified as characteristic of security protocols. We prove the soundness of the techniques by demonstrating that any violation of protocol invariants is preserved in the reduced state graph. In addition, we describe an optimization method for evaluating parameterized rule conditions, which are common in our models of security protocols. All three techniques have been implemented in the Murphi verifier.

Abstract:
The Secure Sockets Layer (SSL) protocol is analyzed using a finite-state enumeration tool called Murphi. The analysis is presented using a sequence of incremental approximations to the SSL 3.0 handshake protocol. Each simplified protocol is "model-checked" using Murphi, with the next protocol in the sequence obtained by correcting errors that Murphi finds automatically. This process identifies the main shortcomings in SSL 2.0 that led to the design of SSL 3.0, as well as a few anomalies in the protocol that is used to resume a session in SSL 3.0. In addition to some insight into SSL, this study demonstrates the feasibility of using formal methods to analyze commercial protocols.