Search

We introduce cryptographic protocols for securely and efficiently computing the cardinality of set union and set intersection. Our private set-cardinality protocols (PSC) are designed for the setting in which a large set of parties in a distributed system makes observations, and a small set of parties with more resources and higher reliability aggregates the observations. PSC allows for secure and useful statistics gathering in privacy-preserving distributed systems. For example, it allows operators of anonymity networks such as Tor to securely answer the questions: Howmany unique users are using the network? and Howmany hidden services are being accessed? We prove the correctness and security of PSC in the Universal Composability framework against an active adversary that compromises all but one of the aggregating parties. Although successful output cannot be guaranteed in this setting, PSC either succeeds or terminates with an abort, and we furthermore make the adversary accountable for causing an abort by blaming at least one malicious party. We also show that PSC prevents adaptive corruption of the data parties from revealing past observations, which prevents them from being victims of targeted compromise, and we ensure safe measurements by making outputs differentially private. We present a proof-of-concept implementation of PSC and use it to demonstrate that PSC operates with lowcomputational overhead and reasonable bandwidth. It can count tens of thousands of unique observations from tens to hundreds of data-collecting parties while completing within hours. PSC is thus suitable for daily measurements in a distributed system. [ABSTRACT FROM AUTHOR]

We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques. [ABSTRACT FROM AUTHOR]

An attacker who controls a computer in an overlay network can effectively control the entire overlay network if the mechanism managing membership information can successfully be targeted. This article describes Fireflies, an overlay network protocol that fights such attacks by organizing members in a verifiable pseudo-random structure so that an intruder cannot incorrectly modify the membership views of correct members. Fireflies provides each member with a view of the entire membership, and supports networks with moderate total churn. We evaluate Fireflies using both simulations and PlanetLab to show that Fireflies is a practical approach for secure membership maintenance in such networks. [ABSTRACT FROM AUTHOR]

Memristor is an exciting new addition to the repertoire of fundamental circuit elements. Alternatives to many security protocols originally employing traditional mathematical cryptography involve novel hardware security primitives, such as Physically Unclonable Functions (PUFs). In this article, we propose a novel hybrid memristor-CMOS PUF circuit and demonstrate its suitability through extensive simulations of environmental and process variation effects. The proposed PUF circuit has substantially less hardware overhead than previously proposed memristor-based PUF circuits while being inherently resistant to machine learningbased modeling attacks because of challenge-dependent delays of the memristor stages. The proposed PUF can be conveniently used in many security applications and protocols based on hardware-intrinsic security. [ABSTRACT FROM AUTHOR]

Users often wish to communicate anonymously on the Internet, for example, in group discussion or instant messaging forums. Existing solutions are vulnerable to misbehaving users, however, who may abuse their anonymity to disrupt communication. Dining Cryptographers Networks (DC-nets) leave groups vulnerable to denial-of-service and Sybil attacks; mix networks are difficult to protect against traffic analysis; and accountable voting schemes are unsuited to general anonymous messaging. DISSENT is the first general protocol offering provable anonymity and accountability for moderate-size groups, while efficiently handling unbalanced communication demands among users. We present an improved and hardened DISSENT protocol, define its precise security properties, and offer rigorous proofs of these properties. The improved protocol systematically addresses the delicate balance between provably hiding the identities of well-behaved users, while provably revealing the identities of disruptive users, a challenging task because many forms of misbehavior are inherently undetectable. The new protocol also addresses several nontrivial attacks on the original DISSENT protocol stemming from subtle design flaws. [ABSTRACT FROM AUTHOR]

The Inductive Method is among the most established tools to analyse security protocols formally. It has successfully coped with large, deployed protocols, and its findings are widely published. However, perhaps due to its embedding in a theorem prover or to the lack of tutorial publications, it is at times criticised to require super-specialised skills and hence to be rather impractical. This paper aims at showing that criticism to be stereotypical. It pursues its aim by presenting the first tutorial-style paper to using the Inductive Method. This paper cannot cover every aspect of the method. It focuses on a key one, that is how the Inductive Method treats one of the main goals of security protocols: confidentiality against a threat model. The treatment of that goal, which may seem elegant in the Inductive Method, in fact forms a key aspect of all protocol analysis tools, hence the paper motivation rises still. With only standard skills as a requirement, the reader is guided step by step towards design and proof of significant confidentiality theorems. These are developed against two threat models, the standard Dolev-Yao and a more up-to-date one, the General Attacker, the latter turning out particularly useful also for didactic purposes. [ABSTRACT FROM AUTHOR]

