%0 Conference Proceedings
%A Bieber, P.
%A Cazin, J.
%A Girard, P.
%A Lanet, J.-L.
%A Wiels, V.
%A Zanon, G.
%T Checking Secure Interactions of Smart Card Applets
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Cuppens, Frédéric
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 1-16
%F Personal Devices and Smartcards
%X This paper presents an approach enabling a smart card issuer to verify that a new applet securely interacts with already downloaded applets. A security policy has been defined that associates levels to applet attributes and methods and defines authorized flows between levels. We propose a technique based on model checking to verify that actual information flows between applets are authorized. We illustrate our approach on applets involved in an electronic purse running on Java enabled smart cards.

%0 Conference Proceedings
%A Schellhorn, Gerhard
%A Reif, Wolfgang
%A Schairer, Axel
%A Karger, Paul
%A Austel, Vernon
%A Toll, David
%T Verification of a Formal Security Model for Multiapplicative Smart Cards
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 17-36
%F Personal Devices and Smartcards
%X We present a generic formal security model for operating systems of multiapplicative smart cards. The model formalizes the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applications. The model satisfies a security policy consisting of authentication and intransitive noninterference. The model extends the classical security models of Bell/LaPadula and Biba, but avoids the need for trusted processes, which are not subject to the security policy by incorporating such processes directly in the model itself. The correctness of the security policy has been formally proven with the VSE II system.

%0 Conference Proceedings
%A Rannenberg, Kai
%T How Much Negociation and Detail Can Users Handle? Experiences with Security Negociation and the Granularity of Access Control in Communications
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 37-54
%F Personal Devices and Smartcards
%X Tailor made security is being enabled by more options for specifying security policies and enhanced possibilities for negotiating security. On the other side these new options raise the complexity of transactions and systems: Users can be overwhelmed, which can lead to less security than before. This paper describes conclusions from a case study and trial of personal reachability and security manager for telephone based communication. The device helped to negociate and balance security requirements. The study analysed how much negociation and detail users could handle during their day-to-day transactions and how they could be supported. Some results are strongly related to more 'classic' security techniques like access control that are becoming more and more interactive: When users learn to understand the consequences of their access control decisions and can tune their policies these mature to a satisfying level. When users see advantages for their daily activities they are willing to invest more time into understanding additional complexity.

%0 Conference Proceedings
%A Van Herreweghen, Els
%T Secure Anonymous Signature-Based Transactions
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 55-71
%F Electronic Commerce Protocols
%X Electronic commerce protocols often require users to reveal their identities and other information not necessary for reasons of security. Some applications such as contract signing are often argued to require a signer's authenticated identity; but this authentication may give the recipient a false feeling of security if certificate registration procedures do not guarantee a mapping to a liable person, or correctness of certificate data. In this paper, we propose a separation of identity from liability. Liability-aware certificates allow certificate issuers to make explicit which liabilities it takes with respect to the transaction, the certificate data or the signer's identity. We illustrate their use in the design of a pseudonym service providing pseudonym certificates for secure anonymous transactions.

%0 Conference Proceedings
%A Masucci, Barbara
%A Stinson, Douglas R.
%T Metering Schemes for General Access Structures
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 72-87
%F Electronic Commerce Protocols
%K distributed audit, metering, security, cryptography, entropy
%X A metering scheme is a method by which an audit agency is able to measure the interaction between servers and clients during a certain number of time frames. Naor and Pinkas considered schemes in which any server is able to construct a proof if and only if it has been visited by at least a number, say h, of clients in a given time frame. In this paper we construct metering schemes for more general access structures, which include multilevel and compartmented access structures. Metering schemes realizing these access structures have useful practical applications: for example, they can be used to measure the interaction of a web site with a specific audience which is of special interest. We also prove lower bounds on the communication complexity of metering schemes realizing general access structures.

%0 Conference Proceedings
%A Brose, Gerald
%T A Typed Access Control Model for CORBA
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 88-105
%F Access Control
%K access control, roles, types, CORBA
%X Specifying and managing access rights in large distributed systems is a non-trivial task. This paper presents a language-based approach to support policy-based management of access rights. We develop an object-oriented access model and a concrete syntax that is designed to allow both flexible and manageable access control policies for CORBA objects. We introduce a typed construct for access rights called view that allows static type checking of specifications and show how a realistic example policy is expressed in our notation.

