Skip to main content

2010 | Buch

Computer Security – ESORICS 2010

15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010. Proceedings

herausgegeben von: Dimitris Gritzalis, Bart Preneel, Marianthi Theoharidou

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

insite
SUCHEN

Über dieses Buch

The EuropeanSymposium on Researchin Computer Security (ESORICS) has a tradition that goes back two decades. It tries to bring together the international research community in a top-quality event that covers all the areas of computer security, ranging from theory to applications. ESORICS 2010 was the 15th edition of the event. It was held in Athens, Greece, September 20-22, 2010. The conference received 201 submissions. The papers went through a careful review process. In a ?rst round, each paper - ceived three independent reviews. For the majority of the papers an electronic discussion was also organized to arrive at the ?nal decision. As a result of the review process, 42 papers were selected for the ?nal program, resulting in an - ceptance rate of as low as 21%. The authors of accepted papers were requested to revise their papers, based on the comments received. The program was c- pleted with an invited talk by Udo Helmbrecht, Executive Director of ENISA (European Network and Information Security Agency). ESORICS 2010 was organized under the aegisof three Ministries of the G- ernment of Greece, namely: (a) the Ministry of Infrastructure, Transport, and Networks, (b) the General Secretariat for Information Systems of the Ministry of Economy and Finance, and (c) the General Secretariat for e-Governance of the Ministry of Interior, Decentralization, and e-Government.

Inhaltsverzeichnis

Frontmatter

RFID and Privacy

A New Framework for RFID Privacy

Formal RFID security and privacy frameworks are fundamental to the design and analysis of robust RFID systems. In this paper, we develop a new definitional framework for RFID privacy in a rigorous and precise manner. Our framework is based on a zero-knowledge (ZK) formulation [8,6] and incorporates the notions of adaptive completeness and mutual authentication. We provide meticulous justification of the new framework and contrast it with existing ones in the literature. In particular, we prove that our framework is strictly stronger than the ind-privacy model of [18], which answers an open question posed in [18] for developing stronger RFID privacy models. We also clarify certain confusions and rectify several defects in the existing frameworks. Finally, based on the protocol of [20], we propose an efficient RFID mutual authentication protocol and analyze its security and privacy. The methodology used in our analysis can also be applied to analyze other RFID protocols within the new framework.

Robert H. Deng, Yingjiu Li, Moti Yung, Yunlei Zhao
Readers Behaving Badly
Reader Revocation in PKI-Based RFID Systems

Recent emergence of RFID tags capable of performing public key operations motivates new RFID applications, including electronic travel documents, identification cards and payment instruments. In this context, public key certificates form the cornerstone of the overall system security. In this paper, we argue that one of the prominent challenges is how to handle revocation and expiration checking of RFID reader certificates. This is an important issue considering that these high-end RFID tags are geared for applications such as e-documents and contactless payment instruments. Furthermore, the problem is unique to public key-based RFID systems, since a passive RFID tag has no clock and thus cannot use (time-based) off-line methods.

In this paper, we address the problem of reader certificate expiration and revocation in PKI-Based RFID systems. We begin by observing an important distinguishing feature of

personal

RFID tags used in authentication, access control or payment applications – the involvement of a human user. We take advantage of the user’s awareness and presence to construct a simple, efficient, secure and (most importantly) feasible solution. We evaluate the usability and practical security of our solution via user studies and discuss its feasibility.

Rishab Nithyanand, Gene Tsudik, Ersin Uzun
Privacy-Preserving, Taxable Bank Accounts

Current banking systems do not aim to protect user privacy. Purchases made from a single bank account can be linked to each other by many parties. This could be addressed in a straight-forward way by generating unlinkable credentials from a single master credential using Camenisch and Lysyanskaya’s algorithm; however, if bank accounts are taxable, some report must be made to the tax authority about each account. Assuming a flat-rate taxation mechanism (which can be extended to a progressive one) and using unlinkable credentials, digital cash, and zero knowledge proofs of knowledge, we present a solution that prevents anyone, even the tax authority, from knowing which accounts belong to which users, or from being able to link any account to another or to purchases or deposits.

Elli Androulaki, Binh Vo, Steven Bellovin
Formal Analysis of Privacy for Vehicular Mix-Zones

Safety critical applications for recently proposed vehicle to vehicle ad-hoc networks (VANETs) rely on a beacon signal, which poses a threat to privacy since it could allow a vehicle to be tracked. Mix-zones, where vehicles encrypt their transmissions and then change their identifiers, have been proposed as a solution to this problem.

In this work, we describe a formal analysis of mix-zones. We model a mix-zone and propose a formal definition of privacy for such a zone. We give a set of necessary conditions for any mix-zone protocol to preserve privacy. We analyse, using the tool ProVerif, a particular proposal for key distribution in mix-zones, the CMIX protocol. We show that in many scenarios it does not preserve privacy, and we propose a fix.

Morten Dahl, Stéphanie Delaune, Graham Steel

Software Security

IntPatch: Automatically Fix Integer-Overflow-to-Buffer-Overflow Vulnerability at Compile-Time

