We introduce a logic for reasoning about contextual trust for web addresses, provide a Kripke semantics for it, and prove its soundness under reasonable assumptions about principals' policies. Self-Authenticating Traditional Addresses (SATAs) are valid DNS addresses or URLs that are generally meaningful—to both humans and web infrastructure—and contain a commitment to a public key in the address itself. Trust in web addresses is currently established via domain name registration, TLS certificates, and other hierarchical elements of the internet infrastructure. SATAs support such structural roots of trust but also complementary contextual roots associated with descriptive properties. The existing structural roots leave web connections open to a variety of well-documented and significant hijack vulnerabilities. Contextual trust roots provide, among other things, stronger resistance to such vulnerabilities. We also consider labeled SATAs, which include descriptive properties such as that a SATA is an address for a news organization, a site belonging to a particular government or company, a site with information about a certain topic, etc. Our logic addresses both trust in the bound together identity of the address and trust in the binding of labels to it. Our logic allows reasoning about delegation of trust with respect to specified labels, relationships between labels that provide more or less specific information, and the interaction between these two aspects. In addition to soundness, we prove that if a principal trusts a particular identity (possibly with label), then either this trust is initially assumed, or there is a trust chain of delegations to this from initial trust assumptions. We also present an algorithm that effectively derives all possible trust statements from the set of initial trust assumptions and show it to be sound, complete, and terminating.

We analyze deficiencies in Tor's positional weighting system, identifying cases in which the system either fails to produce valid weights or fails to properly load balance across positions. We describe how an attacker can take advantage of these failures to reduce Tor's performance, thereby also easing censorship and surveillance through a denial-of-service attack. Our attacks exploit incorrectly determined positional-weight equations by adding new capacity to the network or, for even more covertness, by just minor changes in the status of existing malicious relays. Our analysis of past Tor consensuses shows that these attacks could have reduced the throughput of the network by as much as 45% due only to their triggering of Tor's flawed position weights. Rather than a mere patch to Tor's currently ad hoc scheme, we then propose a new, systematic method for deriving positional weights and propose two goal sets generated using that method. We derive new sets of weights, prove that they satisfy these goal sets, and give examples of how they would change the weights from the current system. Tor could use our results to quickly fix the main deficiencies of its positional weights as well as adopt a better approach long-term.

Abstract Motivated by the effectiveness of correlation attacks against Tor, the censorship arms race, and observations of malicious relays in Tor, we propose that Tor users capture their trust in network elements using probability distributions over the sets of elements observed by network adversaries. We present a modular system that allows users to efficiently and conveniently create such distributions and use them to improve their security. To illustrate this system, we present two novel types of adversaries. First, we study a powerful, pervasive adversary that can compromise an unknown number of Autonomous System organizations, Internet Exchange Point organizations, and Tor relay families. Second, we initiate the study of how an adversary might use Mutual Legal Assistance Treaties (MLATs) to enact surveillance. As part of this, we identify submarine cables as a potential subject of trust and incorporate data about these into our MLAT analysis by using them as a proxy for adversary power. Finally, we present preliminary experimental results that show the potential for our trust framework to be used by Tor clients and services to improve security.

The proliferation of online sensitive data about individuals and organizations makes concern about the privacy of these data a top priority. There have been many formulations of privacy and, unfortunately, many negative results about the feasibility of maintaining privacy of sensitive data in realistic networked environments. We formulate communication-complexity-based definitions, both worst case and average case, of a problem’s privacy-approximation ratio . We use our definitions to investigate the extent to which approximate privacy is achievable in a number of standard problems: the 2 nd -price Vickrey auction, Yao’s millionaires problem, the public-good problem, and the set-theoretic disjointness and intersection problems. For both the 2 nd -price Vickrey auction and the millionaires problem, we show that not only is perfect privacy impossible or infeasibly costly to achieve, but even close approximations of perfect privacy suffer from the same lower bounds. By contrast, if the inputs are drawn uniformly at random from { 0,…, 2 k -1}, then, for both problems, simple and natural communication protocols have privacy-approximation ratios that are linear in k (i.e., logarithmic in the size of the input space). We also demonstrate tradeoffs between privacy and communication in a family of auction protocols. We show that the privacy-approximation ratio provided by any protocol for the disjointness and intersection problems is necessarily exponential (in k ). We also use these ratios to argue that one protocol for each of these problems is significantly fairer than the others we consider (in the sense of relative effects on the privacy of the different players).