The Shadow Semantics (Morgan, Math Prog Construction, vol 4014, pp 359-378, ; Morgan, Sci Comput Program 74(8):629-653, ) is a possibilistic (qualitative) model for noninterference security. Subsequent work (McIver et al., Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, ) presents a similar but more general quantitative model that treats probabilistic information flow. Whilst the latter provides a framework to reason about quantitative security risks, that extra detail entails a significant overhead in the verification effort needed to achieve it. Our first contribution in this paper is to study the relationship between those two models (qualitative and quantitative) in order to understand when qualitative Shadow proofs can be 'promoted' to quantitative versions, i.e. in a probabilistic context. In particular we identify a subset of the Shadow's refinement theorems that, when interpreted in the quantitative model, still remain valid even in a context where a passive adversary may perform probabilistic analysis. To illustrate our technique we show how a semantic analysis together with a syntactic restriction on the protocol description, can be used so that purely qualitative reasoning can nevertheless verify probabilistic refinements for an important class of security protocols. We demonstrate the semantic analysis by implementing the Shadow semantics in Rodin, using its special-purpose refinement provers to generate (and discharge) the required proof obligations (Abrial et al., STTT 12(6):447-466, ). We apply the technique to some small examples based on secure multi-party computations. [ABSTRACT FROM AUTHOR]

Automated formal verification of security protocols has been mostly focused on analyzing high-level abstract models which, however, are significantly different from real protocol implementations written in programming languages. Recently, some researchers have started investigating techniques that bring automated formal proofs closer to real implementations. This paper surveys these attempts, focusing on approaches that target the application code that implements protocol logic, rather than the libraries that implement cryptography. According to these approaches, libraries are assumed to correctly implement some models. The aim is to derive formal proofs that, under this assumption, give assurance about the application code that implements the protocol logic. The two main approaches of model extraction and code generation are presented, along with the main techniques adopted for each approach. [ABSTRACT FROM AUTHOR]

When using formal methods, security protocols are usually modeled at a high level of abstraction. In particular, data encoding and decoding transformations are often abstracted away. However, if no assumptions at all are made on the behavior of such transformations, they could trivially lead to security faults, for example leaking secrets or breaking freshness by collapsing nonces into constants. In order to address this issue this paper formally states sufficient conditions, checkable on sequential code, such that if an abstract protocol model is secure under a Dolev-Yao adversary, then a refined model, which takes into account a wide class of possible implementations of the encoding/decoding operations, is implied to be secure too under the same adversary model. The paper also indicates possible exploitations of this result in the context of methods based on formal model extraction from implementation code and of methods based on automated code generation from formally verified models. [ABSTRACT FROM AUTHOR]

In many industries, the importance of software components provided by third-party suppliers is steadily increasing. As the suppliers seek to secure their intellectual property (IP) rights, the customer usually has no direct access to the suppliers' source code, and is able to enforce the use of verification tools only by legal requirements. In turn, the supplier has no means to convince the customer about successful verification without revealing the source code. This article presents an approach to resolve the conflict between the IP interests of the supplier and the quality interests of the customer. We introduce a protocol in which a dedicated server (called the "amanat") is controlled by both parties: the customer controls the verification task performed by the amanat, while the supplier controls the communication channels of the amanat to ensure that the amanat does not leak information about the source code. We argue that the protocol is both practically useful and mathematically sound. As the protocol is based on well-known (and relatively lightweight) cryptographic primitives, it allows a straightforward implementation on top of existing verification tool chains. To substantiate our security claims, we establish the correctness of the protocol by cryptographic reduction proofs. [ABSTRACT FROM AUTHOR]

As users travel from place to place, they can encounter display servers, that is, machines which supply a collaborative content-sharing environment. Users need a way to control how content is arranged on these display spaces. The software for controlling these display spaces should be consistent from display server to display server. However, display servers could be controlled by institutions which may not allow for the control software to be installed. This article introduces the window broker protocol which allows users to carry familiar control techniques on portable personal devices and use the control technique on any display server without installing the control software on the display server. This article also discusses how the window broker protocol mitigates some security risks that arise from potentially malicious display servers. [ABSTRACT FROM AUTHOR]

