%0 Conference Proceedings
%A Backes, Michael
%A Pfitzmann, Birgit
%T Computational Probabilistic Non-interference
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 1-23
%F Crypto
%X In recent times information flow and non-interference have become very popular concepts for expressing both integrity and privacy properties. We present the first general definition of probabilistic non-interference in reactive systems which includes a computational case. This case is essential to cope with real cryptography since non-interference properties can usually only be guaranteed if the underlying cryptographic primitives have not been broken. This might happen, but only with negligible probability. Furthermore, our definition links non-interference with the common approach of simulatability that modern cryptography often uses. We show that our definition is maintained under simulatability, which allows secure composition of systems, and we present a general strategy how cryptographic primitives can be included in information flow proofs. As an example we present an abstract specification and a possible implementation of a cryptographic firewall guarding two honest users from their environment.

%0 Conference Proceedings
%A Kurosawa, Kaoru
%A Ogata, Wakaha
%T Bit Slice Auction Circuit
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 24-38
%F Crypto
%K auction, multiparty protocol, bit-slice, circuit, mix and match
%X In this paper, we introduce a bit-slice approach for auctions and present a more efficient circuit than the normal approach for the highest-price auction. Our circuit can be combined with any auction protocol based on general circuit evaluation. Especially, if we combine with the mix and match technique, then we can obtain a highest-price auction protocol which is at least seven times faster. A second-price auction protocol is also easily constructed from our circuit.

%0 Conference Proceedings
%A Biskup, Joachim
%A Bonatti, Piero A.
%T Confidentiality Policies and Their Enforcement for Controlled Query Evaluation 
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 39-54
%F Database
%K inference control, controlled query evaluation, confidentiality policy, potential secret, secrecy, refusal, lying, combined refusal and lying
%X An important goal of security in information systems is confidentiality. A confidentiality policy specifies which users should be forbidden to acquire what kind of information, and a controlled query evaluation should enforce such a policy even if users are able to reason about a priori knowledge and the answers to previous queries. We put the following aspects into a unifying and comprehensive framework: formal models of confidentiality policies based on potential secrets or secrecies, user awareness of the policy instance, and enforcement methods applying either lying or refusal, or a combination of lying and refusal. Two new evaluation methods are introduced. Different approaches are systematically compared and evaluated.

%0 Conference Proceedings
%A Wang, Lingyu
%A Wijesekera, Duminda
%A Jajodia, Sushil
%T Cardinality-Based Inference Control in Sum-Only Data Cubes
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 55-71
%F Database
%X This paper addresses the inference problems in data warehouses and decision support systems such as on-line analytical processing (OLAP) systems. Even though OLAP systems restrict user accesses to predefined aggregations, inappropriate disclosure of sensitive attribute values may still occur. Based on a definition of non-compromiseability to mean that any member of a set of variables satisfying a given set of their aggregations can have more than one value, we derive sufficient conditions for non-compromiseability in sum-only data cubes. Under this definition, (1) the non-compromiseability of multi-dimensional aggregations can be reduced to that of one dimensional aggregations, (2) full or dense core cuboids are non-compromiseable, and (3) there is a tight lower bound for the cardinality of a core cuboid to remain non-compromiseable. Based on these results, taken together with a three-tier model for controlling inferences, we provide a divide-and-conquer algorithm that uniformly divides data sets into chunks and builds a data cube on each such chunk. The union of these data cubes are then used to provide users with inference-free OLAP queries.

%0 Conference Proceedings
%A Smith, Sean W.
%T Outbound Authentication for Programmable Secure Coprocessors
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 72-89
%F Hardware
%X A programmable secure coprocessor platform can help solve many security problems in distributed computing. However, these solutions usually require that coprocessor applications be able to participate as full-fledged parties in distributed cryptographic protocols. Thus, to fully enable these solutions, a generic platform must not only provide programmability, maintenance, and configuration in the hostile field--it must also provide outbound authentication for the entities that result. A particular application on a particular untampered device must be able to prove who it is to a party on the other side of the Internet. 
This paper offers our experiences in solving this problem for a high-end secure coprocessor product. This work required synthesis of a number of techniques, so that parties with different and dynamic views of trust can draw consistent and complete conclusions about remote coprocessor applications. These issues may be relevant to the industry's growing interest in rights management for general desktop machines.

%0 Conference Proceedings
%A Gomulkiewicz, Marcin
%A Kutylowski, Miroslaw
%T Hamming Weight Attacks on Cryptographic Hardware - Breaking Masking Defense
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 90-103
%F Hardware
%K cryptographic hardware, side channel cryptanalysis, Hamming weight, power analysis
%X It is believed that masking is an effective countermeasure against power analysis attacks: before a certain operation involving a key is performed in a cryptographic chip, the input to this operation is combined with a random value. This has to prevent leaking information since the input to the operation is random. 
We show that this belief might be wrong. We present a Hamming weight attack on an addition operation. It works with random inputs to the addition circuit, hence masking even helps in the case when we cannot control the plaintext. It can be applied to any round of the encryption. Even with moderate accuracy of measuring power consumption it determines explicitly subkey bits. The attack combines the classical power analysis (over Hamming weight) with the strategy of the saturation attack performed using a random sample. 
We conclude that implementing addition in cryptographic devices must be done very carefully as it might leak secret keys used for encryption. In particular, the simple key schedule of certain algorithms (such as IDEA and Twofish) combined with the usage of addition might be a serious danger.