We present a framework for the design and analysis of probing methods to monitor network performance, an important technique for collecting measurements in tasks such as fault detection. We use this framework to study the interaction among numerous, possibly conflicting, optimization goals in the design of a probing algorithm. We present a rigorous definition of a probing-algorithm design problem that can apply broadly to network-measurement scenarios. We also present several metrics relevant to the analysis of probing algorithms, including probing frequency and network coverage, communication and computational overhead, and the amount of algorithm state required. We show inherent tradeoffs among optimization goals and give hardness results for achieving some combinations of optimization goals. We also consider the possibility of developing approximation algorithms for achieving some of the goals and describe a randomized approach as an alternative, evaluating it using our framework. Our work aids future development of low-overhead probing techniques and introduces principles from IP-based networking to theoretically grounded approaches for concurrent path-selection problems.

We propose a focus on accountability as a mechanism for ensuring security in information systems. To that end, we present a formal definition of it accountability in information systems. Our definition is more general and potentially more widely applicable than the accountability notions that have previously appeared in the security literature. In particular, we treat in a unified manner scenarios in which accountability is enforced automatically and those in which enforcement must be mediated by an authority; similarly, our formalism includes scenarios in which the parties who are held accountable can remain anonymous and those in which they must be identified by the authorities to whom they are accountable. Essential elements of our formalism include event traces and it utility functions and the use of these to define punishment and related notions.