%0 Conference Proceedings
%A Soshi, Masakazu
%T Safety Analysis of the Dynamic-Typed Access Matrix Model
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 106-121
%F Access Control
%K access control, access matrix model, safety problem, computational complexity, decidability
%X The safety problem in access matrix models is the one to determine whether or not a given subject can eventually obtain an access privilege to a given object. Unfortunately, little is known about protection systems for which the safety problem is decidable, except for strongly constrained systems (e.g., monotonic systems). Therefore, we propose the Dynamic-Typed Access Matrix Model, which extends Typed Access Matrix model by allowing the type of an object to change dynamically. DTAM model has an advantage that it can describe non-monotonic protection systems for which the safety problem is decidable. In this paper, we formally define DTAM model and then discuss various aspects of it.

%0 Conference Proceedings
%A Koch, Manuel
%A Mancini, Luigi V.
%A Parisi-Presicce, Francesco
%T A Formal Model for Role-Based Access Control Using Graph Transformations
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 122-139
%F Access Control
%X Role-Based Access Control (RBAC) is supported directly or in a closely related form, by a number of products. This paper presents a formalization of RBAC using graph transformations which is a graphical specification technique based on a generalization to nonlinear structures of classical string grammars. This proposed formalization provides an intuitive description for the manipulation of graph structures as they occur in information systems access control, a specification of static and dynamic consistency conditions on graphs and graph transformations, a uniform treatment of user roles and administrative roles, and a detailed analysis of the decentralization of administrative roles. Moreover, the properties of a given RBAC specification can be verified by employing one of the graph transformation tools available.

%0 Conference Proceedings
%A Howell, Jon
%A Kotz, David
%T A Formal Semantics for SPKI
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 140-158
%F Protocol Verification
%X We extend the logic and semantic of authorization due to Abadi, Lampson et al. to support restricted delegation. Our formal model provides a simple interpretation for the variety of constructs in the Simple Public Key Infrastructure (SPKI), and lends intuition about possible extensions. We discuss both extensions that our semantics supports and extensions that it cautions against.

%0 Conference Proceedings
%A Bella, Giampaolo
%A Massacci, Fabio
%A Paulson, Lawrence C.
%A Tramontano, Piero
%T Formal Verification of Cardholder Registration in SET
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 159-174
%F Protocol Verification
%X The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.

%0 Conference Proceedings
%A Broadfoot, P. J.
%A Lowe, G.
%A Roscoe, A. W.
%T Automating Data Independence
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 175-190
%F Protocol Verification
%K security protocols, data independence, automatic verification, model checking, Casper, CSP, FDR
%X In this paper, we generalize and fully automate the use of data independence techniques in the analysis of security protocols, developed in [Roscoe98, Roscoe&Broadfoot99]. In [Roscoe&Broadfoot99], we successfully applied these techniques to a series of case studies; however, our scripts were carefully crafted by hand to suit each case study, a rather time-consuming and error-prone task. We have fully automated the data independence techniques by incorporating them into Casper, thus abstracting away from the user the complexity of the techniques, making them much more accessible.

%0 Conference Proceedings
%A Yoda, Kunikazu
%A Etoh, Hiroaki
%T Finding a Connection Chain for Tracing Intruders
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 191-205
%F Internet Security
%X Intruders usually log in through a chain of multiple computer systems to hide their origins before breaking into their targets, which makes tracing difficult. In this paper we present a method to find the connection chain of an intruder for tracing back to the origin. We focus on telnet and rlogin as interactive applications intruders use to log in through hosts. The method involves setting up packet monitors at as many traffic points as possible on the Internet to record the activities of intruders at the packet level. When a host is compromised and used as a step-through host to access another host, we compare the packet logs of the intruder at that host to logs we have recorded all over the Internet to find the closest match. We define the 'deviation' for one packet stream on a connection from another, and implement a system to compute deviations. If a deviation is small, the two connections must be in the same connection chain. We present some experimental results showing that the deviation for two unrelated packet streams is large enough to be distinguished from the deviation for packet streams on connections in the same chain.

%0 Conference Proceedings
%A Paul, Olivier
%A Laurent, Maryline
%A Gombault, Sylvain
%T A Full Bandwidth ATM Firewall
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 206-221
%F Internet Security
%X In this paper we describe an architecture providing an high speed access control service for ATM networks. This architecture is based on two main components. The first one is a signalling analyser which takes the signalling information as an input and produces dynamically the configuration for our second module. This second module called IFT (Internet Fast Translator) is used to analyse the information located in the ATM cells and currently operates at 622Mb/s. The complete architecture provides the access control at the ATM, IP and transport levels without packet reassembling.

%0 Conference Proceedings
%A Evans, Neil
%A Schneider, Steve
%T Analysing Time Dependent Security Properties in CSP Using PVS
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 222-237
%F Security Property Analysis
%K authentication protocol verification, automated theorem proving, timed behaviour, CSP, PVS
%X This paper details an approach to verifying time dependent authentication properties of security protocols. We discuss the introduction of time into the Communicating Sequential Processes (CSP) protocol verification framework of [Schneider97]. The embedding of CSP in the theorem prover PVS (Prototype Verification System) is extended to incorporate event-based time, retaining the use of the existing rank function approach to verify such properties. An example analysis is demonstrated using the Wide-Mouthed Frog protocol.

