%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % Foundations of Computer Security - FCS'02 % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Editor: Iliano Cervesato, iliano at itd.nrl.navy.mil Last Updated: Mon Jul 1 2002 Size: 13 entries Source: electronic proceedings FLoC'02 Workshop on Foundations of Computer Security --- FCS'02 Copenhagen, Denmark 25-26 July 2002 ISBN: ??? @InProceedings{Kuster:FCS:2002, author = "Ralf K{\"u}sters", institution = "Christian-Albrecht University Kiel, Germany", title = "On the Decidability of Cryptographic Protocols with Open-ended Data Structures", abstract = "Formal analysis of cryptographic protocols has mainly concentrated on protocols with closed-ended data structures, where closed-ended data structure means that the messages exchanged between principals have fixed and finite format. However, in many protocols the data structures used are open-ended, i.e., messages have an unbounded number of data fields. Formal analysis of protocols with open-ended data structures is one of the challenges pointed out by Meadows. This work studies decidability issues for such protocols. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security is decidable and PSPACE-hard in presence of the standard Dolev-Yao intruder.", booktitle = "Foundations of Computer Security", pages = "3--12", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{Kong-weiWing:FCS:2002, author = "Kong-wei Lye and Jeannette M. Wing", institution = "Carnegie Mellon University, USA", title = "Game Strategies In Network Security", abstract = "This paper presents a game-theoretic method for analyzing the security of computer networks. We view the interactions between an attacker and the administrator as a two-player stochastic game and construct a model for the game. Using a non-linear program, we compute the Nash equilibrium or best-response strategies for the players (attacker and administrator). We then explain why the strategies are realistic and how administrators can use these results to enhance the security of their network.", booktitle = "Foundations of Computer Security", pages = "13--22", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{Conchon:FCS:2002, author = "Sylvain Conchon", institution = "Oregon Graduate Institute, USA", title = "Modular Information Flow Analysis for Process Calculi", abstract = "We present a framework to extend, in a modular way, the type systems of process calculi with information-flow annotations that ensure a noninterference property based on bisimulation. Our method of adding security annotations readily supports modern typing features, such as polymorphism and type reconstruction, together with a non-interference proof. Furthermore, the new systems thus obtained can detect, for instance, information flow caused by contentions on distributed resources, which are not detected in a satisfactory way by using testing equivalences.", booktitle = "Foundations of Computer Security", pages = "23--34", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{AppelMichaelStumpVirga:FCS:2002, author = "Andrew W. Appel and Neophytos G. Michael and Aaron Stump and Roberto Virga", institution = "Princeton University, USA and Princeton University, USA and Stanford University, USA and Princeton University, USA", title = "A Trustworthy Proof Checker", abstract = "Proof-Carrying Code (PCC) and other applications in computer security require machine-checkable proofs of properties of machine-language programs. The main advantage of the PCC approach is that the amount of code that must be explicitly trusted is very small: it consists of the logic in which predicates and proofs are expressed, the safety predicate, and the proof checker. We have built a minimal-TCB checker, and we explain its design principles, and the representation issues of the logic, safety predicate, and safety proofs. We show that the trusted code in such a system can indeed be very small. In our current system the TCB is less than 2,700 lines of code (an order of magnitude smaller even than other PCC systems) which adds to our confidence of its correctness.", booktitle = "Foundations of Computer Security", pages = "37--48", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{SteelBundyDenney:FCS:2002, author = "Graham Steel and Alan Bundy and Ewen Denney", institution = "University of Edinburgh, UK", title = "Finding Counterexamples to Inductive Conjectures and Discovering Security Protocol Attacks", abstract = "We present an implementation of a method for finding counterexamples to universally quantified conjectures in first-order logic. Our method uses the proof by consistency strategy to guide a search for a counterexample and a standard first-order theorem prover to perform a concurrent check for inconsistency. We explain briefly the theory behind the method, describe our implementation, and evaluate results achieved on a variety of incorrect conjectures from various sources. Some work in progress is also presented: we are applying the method to the verification of cryptographic security protocols. In this context, a counterexample to a security property can indicate an attack on the protocol, and our method extracts the trace of messages exchanged in order to effect this attack. This application demonstrates the advantages of the method, in that quite complex side conditions decide whether a particular sequence of messages is possible. Using a theorem prover provides a natural way of dealing with this. Some early results are presented and we discuss future work. Keywords: Counterexamples, Security Protocols, Non-theorems, Proof by Consistency.", booktitle = "Foundations of Computer Security", pages = "49--58", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{ArmandoCompagna:FCS:2002, author = "Alessandro Armando and Luca Compagna", institution = "University of Genova, Italy", title = "Automatic {SAT}-Compilation of Security Problems", abstract = "We provide a fully automatic translation from security protocol specifications into propositional logic which can be effectively used to find attacks to protocols. Our approach results from the combination of a reduction of security problems to planning problems and well-known SAT-reduction techniques developed for planning. We also propose and discuss a set of transformations on security problems whose application has a dramatic effect on the size of the propositional encoding obtained with our SAT-compilation technique. We describe a model-checker for security protocols based on our ideas and show that attacks to a set of well-known authentication protocols are found in few seconds by state-of-the-art SAT solvers.", booktitle = "Foundations of Computer Security", pages = "59--67", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{Gollmann:FCS:2002, author = "Dieter Gollmann", institution = "Microsoft Research, UK", title = "Defining Security is Difficult and Error Prone", abstract = "It is often claimed that the design of security protocols is difficult and error prone, with formal verification suggested as the recommended remedy. Verification requires a formal statement of the desired security properties and, maybe surprisingly, many protocols are broken simply by varying the assumptions on goals and intended environment. To defend my claim that defining security is difficult and error prone (and the really interesting challenge in formal verification) I will discuss some old and new examples of security protocols and their formal analysis.", booktitle = "Foundations of Computer Security", pages = "71", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report", note = "Invited Talk" } @InProceedings{Meadows:FCS:2002, author = "Catherine Meadows", institution = "NRL Washington, USA", title = "Identifying Potential Type Confusion in Authenticated Messages", abstract = "A type confusion attack is one in which a principal accepts data of one type as data of another. Although it has been shown by Heather et al. that there are simple formatting conventions that will guarantee that protocols are free from simple type confusions in which fields of one type are substituted for fields of another, it is not clear how well they defend against more complex attacks, or against attacks arising from interaction with protocols that are formatted according to different conventions. In this paper we show how type confusion attacks can arise in realistic situations even when the types are explicitly defined in at least some of the messages, using examples from our recent analysis of the Group Domain of Interpretation Protocol. We then develop a formal model of types that can capture potential ambiguity of type notation, and outline a procedure for determining whether or not the types of two messages can be confused. We also discuss some open issues.", booktitle = "Foundations of Computer Security", pages = "75--84", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{Cohen:FCS:2002, author = "Ernie Cohen", institution = "Microsoft Research, UK", title = "Proving Protocols Safe from Guessing", abstract = "We describe how to prove cryptographic protocols secure against a Dolev-Yao attacker that can also engage in idealized offline guessing attacks. Our method is based on constructing a first-order invariant that bounds, in every reachable state, both the information available to an an attacker and the steps of guessing attacks starting from this information. We have implemented the method as an extension to the protocol verifier TAPS, making it the first mechanical verifier to prove protocols secure against guessing attacks in an unbounded model.", booktitle = "Foundations of Computer Security", pages = "85--92", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{BauerLigattiWalker:FCS:2002, author = "Lujo Bauer and Jarred Ligatti and David Walker", institution = "Princeton University, USA", title = "More Enforceable Security Policies", abstract = "We analyze the space of security policies that can be enforced by monitoring programs at runtime. Our program ``monitors'' are automata that examine the sequence the program actions and transform the sequence when it deviates from the specified policy. The simplest such automaton truncates the action sequence by terminating a program. Such automata are commonly known as ``security automata,'' and they enforce Schneider's EM class of security policies. We define automata with more powerful transformational abilities, including the ability to insert a sequence of actions into the event stream and to suppress actions in the event stream without terminating the program. We give a set-theoretic characterization of the policies these new automata are able to enforce and show that they are a superset of the EM policies.", booktitle = "Foundations of Computer Security", pages = "95--104", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{LiuSmith:FCS:2002, author = "Yu David Liu and Scott F. Smith", institution = "Johns Hopkins University, USA", title = "A Component Security Infrastructure", abstract = "This paper defines a security infrastructure for access control at the component level of programming language design. Distributed components are an ideal place to define and enforce significant security policies, because components are large entities that often define the political boundaries of computation. Also, rather than building a security infrastructure from scratch, we build on a standard one, the SDSI/SPKI security architecture.", booktitle = "Foundations of Computer Security", pages = "105--115", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{SkalkaSmith:FCS:2002, author = "Christian Skalka and Scott Smith", institution = "Johns Hopkins University, USA", title = "Static Use-Based Object Confinement", abstract = "The confinement of object references is a significant security concern for modern programming languages. We define a language that serves as a uniform model for a variety of confined object reference systems. A \emph{use-based} approach to confinement is adopted, which we argue is more expressive than previous communication-based approaches. We then develop a readable, expressive type system for static analysis of the language, along with a type soundness result demonstrating that run-time checks can be eliminated. The language and type system thus serve as a reliable, declarative and efficient foundation for secure capability-based programming and object confinement.", booktitle = "Foundations of Computer Security", pages = "117--126", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report" } @InProceedings{Panel:FCS:2002, author = "Serge Autexier and Iliano Cervesato and Heiko Mantel (moderators)", institution = "DFKI Saarbr{\"u}cken and ITT industries and DFKI Saarbr{\"u}cken", title = "The Future of Protocol Verification", abstract = "This panel is aimed at assessing the state of the art and exploring trends and emerging issues in computer security in general and protocol verification in particular. It brings together experts from both the security community and the verification area. Some of questions over which they will be invited to discuss their views, and maybe even to answer, include: What is already solved? What still needs improvement? What are the challenging open problems? What is the role of automated theorem proving in protocol verification? What else is there in computer security besides protocol verification? A format for this panel has been chosen as to achieve an interesting, vibrant, and productive discussion.", booktitle = "Foundations of Computer Security", pages = "129", year = "2002", editor = "Iliano Cervesato", address = "Copenhagen, Denmark", month = "25--26 July", publisher = "DIKU Technical Report", note = "Panel" }