Today, there is a fundamental imbalance in cybersecurity. While attackers act more and more globally and coordinated, network defense is limited to examine local information only due to privacy concerns. To overcome this privacy barrier, we use secure multiparty computation (MPC) for the problem of aggregating network data from multiple domains. We first optimize MPC comparison operations for processing high volume data in near real-time by not enforcing protocols to run in a constant number of synchronization rounds. We then implement a complete set of basic MPC primitives in the SEPIA library. For parallel invocations, SEPIA's basic operations are between 35 and several hundred times faster than those of comparable MPC frameworks. Using these operations, we develop four protocols tailored for distributed network monitoring and security applications: the entropy, distinct count, event correlation, and top-k protocols. Extensive evaluation shows that the protocols are suitable for near real-time data aggregation. For example, our top-k protocol PPTKS accurately aggregates counts for 180,000 distributed IP addresses in only a few minutes. Finally, we use SEPIA with real traffic data from 17 customers of a backbone network to collaboratively detect, analyze, and mitigate distributed anomalies. Our work follows a path starting from theory, going to system design, performance evaluation, and ending with measurement. Along this way, it makes a first effort to bridge two very disparate worlds: MPC theory and network monitoring and security practices. [ABSTRACT FROM AUTHOR]

Recent studies have shown that network coding can provide significant benefits to network protocols, such as increased throughput, reduced network congestion, higher reliability, and lower power consumption. The core principle of network coding is that intermediate nodes actively mix input packets to produce output packets. This mixing subjects network coding systems to a severe security threat, known as a pollution attack, where attacker nodes inject corrupted packets into the network. Corrupted packets propagate in an epidemic manner, depleting network resources and significantly decreasing throughput. Pollution attacks are particularly dangerous in wireless networks, where attackers can easily inject packets or compromise devices due to the increased network vulnerability. In this article, we address pollution attacks against network coding systems in wireless mesh networks. We demonstrate that previous solutions are impractical in wireless networks, incurring an unacceptable high degradation of throughput. We propose a lightweight scheme, DART, that uses time-based authentication in combination with random linear transformations to defend against pollution attacks. We further improve system performance and propose EDART, which enhances DART with an optimistic forwarding scheme. We also propose efficient attacker identification schemes for both DART and EDART that enable quick attacker isolation and the selection of attacker-free paths, achieving additional performance improvement. A detailed security analysis shows that the probability of a polluted packet passing our verification procedure is very low (less than 0.002% in typical settings). Performance results using the well-known MORE protocol and realistic link quality measurements from the Roofnet experimental testbed show that our schemes improve system performance over 20 times compared with previous solutions. [ABSTRACT FROM AUTHOR]

We propose a lightweight RFID authentication protocol that supports forward and backward security. The only cryptographic mechanism that this protocol uses is a pseudorandom number generator (PRNG) that is shared with the backend Server. Authentication is achieved by exchanging a few numbers (3 or 5) drawn from the PRNG. The lookup time is constant, and the protocol can be easily adapted to prevent online man-in-the-middle relay attacks. Security is proven in the UC security framework. [ABSTRACT FROM AUTHOR]

The use of privacy-enhancing cryptographic protocols, such as anonymous credentials and oblivious transfer, could have a detrimental effect on the ability of providers to effectively implement access controls on their content. In this article, we propose a stateful anonymous credential system that allows the provider to implement nontrivial, real-world access controls on oblivious protocols conducted with anonymous users. Our system models the behavior of users as a state machine and embeds that state within an anonymous credential to restrict access to resources based on the state information. The use of state machine models of user behavior allows the provider to restrict the users' actions according to a wide variety of access control models without learning anything about the users' identities or actions. Our system is secure in the standard model under basic assumptions and, after an initial setup phase, each transaction requires only constant time. As a concrete example, we show how to implement the Brewer-Nash (Chinese Wall) and Bell-La Padula (Multilevel Security) access control models within our credential system. Furthermore, we combine our credential system with an adaptive oblivious transfer scheme to create a privacy-friendly oblivious database with strong access controls. [ABSTRACT FROM AUTHOR]