The Integer-Overflow-to-Buffer-Overflow (

IO2BO

) vulnerability is an underestimated threat. Automatically identifying and fixing this kind of vulnerability are critical for software security. In this paper, we present the design and implementation of IntPatch, a compiler extension for automatically fixing IO2BO vulnerabilities in C/C++ programs at compile time. IntPatch utilizes classic type theory and dataflow analysis framework to identify potential IO2BO vulnerabilities, and then instruments programs with runtime checks. Moreover, IntPatch provides an interface for programmers to facilitate checking integer overflows. We evaluate IntPatch on a number of real-world applications. It has caught all 46 previously known IO2BO vulnerabilities in our test suite and found 21 new bugs. Applications patched by IntPatch have a negligible runtime performance loss which is averaging about 1%.

Chao Zhang, Tielei Wang, Tao Wei, Yu Chen, Wei Zou
A Theory of Runtime Enforcement, with Results

This paper presents a theory of runtime enforcement based on mechanism models called MRAs (Mandatory Results Automata). MRAs can monitor and transform security-relevant actions and their results. Because previous work could not model monitors transforming results, MRAs capture realistic behaviors outside the scope of previous models. MRAs also have a simple but realistic operational semantics that makes it straightforward to define concrete MRAs. Moreover, the definitions of policies and enforcement with MRAs are significantly simpler and more expressive than those of previous models. Putting all these features together, we argue that MRAs make good general models of runtime mechanisms, upon which a theory of runtime enforcement can be based. We develop some enforceability theory by characterizing the policies MRAs can and cannot enforce.

Jay Ligatti, Srikar Reddy
Enforcing Secure Object Initialization in Java

Sun and the CERT recommend for secure Java development to

not allow partially initialized objects to be accessed

. The CERT considers the severity of the risks taken by not following this recommendation as

high

. The solution currently used to enforce object initialization is to implement a coding pattern proposed by Sun, which is not formally checked. We propose a modular type system to formally specify the initialization policy of libraries or programs and a type checker to statically check at load time that all loaded classes respect the policy. This allows to prove the absence of bugs which have allowed some famous privilege escalations in Java. Our experimental results show that our safe default policy allows to prove 91% of classes of

java.lang

,

java.security

and

javax.security

safe without any annotation and by adding 57 simple annotations we proved all classes but four safe. The type system and its soundness theorem have been formalized and machine checked using Coq.

Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie
Flexible Scheduler-Independent Security

We propose an approach to certify the information flow security of multi-threaded programs independently from the scheduling algorithm. A scheduler-independent verification is desirable because the scheduler is part of the runtime environment and, hence, usually not known when a program is analyzed. Unlike for other system properties, it is not straightforward to achieve scheduler independence when verifying information flow security, and the existing independence results are very restrictive. In this article, we show how some of these restrictions can be overcome. The key insight in our development of a novel scheduler-independent information flow property was the identification of a suitable class of schedulers that covers the most relevant schedulers. The contributions of this article include a novel security property, a scheduler independence result, and a provably sound program analysis.

Heiko Mantel, Henning Sudbrock

Cryptographic Protocols

Secure Multiparty Linear Programming Using Fixed-Point Arithmetic

Collaborative optimization problems can often be modeled as a linear program whose objective function and constraints combine data from several parties. However, important applications of this model (e.g., supply chain planning) involve private data that the parties cannot reveal to each other. Traditional linear programming methods cannot be used in this case. The problem can be solved using cryptographic protocols that compute with private data and preserve data privacy. We present a practical solution using multiparty computation based on secret sharing. The linear programming protocols use a variant of the simplex algorithm and secure computation with fixed-point rational numbers, optimized for this type of application. We present the main protocols as well as performance measurements for an implementation of our solution.

Octavian Catrina, Sebastiaan de Hoogh
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Σ-Protocols

Zero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have a high potential impact, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation are time-consuming and error-prone.

We contribute to overcoming these challenges as follows: We present a comprehensive specification language and a compiler for ZK-PoK protocols based on Σ-protocols. The compiler allows the fully automatic translation of an abstract description of a proof goal into an executable implementation. Moreover, the compiler overcomes various restrictions of previous approaches, e.g., it supports the important class of exponentiation homomorphisms with hidden-order co-domain, needed for privacypreserving applications such as DAA. Finally, our compiler is certifying, in the sense that it automatically produces a formal proof of the soundness of the compiled protocol for a large class of protocols using the Isabelle/HOL theorem prover.

José Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider
Short Generic Transformation to Strongly Unforgeable Signature in the Standard Model

Standard signature schemes are usually devised to merely achieve existential unforgeability, i.e., to prevent forgeries on new messages not previously signed. Unfortunately, existential unforgeability is not suitable for several applications, since a new signature on a previously signed message may be produced. Therefore, there is a need to construct signature schemes with strong unforgeability, that is, it is hard to produce a new signature on any message, even if it has been signed before by legitimate signer. Recently, there have been several generic transformations proposed to convert weak unforgeability into strong unforgeability. For instance, various generic transforms of signatures that are existential unforgeable under adaptive chosen message attack (

uf-cma

) to strongly unforgeable under adaptive chosen message attack (

suf-cma

) have been proposed. Moreover, methods of converting signatures that are existentially unforgeable under generic chosen message attack (

uf-gma

) to