We present our recent work (ICS 2011) on dynamic environments in which computational nodes, or decision makers, follow simple and unsophisticated rules of behavior (e.g., repeatedly "best replying" to others' actions, and minimizing "regret") that have been extensively studied in game theory and economics. We aim to understand when convergence of the resulting dynamics to an equilibrium point is guaranteed if nodes' interaction is not synchronized (e.g., as in Internet protocols and large-scale markets). We take the first steps of this research agenda. We exhibit a general non-convergence result and consider its implications across a wide variety of interesting and timely applications: routing, congestion control, game theory, social networks and circuit design. We also consider the relationship between classical nontermination results in distributed computing theory and our result, explore the impact of scheduling on convergence, study the computational and communication complexity of asynchronous dynamics and present some basic observations regarding the effects of asynchrony on no-regret dynamics.

Increasing use of computers and networks in business, government, recreation, and almost all aspects of daily life has led to a proliferation of online sensitive data about individuals and organizations. Consequently, concern about the privacy of these data has become a top priority, particularly those data that are created and used in electronic commerce. Despite many careful formulations and extensive study, there are still open questions about the feasibility of maintaining meaningful privacy in realistic networked environments. We formulate communication-complexity-based definitions, both worst-case and average-case, of a problem's privacy-approximation ratio. We use our definitions to investigate the extent to which approximate privacy is achievable in many well studied contexts: the 2ndprice Vickrey auction [20], the millionaires problem of Yao [22], the provisioning of a public good, and also set disjointness and set intersection. We present both positive and negative results and many interesting directions for future research.

Autonomous routing algorithms, such as BGP, are intended to reach a globally consistent set of routes after nodes iteratively and independently collect, process, and share network information. Generally, the important role of the mechanism used to share information has been overlooked in previous analyses of these algorithms. In this paper, we explicitly study how the network-communication model affects algorithm convergence. To do this, we consider a variety of factors, including channel reliability, how much information is processed from channels, and how many channels are processed simultaneously. Using these factors, we define a taxonomy of communication models and identify particular models of interest, including those used in previous theoretical work, those that most closely model real-world implementations of BGP, and those of potential interest for the design of future routing algorithms. We characterize an extensive set of relationships among models in our taxonomy and show that convergence depends on the communication model in nontrivial ways. These results highlight that certain models are best for proving conditions that guarantee convergence, while other models are best for characterizing conditions that might permit nonconvergence.

We present a computationally sound mechanized analysis of Kerberos 5, both with and without its public-key extension PKINIT. We prove authentication and key secrecy properties using the prover CryptoVerif, which works directly in the computational model; these are the first mechanical proofs of a full industrial protocol at the computational level. We also generalize the notion of key usability and use CryptoVerif to prove that this definition is satisfied by keys in Kerberos.

We study situations in which autonomous systems (ASes) may have incentives to send BGP announcements differing from the AS-level paths that packets traverse in the data plane. Prior work on this issue assumed that ASes seek only to obtain the best possible outgoing path for their traffic. In reality, other factors can influence a rational AS's behavior. Here we consider a more natural model, in which an AS is also interested in attracting incoming traffic (e.g., because other ASes pay it to carry their traffic). We ask what combinations of BGP enhancements and restrictions on routing policies can ensure that ASes have no incentive to lie about their data-plane paths. We find that protocols like S-BGP alone are insufficient, but that S-BGP does suffice if coupled with additional (quite unrealistic) restrictions on routing policies. Our game-theoretic analysis illustrates the high cost of ensuring that the ASes honestly announce data-plane paths in their BGP path announcements.

Some commonly used inter-domain-routing policies-e.g., those using BGP's MED attribute for cold-potato routing-are beyond the scope of routing theory developed to date. This is because these policies cannot be expressed as a linear preference ranking of available routes at each node. Existing characterizations of well-behaved path-vector routing, however, critically depend on this linear ranking and do not naturally extend to more complex policies. In this paper, we present a framework that is able to model these more general policies. We use it to give the broadest-known sufficient condition for robust convergence of path-vector protocols, even when complex policies are used. In doing so, we present a new, unified notion of order on policies; this reduces to earlier results in the case of restricted policies, but it allows us to analyze the practically useful but inconsistent policies that could not be directly modeled before. As an application, we rigorously analyze (and improve) various robust protocol-design proposals.

This paper unifies two independently developed formalisms for path-vector routing protocols such as the border gateway protocol (BGP), the standard inter-domain routing protocol for the Internet. Sobrinho (2003) and Griffin, Jaggard, and Ramachandran (2003) proved conditions for guaranteed protocol convergence, but as these works operate at different levels of abstraction in modeling the protocols, the relationship between them is not obvious. Here we provide a rigorous translation between these two frameworks and use it to connect the convergence results, yielding a more complete set of analysis tools than in either framework alone. We motivate our discussion by presenting an example of applying both frameworks to analyze a set of protocols; in doing so, we show how the models, in conjunction, give important guidelines for protocol design.

Griffin, Jaggard, and Ramachandran [2004] introduced a framework for studying design principles for path-vector protocols, such as the border gateway protocol (BGP) used for inter-domain routing in the Internet. They outlined how their framework could describe hierarchical-BGP-like systems in which routing at a node is determined by the relationship with the next-hop node on a path (e.g., an ISP-peering relationship) and some additional scoping rules (e.g., the use of backup routes). The robustness of these class-based path-vector systems depends on the presence of a global constraint on the system, but an adequate constraint has not yet been given in general. In This work, we give the best-known sufficient constraint that guarantees robust convergence. We show how to generate this constraint from the design specification of the path-vector system. We also give centralized and distributed algorithms to enforce this constraint, discuss applications of these algorithms, and compare them to algorithms given in previous work on path-vector protocol design.

BGP is unique among IP-routing protocols in that routing is determined using semantically rich routing policies. However this expressiveness has come with hidden risks. The interaction of locally defined routing policies can lead to unexpected global routing anomalies, which can be very difficult to identify and correct in the decentralized and competitive Internet environment. These risks increase as the complexity of local policies increase. which is precisely the current trend. BGP policy languages have evolved in a rather organic fashion with little effort to avoid policy-interaction problems. We believe that researchers should start to consider how to design policy languages for path-vector protocols in order to avoid routing anomalies while obtaining desirable protocol properties. We take a few steps in this direction by identifying the important dimensions of this design space and characterizing some of the inherent design trade-offs. We do this in a general way that is not constrained by the details of BGP.

We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the intricate structure of the Kerberos 5 specification, taking into account several protocol features which have not been previously considered. In the abstract formalization, we prove an authentication property about Kerberos 5. We discovered three anomalies, one of which occurs on both levels of detail, while the other two rely on the richer structure of the detailed formalization. We also discuss how the addition of checksums (some of which are in the protocol specification and some of which are not) may eliminate some of these anomalies.