Wireless self-organizing networks (WSONs) have attracted considerable attention from the network research community; however, the key for their success is the rigorous validation of the properties of the network protocols. Applications of risk or those demanding precision (like alert-based systems) require a rigorous and reliable validation of deployed network protocols. While the main goal is to ensure the reliability of the protocols, validation techniques also allow the establishment of their correctness regarding the related protocols' requirements. Nevertheless, even if different communities have carried out intensive research activities on the validation domain, WSONs still raise new issues for and challenging constraints to these communities. We thus, advocate the use of complementary techniques coming from different research communities to efficiently address the validation of WSON protocols. The goal of this tutorial is to present a comprehensive review of the literature on protocol engineering techniques and to discuss difficulties imposed by the characteristics of WSONs on the protocol engineering community. Following the formal and nonformal classification of techniques, we provide a discussion about components and similarities of existing protocol validation approaches. We also investigate how to take advantage of such similarities to obtain complementary techniques and outline new challenges. [ABSTRACT FROM AUTHOR]

In this article, we propose an access control mechanism for Web-based social networks, which adopts a rule-based approach for specifying access policies on the resources owned by network participants, and where authorized users are denoted in terms of the type, depth, and trust level of the relationships existing between nodes in the network. Different from traditional access control systems, our mechanism makes use of a semidecentralized architecture, where access control enforcement is carried out client-side. Access to a resource is granted when the requestor is able to demonstrate being authorized to do that by providing a proof. In the article, besides illustrating the main notions on which our access control model relies, we present all the protocols underlying our system and a performance study of the implemented prototype. [ABSTRACT FROM AUTHOR]

We show that the insecurity problem for protocols with modular exponentiation and arbitrary products allowed in exponents is NP-complete. This result is based on a protocol and intruder model which is powerful enough to uncover known attacks on the Authenticated Group Diffie-Hellman (A-GDH.2) protocol suite. To prove our results, we develop a general framework in which the Dolev-Yao intruder is extended by generic intruder rules. This framework is also applied to obtain complexity results for protocols with commuting public key encryption. [ABSTRACT FROM AUTHOR]

The cryptographic protocols that we use in everyday life rely on the secure storage of keys in consumer devices. Protecting these keys from invasive attackers, who open a device to steal its key, is a challenging problem. We propose controlled physical random functions (CPUFs) as an alternative to storing keys and describe the core protocols that are needed to use CPUFs. A physical random functions (PUF) is a physical system with an input and output. The functional relationship between input and output looks like that of a random function. The particular relationship is unique to a specific instance of a PUF, hence, one needs access to a particular PUF instance to evaluate the function it embodies. The cryptographic applications of a PUF are quite limited unless the PUF is combined with an algorithm that limits the ways in which the PUF can be evaluated; this is a CPUF. A major difficulty in using CPUFs is that you can only know a small set of outputs of the PUF—the unknown outputs being unrelated to the known ones. We present protocols that get around this difficulty and allow a chain of trust to be established between the CPUF manufacturer and a party that wishes to interact securely with the PUF device. We also present some elementary applications, such as certified execution. [ABSTRACT FROM AUTHOR]

It is well known that the Border Gateway Protocol (BGP), the IETF standard interdomain routing protocol, is vulnerable to a variety of attacks, and that a single misconfigured or malicious BGP speaker could result in large-scale service disruption. In this paper, we present Pretty Secure BGP (psBGP)—a proposal for securing BGP, including an architectural overview, design details for significant aspects, and preliminary security and operational analysis. psBGP differs from other security proposals (e.g., S-BGP and soBGP) in that it makes use of a single-level PKI for AS number authentication, a decentralized trust model for verifying the propriety of IP prefix origin, and a rating-based stepwise approach for AS-PATH (integrity) verification. psBGP trades off the strong security guarantees of S-BGP for presumed-simpler operation, e.g., using a PIG with a simple structure, with a small number of certificate types, and of manageable size. psBGP is designed to successfully defend against various (nonmalicious and malicious) threats from uncoordinated BGP speakers, and to be incrementally deployed with incremental benefits. [ABSTRACT FROM AUTHOR]

APSS, a proactive secret sharing (P55) protocol for asynchronous systems, is explained and proved correct. The protocol enables a set of secret shares to be periodically refreshed with a new, independent set, thereby thwarting mobile-adversary attacks. Protocols for asynchronous systems are inherently less vulnerable to denial-of-service attacks, which slow processor execution or delay message delivery. So APSS tolerates certain attacks that PSS protocols for synchronous systems cannot. [ABSTRACT FROM AUTHOR]