%0 Conference Proceedings
%A Hogben, Giles
%A Jackson, Tom
%A Wilikens, Marc
%T A Fully Compliant Research Implementation of the P3P Standard for Privacy Protection: Experiences and Recommendations
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 104-125
%F Privacy and Applications
%K privacy enhancing technologies, P3P, XML digital signatures, secure electronic commerce, transaction management, security verification
%X This paper describes experiences gained from development of a fully compliant implementation of the W3C's XML based P3P standard. P3P aims to make privacy policies of web sites transparent for automated agents, and thereby to improve transactions of personal data on the Internet. We look at some of the most important issues that have arisen from our development work, including problems with the privacy preference standard, APPEL, before concentrating on issues related to end user assurance. We look at P3P usage scenarios to show that the current P3P standard has weaknesses in this area. The paper then considers possible extensions to P3P, which could provide greater assurance to end users and facilitate dispute resolution. In particular, we present an overview of a way for increasing assurance of a privacy policy's validity using signed XML.

%0 Conference Proceedings
%A Giles, James
%A Sailer, Reiner
%A Verma, Dinesh
%A Chari, Suresh
%T Authentication for Distributed Web Caches
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 126-145
%F Privacy and Applications
%K security, authentication, cookies, distributed applications, CDN
%X We consider the problem of offloading secure access-controlled content from central origin servers to distributed caches so clients can access a proximal cache rather than the origin servers. Our security architecture enforces the access-control policies of the origin server without replicating the access-control databases to each of the caches. We describe the security mechanisms to affect such a system and perform an extensive security analysis of our implementation. Our system is an example of how less trustworthy systems can be integrated into a distributed system architecture; it provides mechanisms to preserve the whole distributed system security even in case less trustworthy subsystems are compromised. An application of our system is the cached distribution of access-controlled contents such as subscription-based electronic libraries.

%0 Conference Proceedings
%A Broadfoot, Philippa
%A Lowe, Gavin
%T Analysing a Stream Authentication Protocol using Model Checking
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 146-161
%F Formal
%X In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we focus on the Timed Efficient Stream Loss-tolerant Authentication Protocol, TESLA. This protocol differs from the standard class of authentication protocols previously analysed using model checking techniques in the following interesting way: an unbounded stream of messages is broadcast by a sender, making use of an unbounded stream of keys; the authentication of the n-th message in the stream is achieved on receipt of the n+1-th message. We show that, despite the infinite nature of the protocol, it is possible to build a finite model that correctly captures its behaviour.

%0 Conference Proceedings
%A Heather, James
%A Schneider, Steve
%T Equal To The Task?
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 162-177
%F Formal
%K cryptographic protocols, rank functions, strand spaces, data independence, inequality tests, RSA, formal methods in security, security models, security verification
%X Many methods of analysing security protocols have been proposed, but most such methods rely on analysing a protocol running only a finite network. Some, however - notably, data independence, the strand spaces model, and the rank functions model - can be used to prove correctness of a protocol running on an unbounded network.
Roscoe and Broadfoot in [17] show how data independence techniques may be used to verify a security protocol running on an unbounded network. They also consider a weakness inherent in the RSA algorithm, discovered by Franklin and Reiter [3], and show that their data independence approach cannot deal with an intruder endowed with the ability to exploit this weakness. 
In this paper, we show that neither can the use of honest ideals in the strand spaces model or the use of rank functions in the CSP model be easily adapted to cover such an intruder. In each case, the inequality tests required to model the new intruder cause problems when attempting to extend analysis of a finite network to cover an unbounded network. The results suggest that more work is needed on adapting the intruder model to allow for cryptographic attacks.

%0 Conference Proceedings
%A Mok, Aloysius K.
%A Yu, Weijiang
%T TINMAN: A Resource Bound Security Checking System for Mobile Code
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 178-193
%F Formal
%X Resource security pertains to the prevention of unauthorized usage of system resources that may not directly cause corruption or leakage of information. A common breach of resource security is the class of attacks called DoS (Denial of Service) attacks. This paper proposes an architecture called TINMAN whose goal is to efficiently and effectively safeguard resource security for mobile source code written in C. We couple resource usage checks at the programming language level and at the run-time system level. This is achieved by the generation of a resource skeleton from source code. This resource skeleton abstracts the resource consumption behavior of the program which is validated by means of a resource usage certificate that is derived from proof generation. TINMAN uses resource-usage checking tools to generate proof obligations required of the resource usage certificate and provides full coverage by monitoring any essential property not guaranteed by the certificates. We shall describe the architecture of TINMAN and give some experimental results of the preliminary TINMAN implementation.