uf-cma

secure digital signatures have also been studied. Combination of these methods yields generic transform of digital signatures offering

uf-gma

security to

suf-cma

security. In this paper, we present a short universal transform that directly converts any

uf-gma

secure signatures into

suf-cma

secure. Our transform is

the shortest generic transformation

, in terms of signature size expansion, which results in

suf-cma

secure signature in the standard model. While our generic transformation can convert any

uf-gma

secure signature to

suf-cma

secure signature directly, the efficiency of ours is comparable to those which only transform signatures from

uf-gma

secure to

uf-cma

secure in the standard model.

Joseph K. Liu, Man Ho Au, Willy Susilo, Jianying Zhou
DR@FT: Efficient Remote Attestation Framework for Dynamic Systems

Remote attestation is an important mechanism to provide the trustworthiness proof of a computing system by verifying its integrity. In this paper, we propose an innovative remote attestation framework called DR@FT for efficiently measuring a target system based on an information flow-based integrity model. With this model, the high integrity processes of a system are first verified through measurements and these processes are then protected from accesses initiated by low integrity processes. Also, our framework verifies the latest state changes in a dynamic system instead of considering the entire system information. In addition, we adopt a graph-based method to represent integrity violations with a ranked violation graph, which supports intuitive reasoning of attestation results. Our experiments and performance evaluation demonstrate the feasibility and practicality of DR@FT.

Wenjuan Xu, Gail-Joon Ahn, Hongxin Hu, Xinwen Zhang, Jean-Pierre Seifert

Traffic Analysis

Website Fingerprinting and Identification Using Ordered Feature Sequences

We consider website fingerprinting over encrypted and proxied channel. It has been shown that information on packet sizes is sufficient to achieve good identification accuracy. Recently, traffic morphing [1] was proposed to thwart website fingerprinting by changing the packet size distribution so as to mimic some other website, while minimizing bandwidth overhead. In this paper, we point out that packet ordering information, though noisy, can be utilized to enhance website fingerprinting. In addition, traces of the ordering information remain even under traffic morphing and they can be extracted for identification. When web access is performed over OpenSSH and 2000 profiled websites, the identification accuracy of our scheme reaches 81%, which is 11% better than Liberatore and Levine’s scheme presented in CCS’06 [2]. We are able to identify 78% of the morphed traffic among 2000 websites while Liberatore and Levine’s scheme identifies only 52%. Our analysis suggests that an effective countermeasure to website fingerprinting should not only hide the packet size distribution, but also aggressively remove the ordering information.

Liming Lu, Ee-Chien Chang, Mun Choon Chan
Web Browser History Detection as a Real-World Privacy Threat

Web browser history detection using CSS

visited

styles has long been dismissed as an issue of marginal impact. However, due to recent changes in Web usage patterns, coupled with browser performance improvements, the long-standing issue has now become a significant threat to the privacy of Internet users.

In this paper we analyze the impact of CSS-based history detection and demonstrate the feasibility of conducting practical attacks with minimal resources. We analyze Web browser behavior and detectability of content loaded via standard protocols and with various HTTP response codes. We develop an algorithm for efficient examination of large link sets and evaluate its performance in modern browsers. Compared to existing methods our approach is up to 6 times faster, and is able to detect up to 30,000 visited links per second.

We present a novel Web application capable of effectively detecting clients’ browsing histories and discuss real-world results obtained from 271,576 Internet users. Our results indicate that at least 76% of Internet users are vulnerable to history detection, including over 94% of Google Chrome users; for a test of most popular Internet websites we were able to detect, on average, 62.6 (median 22) visited locations per client. We also demonstrate the potential to profile users based on social news stories they visited, and to detect private data such as zipcodes or search queries typed into online forms.

Artur Janc, Lukasz Olejnik
On the Secrecy of Spread-Spectrum Flow Watermarks

Spread-spectrum flow watermarks offer an invisible and ready-to-use flow watermarking scheme that can be employed to stealthily correlate the two ends of a network communication. Such technique has wide applications in network security and privacy. Although several methods have been proposed to detect various flow watermarks, few can effectively detect spread-spectrum flow watermarks. Moreover, there is currently no solution that allows end users to eliminate spread-spectrum flow watermarks from their flows

without

the support of a separate network element. In this paper, we propose a novel approach to detect spread-spectrum flow watermarks by leveraging their intrinsic features. Contrary to the common belief that Pseudo-Noise (PN) codes can render flow watermarks invisible, we prove that PN codes actually facilitate their detection. Furthermore, we propose a novel method based on TCP’s flow-control mechanism that provides end users with the ability to autonomously remove spread-spectrum flow watermarks. We conducted extensive experiments on traffic flowing both through one-hop proxies in the PlanetLab network, and through Tor. The experimental results show that the proposed detection system can achieve up to 100% detection rate with zero false positives, and confirm that our elimination system can effectively remove spread-spectrum flow watermarks.