Security protocols are one of the most critical elements in enabling the secure communication and processing of information. The presence of flaws in published protocols highlights the complexity of security protocol design. Only formal verification can provide strong confidence in the correctness of security protocols and is considered an imperative step in their design. This paper presents a new theoretical concept, called Layered Proving Trees, for automatically applying logical postulates in logic-based security protocol verification. An algorithm for the new concept is introduced and the soundness and completeness of the technique is proved. Empirical results on the performance of the algorithm are presented. The presented proofs and empirical results demonstrate the feasibility and effectiveness of the Layered Proving Tree approach. [ABSTRACT FROM AUTHOR]

Group key agreement is a fundamental building block for secure peer group communication systems. Several group key management techniques were proposed in the last decade, all assuming the existence of an underlying group communication infrastructure to provide reliable and ordered message delivery as well as group membership information. Despite analysis, implementation, and deployment of some of these techniques, the actual costs associated with group key management have been poorly understood so far. This resulted in an undesirable tendency: on the one hand, adopting suboptimal security for reliable group communication, while, on the other hand, constructing excessively costly group key management protocols. This paper presents a thorough performance evaluation of five notable distributed key management techniques (for collaborative peer groups) integrated with a reliable group communication system. An in-depth comparison and analysis of the five techniques is presented based on experimental results obtained in actual local- and wide-area networks. The extensive performance measurement experiments conducted for all methods offer insights into their scalability and practicality. Furthermore, our analysis of the experimental results highlights several observations that are not obvious from the theoretical analysis. [ABSTRACT FROM AUTHOR]

In this paper, we present a practical key recovery attack on WEP, the link-layer security protocol for 802.1lb wireless networks. The attack is based on a partial key exposure vulnerability in the RC4 stream cipher discovered by Fluhrer, Mantin, and Shamir. This paper describes how to apply this flaw to breaking WEP, our implementation of the attack, and optimizations that can be used to reduce the number of packets required for the attack. We conclude that the 802.1lb WEP standard is completely insecure, and we provide recommendations on how this vulnerability could be mitigated and repaired. [ABSTRACT FROM AUTHOR]

Secure and reliable group communication is an active area of research. Its popularity is fueled by the growing importance of group-oriented and collaborative applications. The central research challenge is secure and efficient group key management. While centralized methods are often appropriate for key distribution in large multicast-style groups, many collaborative group settings require distributed key agreement techniques. This work investigates a novel group key agreement approach which blends key trees with Diffie­Hellman key exchange. It yields a secure protocol suite called Tree-based Group Diffie­Heliman (TGDH) that is both simple and fault-tolerant. Moreover, the efficiency of TGDH appreciably surpasses that of prior art. [ABSTRACT FROM AUTHOR]

In this paper we study privacy issues regarding the use of the SSL/TLS protocol and X.509 certificates. Our main attention is placed on subscription-based remote services (e.g., subscription to newspapers and databases) where the service manager charges a fiat fee for a period of time independent of the actual number of times the service is requested. We start by pointing out that restricting the access to such services by using X.509 certificates and the SSL/TLS protocol, while preserving the interests of the service managers, neglects the right to privacy of the users. We then propose the concept of a crypto certificate and the Secure and Private Socket Layer protocol (SPSL protocol, in short) and show how they can be used to preserve user privacy and, at the same time, protecting the interests of the service managers. The SPSL protocol only requires the user to have a standard X.509 certificate (with an RSA key) and does not require the user to get any special ad hoc certificate. Finally, we show the viability of the proposed solution by describing a system based on SPSL for secure and private access to subscription-based web services. Our implementation includes an SPSL proxy for a TLS-enabled web client and a module for the Apache web server along with administrative tools for the server side. The system has been developed starting from the implementation of an API for the SPSL protocol that we describe in the paper. [ABSTRACT FROM AUTHOR]

There is increasing growth in the number of computer networks in use and in the kinds of distributed computing applications available on these networks. This increase, together with concern about privacy, security, and integrity of information exchange, has created considerable interest in the use of encryption to protect information in the networks. This survey is directed at the reader who is knowledgeable about various network designs and who now wishes to consider incorporating encryption methods into these designs. It is also directed at developers of encryption algorithms who wish to understand the characteristics of such algorithms useful in network applications. Key management, network encryption protocols, digital signatures, and the utility of conventional-or public-key encryption methods are each discussed. A case study of how encryption was integrated into an actual network, the Arpanet, illustrates many issues present in the design of a network encryption facility. [ABSTRACT FROM AUTHOR]