%0 Conference Proceedings
%A Santen, Thomas
%A Heisel, Maritta
%A Pfitzmann, Andreas
%T Confidentiality-Preserving Refinement is Compositional - Sometimes
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 194-211
%F Formal
%X Confidentiality-preserving refinement describes a relation between a specification and an implementation that ensures that all confidentiality properties required in the specification are preserved by the implementation in a probabilistic setting. The present paper investigates the condition under which that notion of refinement is compositional, i.e. the condition under which refining a subsystem of a larger system yields a confidentiality-preserving refinement of the larger system. It turns out that the refinement relation is not composition in general, but the condition for compositionality can be stated in a way that builds on the analysis of subsystems thus aiding system designers in analyzing a composition.

%0 Conference Proceedings
%A von Oheimb, David
%A Lotz, Volkmar
%T Formal Security Analysis with Interacting State Machines
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 212-228
%F Formal
%X We introduce the ISM approach, a framework for modeling and verifying reactive systems in a formal, even machine-checked, way. The framework has been developed for applications in security analysis. It is based on the notion of Interacting State Machines (ISMs), sort of high-level Input/Output Automata. System models can be defined and presented graphically using the AutoFocus tool. They may be type-checked and translated to a representation within the theorem prover Isabelle or defined directly as Isabelle theories. The theorem prover may be used to perform any kind of syntactic and semantic checks, in particular semi-automatic verification. We demonstrate that the framework can be fruitfully applied for formal system analysis by two classical application examples: the LKW model of the Infineon SLE66 SmartCard chip and Lowe's fix of the Needham-Schroeder Public-Key Protocol.

%0 Conference Proceedings
%A Koch, Manuel
%A Mancini, Luigi V.
%A Parisi-Presicce, Francesco
%T Decidability of Safety in Graph-based Models for Access Control
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 229-243
%F Formal
%X Models of Access Control Policies specified with graphs and graph transformation rules combine an intuitive visual representation with solid semantical foundations. While the expressive power of graph transformations leads in general to undecidable models, we prove that it is possible, with reasonable restrictions on the form of the rules, to obtain access control models where safety is decidable. The restrictions introduced are minimal in that no deletion and addition of a graph structure are allowed in the same modification step. We then illustrate our result with two examples: a graph based DAC model and a simplified decentralized RBAC model.

%0 Conference Proceedings
%A Wang, Xinyuan
%A Reeves, Douglas S.
%A Wu, S. Felix
%T Inter-Packet Delay Based Correlation for Tracing Encrypted Connections Through Stepping Stones
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 244-263
%F Intrusion Detection
%X Network based intrusions have become a serious threat to the users of the Internet. Intruders who wish to attack computers attached to the Internet frequently conceal their identity by staging their attacks through intermediate ``stepping stones''. This makes tracing the source of the attack substantially more difficult, particularly if the attack traffic is encrypted. In this paper, we address the problem of tracing encrypted connections through stepping stones. The incoming and outgoing connections through a stepping stone must be correlated to accomplish this. We propose a novel correlation scheme based on inter-packet timing characteristics of both encrypted and unencrypted connections. We show that (after some filtering) inter-packet delays (IPDs) of both encrypted and unencrypted, interactive connections are preserved across many router hops and stepping stones. The effectiveness of this method for correlation purposes also requires that timing characteristics be distinctive enough to identify connections. We have found that normal interactive connections such as telnet, SSH and rlogin are almost always distinctive enough to provide correct correlation across stepping stones. The number of packets needed to correctly correlate two connections is also an important metric, and is shown to be quite modest for this method.

%0 Conference Proceedings
%A Lee, Sin Yeung
%A Low, Wai Lup
%A Wong, Pei Yuen
%T Learning Fingerprints For A Database Intrusion Detection System
%B Computer Security - ESORICS 2002
%D 2002
%J 7th European Symposium on Research in Computer Security (ESORICS 2002)
%E Gollmann, Dieter
%E Karjoth, Günter
%E Waidner, Michael
%I Springer-Verlag
%C Zurich, Switzerland
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 2502
%P 264-280
%F Intrusion Detection
%X There is a growing security concern on the increasing number of databases that are accessible through the Internet. Such databases may contain sensitive information like credit card numbers and personal medical histories. Many e-service providers are reported to be leaking customers' information through their websites. The hackers exploited poorly coded programs that interface with backend databases using SQL injection techniques. We developed an architectural framework, DIDAFIT (Detecting Intrusions in DAtabases through FIngerprinting Transactions) [1], that can efficiently detect illegitimate database accesses. The system works by matching SQL statements against a known set of legitimate database transaction fingerprints. In this paper, we explore the various issues that arise in the collation, representation and summarization of this potentially huge set of legitimate transaction fingerprints. We describe an algorithm that summarizes the raw transactional SQL queries into compact regular expressions. This representation can be used to match against incoming database transactions efficiently. A set of heuristics is used during the summarization process to ensure that the level of false negatives remains low. This algorithm also takes into consideration incomplete logs and heuristically identifies "high risk" transactions.