Xiapu Luo, Junjie Zhang, Roberto Perdisci, Wenke Lee
Traffic Analysis against Low-Latency Anonymity Networks Using Available Bandwidth Estimation

We introduce a novel remotely-mounted attack that can expose the network identity of an anonymous client, hidden service, and anonymizing proxies. To achieve this, we employ

single-end controlled

available bandwidth estimation tools and a colluding network entity that can modulate the traffic destined for the victim. To expose the circuit including the source, we inject a number of short or one large burst of traffic. Although timing attacks have been successful against anonymity networks, they require either a

Global Adversary

or the compromise of substantial number of anonymity nodes. Our technique does not require compromise of, or collaboration with,

any

such entity.

To validate our attack, we performed a series of experiments using different network conditions and locations for the adversaries on both controlled and real-world

Tor

circuits. Our results demonstrate that our attack is successful in controlled environments. In real-world scenarios, even an under-provisioned adversary with only a few network vantage points can, under certain conditions, successfully identify the IP address of both Tor users and

Hidden Servers

. However, Tor’s inherent circuit scheduling results in limited quality of service for its users. This at times leads to increased false negatives and it can degrade the performance of our circuit detection. We believe that as high speed anonymity networks become readily available, a well-provisioned adversary, with a partial or inferred network “map”, will be able to partially or fully expose anonymous users.

Sambuddho Chakravarty, Angelos Stavrou, Angelos D. Keromytis

End-User Security

A Hierarchical Adaptive Probabilistic Approach for Zero Hour Phish Detection

Phishing attacks are a significant threat to users of the Internet, causing tremendous economic loss every year. In combating phish, industry relies heavily on manual verification to achieve a low false positive rate, which, however, tends to be slow in responding to the huge volume of unique phishing URLs created by toolkits. Our goal here is to combine the best aspects of human verified blacklists and heuristic-based methods, i.e., the low false positive rate of the former and the broad and fast coverage of the latter. To this end, we present the design and evaluation of a hierarchical blacklist-enhanced phish detection framework. The key insight behind our detection algorithm is to leverage existing human-verified blacklists and apply the shingling technique, a popular near-duplicate detection algorithm used by search engines, to detect phish in a probabilistic fashion with very high accuracy. To achieve an extremely low false positive rate, we use a filtering module in our layered system, harnessing the power of search engines via information retrieval techniques to correct false positives. Comprehensive experiments over a diverse spectrum of data sources show that our method achieves 0% false positive rate (FP) with a true positive rate (TP) of 67.15% using search-oriented filtering, and 0.03% FP and 73.53% TP without the filtering module. With incremental model building capability via a sliding window mechanism, our approach is able to adapt quickly to new phishing variants, and is thus more responsive to the evolving attacks.

Guang Xiang, Bryan A. Pendleton, Jason Hong, Carolyn P. Rose
Kamouflage: Loss-Resistant Password Management

We introduce Kamouflage: a new architecture for building theft-resistant password managers. An attacker who steals a laptop or cell phone with a Kamouflage-based password manager is forced to carry out a considerable amount of online work before obtaining any user credentials. We implemented our proposal as a replacement for the built-in Firefox password manager, and provide performance measurements and the results from experiments with large real-world password sets to evaluate the feasibility and effectiveness of our approach. Kamouflage is well suited to become a standard architecture for password managers on mobile devices.

Hristo Bojinov, Elie Bursztein, Xavier Boyen, Dan Boneh

Formal Analysis

Sequential Protocol Composition in Maude-NPA

Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified separately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification. Moreover, we show that, by a simple protocol transformation, we are able to analyze and verify this dynamic composition in the current Maude-NPA tool. We prove soundness and completeness of the protocol transformation with respect to the extended operational semantics, and illustrate our results on some examples.

Santiago Escobar, Catherine Meadows, José Meseguer, Sonia Santiago
Verifying Security Property of Peer-to-Peer Systems Using CSP

Due to their nature, Peer-to-Peer (P2P) systems are subject to a wide range of security issues. In this paper, we focus on a specific security property, called the

root authenticity

(or RA) property of the so-called structured P2P overlays. We propose a P2P architecture that uses Trusted Computing as the security mechanism. We formalize that system using a process algebra (CSP), then verify that it indeed meets the RA property.

Tien Tuan Anh Dinh, Mark Ryan
Modeling and Analyzing Security in the Presence of Compromising Adversaries

We present a framework for modeling adversaries in security protocol analysis, ranging from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals’ states during protocol execution. Our adversary models unify and generalize many existing security notions from both the computational and symbolic settings. We extend an existing symbolic protocol-verification tool with our adversary models, resulting in the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.

David Basin, Cas Cremers
On Bounding Problems of Quantitative Information Flow

Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the “bounding problem” of quantitative information flow, defined as follows: Given a program