%0 Conference Proceedings
%A Mantel, Heiko
%T Unwinding Possibilistic Security Properties
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 238-254
%F Security Property Analysis
%K security models, information flow, unwinding, refinement
%X Unwinding conditions are helpful to prove that deterministic systems fulfill non-interference. In order to generalize non-interference to non-deterministic systems various possibilistic security properties have been proposed. In this paper, we present generic unwinding conditions which are applicable to a large class of such security properties. That these conditions are sufficient to ensure security is demonstrated by unwinding theorems. In certain cases, they are also necessary. The practical usefulness of our results is illustrated by instantiating the generic unwinding conditions for well-known security properties. Furthermore, similarities of proving security with proving refinement are identified which results in proof techniques which are correct as well as complete.

%0 Conference Proceedings
%A Guttman, Joshua D.
%A Herzog, Amy L.
%A Thayer, F. Javier
%T Authentication and Confidentiality via IPsec
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 255-272
%F Security Property Analysis
%X The IP security protocols (IPSEC) may be used via security gateways that apply cryptographic operations to provide security services to datagrams, and this mode of use is supported by an increasing number of commercial products. In this paper, we formalize the types of authentication and confidentiality goal that IPSEC is capable of achieving, and we provide criteria that entail that a network with particular IPSEC processing achieves its security goals. This requires us to formalize the structure of networks using IPSEC, and the state of packets relevant to IPSEC processing. We can then prove confidentiality goals as invariants of the formalized systems. Authentication goals are formalized in the manner of [Schneider96], and a simple proof method using "unwinding sets" is introduced. We end the paper by explaining the network threats that are prevented by correct IPSEC processing.

%0 Conference Proceedings
%A Bryce, Ciaran
%T A Security Framework for a Mobile Agent System
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 273-290
%F Mobile Agents
%X This paper describes a distributed security infrastructure for mobile agents. The first property of the infrastructure is believability; this means that mechanisms are provided for authenticating information furnished by an agent. A second security property is survivability. This means that an agent computation can be programmed to survive attacks by malicious hosts on individual agents; this is achieved through encryption as well as agent replication and voting. The main feature of the infrastructure is that mobile agents are themselves used to enforce the security properties.

%0 Conference Proceedings
%A Molva, Refik
%A Roudier, Yves
%T A Distributed Access Control Model for Java
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 291-308
%F Mobile Agents
%K Java, access control model, distribution, SPKI, capabilities
%X Despite its fully distributed and multi-party execution model, Java only supports centralized and single party access control. We suggest a new access control model for mobile code that copes with the shortcomings of the current access control model of Java. This new model is based on two key enhancements: the association of access control information with each mobile code segment in the form of attributes and the introduction of intermediate elements in the access control schema. The combination of the current ACL-based approach with the capability scheme achieved through mobile code attributes allows the new access control model to address dynamic multi-party scenarios while keeping the burden of security policy configuration at a minimum. We finally sketch the design of an access control system based on the proposed model using Simple Public Key Infrastructure (SPKI) certificates.

%0 Conference Proceedings
%A Welch, Ian
%A Stroud, Robert J.
%T Using Reflection as a Mechanism for Enforcing Security Policies in Mobile Code
%B Computer Security - ESORICS 2000
%D 2000
%J 6th European Symposium on Research in Computer Security (ESORICS 2000)
%E Frédéric Cuppens
%I Springer-Verlag
%C Toulouse, France
%6 1
%S Lecture Notes in Computer Science
%Y Goos, G.
%Y Hartmanis, J.
%Y van Leeuwen, J.
%V 1895
%P 309-323
%F Mobile Agents
%X Several authors have proposed using code modification as a technique for enforcing security policies such as resource limits, access controls, and network information flows. However, these approaches are typically ad hoc and are implemented witout a high level abstract framework for code modification. We propose using reflection as a mechanism for implementing code modifications within an abstract framework based on the semantics of the underlying programming language. We have developed a reflective version of Java called Kava that uses byte-code rewriting techniques to insert pre-defined hooks into Java class files at load time. This makes it possible to specify and implement security policies for mobile code in a more abstract and flexible way. Our mechanism could be used as a more principled way of enforcing some of the existing security policies described in the literature. The advantages of our approach over related work (SASI, JRes, etc.) are that we can guarantee that our security mechanisms cannot be bypassed, a property we call strong non-bypassability, and that our approach provides the high level abstractions needed to build useful security policies.