M

and a positive real number

q

, decide if the quantitative information flow of

M

is less than or equal to

q

. We prove that the bounding problem is not a

k

-safety property for any

k

(even when

q

is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free boolean programs. Specifically, we show that the problem is PP-hard for all the definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.

Hirotoshi Yasuoka, Tachio Terauchi

E-voting and Broadcast

On E-Vote Integrity in the Case of Malicious Voter Computers

Norway has started to implement e-voting (over the Internet, and by using voters’ own computers) within the next few years. The vulnerability of voter’s computers was identified as a serious threat to e-voting. In this paper, we study the vote integrity of e-voting when the voter computers cannot be trusted. First, we make a number of assumptions about the available infrastructure. In particular, we assume the existence of two out-of-band channels that do not depend on the voter computers. The first channel is used to transmit integrity check codes to the voters prior the election, and the second channel is used to transmit a check code, that corresponds to her vote, back to a voter just after his or her e-vote vast cast. For this we also introduce a new cryptographic protocol. We present the new protocol with enough details to facilitate an implementation, and also present the timings of an actual implementation.

Sven Heiberg, Helger Lipmaa, Filip van Laenen
Election Verifiability in Electronic Voting Protocols

We present a formal, symbolic definition of election verifiability for electronic voting protocols in the context of the applied pi calculus. Our definition is given in terms of boolean tests which can be performed on the data produced by an election. The definition distinguishes three aspects of verifiability: individual, universal and eligibility verifiability. It also allows us to determine precisely which aspects of the system’s hardware and software must be trusted for the purpose of election verifiability. In contrast with earlier work our definition is compatible with a large class of electronic voting schemes, including those based on blind signatures, homomorphic encryption and mixnets. We demonstrate the applicability of our formalism by analysing three protocols: FOO, Helios 2.0, and Civitas (the latter two have been deployed).

Steve Kremer, Mark Ryan, Ben Smyth
Pretty Good Democracy for More Expressive Voting Schemes

In this paper we revisit

Pretty Good Democracy

, a scheme for verifiable Internet voting from untrusted client machines. The original scheme was designed for first-past-the-post elections. Here, we show how Pretty Good Democracy can be extended to voting schemes in which the voter lists the candidates in their order of preference. Our scheme applies to elections using STV, IRV, Borda, or any other tallying scheme in which a vote is a list of candidates in preference order. We also describe an extension to cover Approval or Range voting.

James Heather, Peter Y. A. Ryan, Vanessa Teague
Efficient Multi-dimensional Key Management in Broadcast Services

The prevalent nature of Internet makes it a well suitable medium for many new types of services such as location-based services and streaming content. Subscribers to such services normally receive encrypted content and can obtain access to it if they possess the corresponding decryption key. Furthermore, in location-based services a subscription is normally granted to a geographic area specified by user-specific coordinates (

x

1

,

x

2

), (

y

1

,

y

2

) and custom time interval (

t

1

,

t

2

). Similarly, subscriptions to other services also involve multiple dimensions. The problem of key management is then to assign keys to each point on a

D

-dimensional grid and to subscribers in such a way as to permit all users to obtain access only to the resources in their subscriptions and minimize the associated overhead. In this work, we develop a novel key management scheme for multi-dimensional subscriptions that both outperforms existing solutions and supports a richer set of access privileges than existing schemes. Our scheme is provably secure under the Decision Linear Diffie-Hellman Assumption.

Marina Blanton, Keith B. Frikken

Authentication, Access Control, Authorization and Attestation

Caught in the Maze of Security Standards

We analyze the interactions between several national and international standards relevant for eCard applications, noting deficiencies in those standards, or at least deficiencies in the documentation of their dependencies. We show that smart card protocols are currently specified in a way that standard compliant protocol implementations may be vulnerable to attacks. We further show that attempts to upgrade security by increasing the length of cryptographic keys may fail when message formats in protocols are not re-examined at the same time. We argue that the entities responsible for accrediting smart card based applications thus require security expertise beyond the knowledge encoded in security standards and that a purely compliance based certification of eCard applications is insufficient.

Jan Meier, Dieter Gollmann
User-Role Reachability Analysis of Evolving Administrative Role Based Access Control

Role Based Access Control (RBAC) has been widely used for restricting resource access to only authorized users. Administrative Role Based Access Control (ARBAC) specifies permissions for administrators to change RBAC policies. Due to complex interactions between changes made by different administrators, it is often difficult to comprehend the full effect of ARBAC policies by manual inspection alone. Policy analysis helps administrators detect potential flaws in the policy specification.

Prior work on ARBAC policy analysis considers only static ARBAC policies. In practice, ARBAC policies tend to change over time in order to fix design flaws or to cope with the changing requirements of an organization. Changes to ARBAC policies may invalidate security properties that were previously satisfied. In this paper, we present incremental algorithms for user-role reachability analysis of ARBAC policies, which asks whether a given user can be assigned to given roles by given administrators. Our incremental algorithms determine if a change may affect the analysis result, and if so, use the information of the previous analysis to incrementally update the analysis result. To the best of our knowledge, these are the first known incremental algorithms in literature for ARBAC analysis. Detailed evaluations show that our incremental algorithms outperform the non-incremental algorithm in terms of execution time.

Mikhail I. Gofman, Ruiqi Luo, Ping Yang
An Authorization Framework Resilient to Policy Evaluation Failures

In distributed computer systems, it is possible that the evaluation of an authorization policy may suffer unexpected failures, perhaps because a sub-policy cannot be evaluated or a sub-policy cannot be retrieved from some remote repository. Ideally, policy evaluation should be resilient to such failures and, at the very least, fail “gracefully” if no decision can be computed. We define syntax and semantics for an XACML-like policy language. The semantics are incremental and reflect different assumptions about the manner in which failures can occur. Unlike XACML, our language uses simple

binary

operators to combine sub-policy decisions. This enables us to characterize those few binary operators likely to be used in practice, and hence to identify a number of strategies for optimizing policy evaluation and policy representation.

Jason Crampton, Michael Huth
Optimistic Fair Exchange with Multiple Arbiters

Fair exchange is one of the most fundamental problems in secure distributed computation. Alice has something that Bob wants, and Bob has something that Alice wants. A fair exchange protocol would guarantee that, even if one of them maliciously deviates from the protocol, either both of them get the desired content, or neither of them do. It is known that no two-party protocol can guarantee fairness in general; therefore the presence of a trusted

arbiter

is necessary. In optimistic fair exchange, the arbiter only gets involved in case of faults, but needs to be trusted. To reduce the trust put in the arbiter, it is natural to consider employing multiple arbiters.

Expensive techniques like byzantine agreement or secure multi-party computation with Ω(

n

2

) communication can be applied to distribute arbiters in a non-autonomous way. Yet we are interested in efficient protocols that can be achieved by keeping the arbiters autonomous (non-communicating), especially for p2p settings in which the arbiters do not even know each other. Avoine and Vaudenay [6] employ multiple autonomous arbiters in their optimistic fair exchange protocol which uses global timeout mechanisms; all arbiters have access to -loosely- synchronized clocks. They left two open questions regarding the use of distributed autonomous arbiters: (1) Can an optimistic fair exchange protocol without timeouts provide fairness (since it is hard to achieve synchronization in a p2p setting) when employing multiple autonomous arbiters? (2) Can any other optimistic fair exchange protocol with timeouts achieve better bounds on the number of honest arbiters required? In this paper, we answer both questions negatively. To answer these questions, we define a general class of optimistic fair exchange protocols with multiple arbiters, called “distributed arbiter fair exchange” (DAFE) protocols. Informally, in a DAFE protocol, if a participant fails to send a correctly formed message, the other party must contact some subset of the arbiters and get correctly formed responses from them. The arbiters do not communicate with each other, but only to Alice and Bob. We prove that no DAFE protocol can meaningfully exist.

Alptekin Küpçü, Anna Lysyanskaya

Anonymity and Unlinkability

Speaker Recognition in Encrypted Voice Streams

Transmitting voice communication over untrusted networks puts personal information at risk. Although voice streams are typically encrypted to prevent unwanted eavesdropping, additional features of voice communication protocols might still allow eavesdroppers to discover information on the transmitted content and the speaker.

We develop a novel approach for unveiling the identity of speakers who participate in encrypted voice communication, solely by eavesdropping on the encrypted traffic. Our approach exploits the concept of voice activity detection (VAD), a widely used technique for reducing the bandwidth consumption of voice traffic. We show that the reduction of traffic caused by VAD techniques creates patterns in the encrypted traffic, which in turn reveal the patterns of pauses in the underlying voice stream. We show that these patterns are speaker-characteristic, and that they are sufficient to undermine the anonymity of the speaker in encrypted voice communication. In an empirical setup with 20 speakers our analysis is able to correctly identify an unknown speaker in about 48% of all cases. Our work extends and generalizes existing work that exploits variable bit-rate encoding for identifying the conversation language and content of encrypted voice streams.

Michael Backes, Goran Doychev, Markus Dürmuth, Boris Köpf
Evaluating Adversarial Partitions

In this paper, we introduce a framework for measuring unlinkability both per subject and for an entire system. The framework enables the evaluator to attach different sensitivities to individual items in the system, and to specify the severity of different types of error that an adversary can make. These parameters, as well as a threshold that defines what constitutes a privacy breach, may be varied for each subject in the system; the framework respects and combines these potentially differing parametrisations. It also makes use of graphs in a way that results in

intuitive

feedback of different levels of detail. We exhibit the behaviour of our measures in two experimental settings, namely that of adversaries that output randomly chosen partitions, and that of adversaries that launch attacks of different effectiveness.

Andreas Pashalidis, Stefan Schiffner
Providing Mobile Users’ Anonymity in Hybrid Networks

We present a novel hybrid communication protocol that guarantees mobile users’

k

-anonymity against a wide-range of adversaries by exploiting the capability of handheld devices to connect to both WiFi and cellular networks. Unlike existing anonymity schemes, we consider all parties that can intercept communications between the mobile user and a server as potential privacy threats. We formally quantify the privacy exposure and the protection of our system in the presence of malicious neighboring peers, global WiFi eavesdroppers, and omniscient mobile network operators. We show how our system provides an automatic incentive for users to collaborate, since by forwarding packets for other peers users gain anonymity for their own traffic.

Claudio A. Ardagna, Sushil Jajodia, Pierangela Samarati, Angelos Stavrou
Complexity of Anonymity for Security Protocols

Anonymity, as an instance of information hiding, is one of the security properties intensively studied nowadays due to its applications to various fields such as e-voting, e-commerce, e-mail, e -cash, and so on. In this paper we study the decidability and complexity status of the anonymity property in security protocols. We show that anonymity is undecidable for unrestricted security protocols, is NEXPTIME-complete for bounded security protocols, and it is NP-complete for 1-session bounded security protocols. In order to reach these objectives, an epistemic language and logic to reason about anonymity properties for security protocols under an active intruder, are provided. Agent states are endowed with facts derived from actions performed by agents in protocol executions, and an inference system is provided. To define anonymity, an observational equivalence is used, which is shown to be decidable in deterministic polynomial time.

Ferucio Laurenţiu Ţiplea, Loredana Vamanu, Cosmin Vârlan

Network Security and Economics

k-Zero Day Safety: Measuring the Security Risk of Networks against Unknown Attacks

The security risk of a network against unknown zero day attacks has been considered as something unmeasurable since software flaws are less predictable than hardware faults and the process of finding such flaws and developing exploits seems to be chaotic [10]. In this paper, we propose a novel security metric,

k-zero day safety

, based on the number of unknown zero day vulnerabilities. That is, the metric simply counts how many unknown vulnerabilities would be required for compromising a network asset, regardless of what vulnerabilities those might be. We formally define the metric based on an abstract model of networks and attacks. We then devise algorithms for computing the metric. Finally, we show the metric can quantify many existing practices in hardening a network.

Lingyu Wang, Sushil Jajodia, Anoop Singhal, Steven Noel
Are Security Experts Useful? Bayesian Nash Equilibria for Network Security Games with Limited Information

A common assumption in security research is that more individual expertise unambiguously leads to a more secure overall network. We present a game-theoretic model in which this common assumption does not hold. Our findings indicate that expert users can be not only invaluable contributors, but also free-riders, defectors, and narcissistic opportunists. A direct application is that user education needs to highlight the cooperative nature of security, and foster the community sense, in particular, of higher skilled computer users.

As a technical contribution, this paper represents, to our knowledge, the first formal study to quantitatively assess the impact of different degrees of information security expertise on the overall security of a network.

Benjamin Johnson, Jens Grossklags, Nicolas Christin, John Chuang
RatFish: A File Sharing Protocol Provably Secure against Rational Users

The proliferation of P2P computing has recently been propelled by popular applications, most notably file sharing protocols such as BitTorrent. These protocols provide remarkable efficiency and scalability, as well as adaptivity to dynamic situations. However, none of them is secure against attacks from rational users, i.e., users that misuse the protocol if doing so increases their benefits (e.g., reduces download time or amount of upload capacity).

We propose a rigorous model of rational file sharing for both seeders and leechers, building upon the concept of rational cryptography. We design a novel file sharing protocol called RatFish, and we formally prove that no rational party has an incentive to deviate from RatFish; i.e., RatFish constitutes a Nash equilibrium. Compared to existing file sharing protocols such as BitTorrent, the tracker in RatFish is assigned additional tasks while the communication overhead of a RatFish client is kept to a minimum. We demonstrate by means of a prototype implementation that RatFish is practical and efficient.

Michael Backes, Oana Ciobotaru, Anton Krohmer
A Service Dependency Model for Cost-Sensitive Intrusion Response

Recent advances in intrusion detection and prevention have brought promising solutions to enhance

IT

security. Despite these efforts, the battle with cyber attackers has reached a deadlock. While attackers always try to unveil new vulnerabilities, security experts are bounded to keep their softwares compliant with the latest updates. Intrusion response systems are thus relegated to a second rank because no one trusts them to modify system configuration during runtime.

Current response cost evaluation techniques do not cover all impact aspects, favoring availability over confidentiality and integrity. They do not profit from the findings in intrusion prevention which led to powerful models including vulnerability graphs, exploit graphs, etc. This paper bridges the gap between these models and service dependency models that are used for response evaluation. It proposes a new service dependency representation that enables intrusion and response impact evaluation. The outcome is a service dependency model and a complete methodology to use this model in order to evaluate intrusion and response costs. The latter covers response collateral damages and positive response effects as they reduce intrusion costs.

Nizar Kheir, Nora Cuppens-Boulahia, Frédéric Cuppens, Hervé Debar

Secure Update, DOS and Intrustion Detection

Secure Code Update for Embedded Devices via Proofs of Secure Erasure

Remote attestation is the process of verifying internal state of a remote embedded device. It is an important component of many security protocols and applications. Although previously proposed remote attestation techniques assisted by specialized secure hardware are effective, they not yet viable for low-cost embedded devices. One notable alternative is software-based attestation, that is both less costly and more efficient. However, recent results identified weaknesses in some proposed software-based methods, thus showing that security of remote software attestation remains a challenge.

Inspired by these developments, this paper explores an approach that relies neither on secure hardware nor on tight timing constraints typical of software-based technqiques. By taking advantage of the bounded memory/storage model of low-cost embedded devices and assuming a small amount of read-only memory (ROM), our approach involves a new primitive – Proofs of Secure Erasure (PoSE-s). We also show that, even though it is effective and provably secure, PoSE-based attestation is not cheap. However, it is particularly well-suited and practical for two other related tasks: secure code update and secure memory/storage erasure. We consider several flavors of PoSE-based protocols and demonstrate their feasibility in the context of existing commodity embedded devices.

Daniele Perito, Gene Tsudik
D(e|i)aling with VoIP: Robust Prevention of DIAL Attacks

We carry out attacks using Internet services that aim to keep telephone devices busy, hindering legitimate callers from gaining access. We use the term

DIAL (Digitally Initiated Abuse of teLephones)

, or, in the simple form,

Dial attack

, to refer to this behavior. We develop a simulation environment for modeling a Dial attack in order to quantify its full potential and measure the effect of attack parameters. Based on the simulation’s results we perform the attack in the real-world. By using a Voice over IP (VoIP) provider as the attack medium, we manage to hold an existing landline device busy for 85% of the attack duration by issuing only 3 calls per second and, thus, render the device unusable. The attack has zero financial cost, requires negligible computational resources and cannot be traced back to the attacker. Furthermore, the nature of the attack is such that anyone can launch a Dial attack towards any telephone device.

Our investigation of existing countermeasures in VoIP providers shows that they follow an

all-or-nothing

approach, but most importantly, that their anomaly detection systems react slowly against our attacks, as we managed to issue tens of thousands of calls before getting spotted. To cope with this, we propose a flexible anomaly detection system for VoIP calls, which promotes fairness for callers. With our system in place it is hard for an adversary to keep the device busy for more than 5% of the duration of the attack.

Alexandros Kapravelos, Iasonas Polakis, Elias Athanasopoulos, Sotiris Ioannidis, Evangelos P. Markatos
Low-Cost Client Puzzles Based on Modular Exponentiation

Client puzzles have been proposed as a useful mechanism for mitigating Denial of Service attacks on network protocols. While several puzzles have been proposed in recent years, most existing non-parallelizable puzzles are based on modular exponentiations. The main drawback of these puzzles is in the high cost that they incur on the puzzle generator (the verifier). In this paper, we propose cryptographic puzzles based on modular exponentiation that reduce this overhead. Our constructions are based on a reasonable intractability assumption in RSA: essentially the difficulty of computing a small private exponent when the public key is larger by several orders of magnitude than the semi-prime modulus. We also discuss puzzle constructions based on CRT-RSA [11]. Given a semi-prime modulus

N

, the costs incurred on the verifier in our puzzle are decreased by a factor of

${{|N|}\over{k}}$

when compared to existing modular exponentiation puzzles, where

k

is a security parameter. We further show how our puzzle can be integrated in a number of protocols, including those used for the remote verification of computing performance of devices and for the protection against Denial of Service attacks. We validate the performance of our puzzle on PlanetLab nodes.

Ghassan O. Karame, Srdjan Čapkun
Expressive, Efficient and Obfuscation Resilient Behavior Based IDS

Behavior based intrusion detection systems (BIDS) offer the only effective solution against modern malware. While dynamic BIDS have obvious advantages, their success hinges upon three interrelated factors: signature expressiveness, vulnerability to behavioral obfuscation and run-time efficiency of signature matching. To achieve higher signature expressiveness, a new approach for formal specification of the malicious functionalities based on abstract activity diagrams (AD) which incorporate multiple realizations of the specified functionality. We analyzed both inter and intra-process behavioral obfuscation techniques that can compromise existing BIDS. As a solution, we proposed specification generalization that implies augmenting (generalizing) otherwise obfuscation prone specification into more generic, obfuscation resilient specification. We suggest colored Petri nets as a basis for functionality recognition at the system call level. We implemented a prototype IDS that has been evaluated on malicious and legitimate programs. The experimental results indicated extremely low false positives and negatives. Moreover, the IDS shows very low execution overhead and negligible overhead penalty due to antiobfuscation generalization.

Arnur G. Tokhtabayev, Victor A. Skormin, Andrey M. Dolgikh
Backmatter
Metadaten
Titel
Computer Security – ESORICS 2010
herausgegeben von
Dimitris Gritzalis
Bart Preneel
Marianthi Theoharidou
Copyright-Jahr
2010
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-15497-3
Print ISBN
978-3-642-15496-6
DOI
https://doi.org/10.1007/978-3-642-15497-3