Workshop Program with hyperlinks to presented papers
The 12th IEEE CSFW was held in the delightful Hotel Panazza, in Mordano, Italy, a small town near Imola. The opening comments by Roberto Gorrieri (general chair) and Paul Syverson (program chair) revealed that this was the largest CSFW ever. There were 50 attendees, with 25 from the USA, and 12 from the UK. Ten more people were interested in attending but had to be turned away. The 13th CSFW will be held in Cambridge, England. Details will be available from http://www.csl.sri.com/csfw/ A Formal Framework and Evaluation Method for Network Denial of Service Cathy Meadows. In network denial of service attacks on protocols for establishing authenticated communication channels, the identity of the attacker is generally unknown, because authentication has not been completed. A design technique for making protocols more resistant to such attacks is the use of a sequence of authentication mechanisms, arranged in order of increasing cost (to both parties) and security. Thus, an attacker must be willing to complete the earlier stages of the protocol before it can force a system to expend resources running the later stages of the protocol. Cathy proposed a framework for analyzing such protocols. The framework is based on Gong and Syverson's model of fail-stop protocols. The NRL protocol analyzer was used to formally verify some properties of such protocols. I/O Automaton Models and Proofs of Shared-Key Communications Systems Nancy Lynch The emphasis is on modular reasoning using standard proof techniques, specifically, invariant assertions and simulation relations. To illustrate the approach, I/O-automaton models of private communication channels, key distribution, shared-key cryptography, base-exponent cryptography, and an eavesdropper were developed, and a modular proof was given to show that a straightforward cryptographic protocol implements private communication channels in the presence of an eavesdropper. The modular proof requires finding, for each subprotocol, an invariant characterizing the set of messages that that subprotocol can tolerate being revealed to the eavesdropper. A similar proof involving an active attacker is almost finished. More ambitious future work aims at modular probabilistic reasoning; the central problem there is to show that a small probability of a successful attack on a protocol does not blow up when the protocol is composed with other protocols. John Mitchell pointed out that the invariants sometimes need to be time-dependent; for example, it might be OK to reveal a particular message after (but not before) a certain point in the protocol. Cathy Meadows asked whether this approach can be used to show that similar subprotocols in a protocol suite don't interfere with each other. Nancy replied that it can. Safe Simplifying Transformations for Security Protocols Gavin Lowe (speaker) and Mei Lin Hui The goal is to reduce the cost of model checking by first applying some safe simplifying transformations to the protocol. In this context, "safe" means: if the original protocol is insecure, then so is the transformed protocol. Thus, if the model checker does not find an attack on the simplified protocol, then the original protocol is secure. If the model checker does find an attack on the simplified protocol, then the user must determine by inspection whether the original protocol is vulnerable to an analogous attack, or whether the attack is an artifact of the simplifications. They applied this approach while analyzing the Cybercash and SET protocols. They assume that cryptographic keys are atomic. Someone asked whether this assumption is necessary. Gavin was uncertain whether structured keys could easily be accommodated. Someone asked whether the simplifying transformations are a special case of forward simulations. Gavin said they probably are. Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief David Monniaux Decision procedures for BAN-like logics of belief are not new. Mao and Boyd (IEEE CSFW, 1993) describe a tableau-based procedure. Kindred and Wing (USENIX Workshop on Electronic Commerce, 1996) describe a decision procedure that uses forward chaining and backward chaining. David's approach uses only forward chaining. Some automatic transformations of the proof system are used to make all rules suitable for forward chaining. David considered trying to use only backward chaining, but that seemed more difficult. Cathy Meadows asked how decidability of such proof systems relates to undecidability results such as that in the paper by Cervesato et al. (described next). David replied that the undecidability results apply to semantic models of authentication protocols, and there is no good such semantics for belief logics. A Meta-Notation for Protocol Analysis Iliano Cervesato, Nancy Durgin, Pat Lincoln, John Mitchell (speaker), and Andre Scedrov The goal is to find the simplest framework that captures the essential aspects of the Dolev-Yao model of cryptographic protocols. The Dolev-Yao model implies certain assumptions about the adversary, e.g., the adversary cannot gain partial knowledge of a value or perform statistical tests. The framework is designed to facilitate meta-theory. It is also hoped that other researchers will adopt the framework, to help unify work on analysis of cryptographic protocols. The framework is based on multiset rewriting. Generation of fresh values (e.g., nonces) is modeled by existential quantification. Using this framework, they studied how various restrictions on protocols affect the complexity of verification. If the depth of encryptions and the number of fields per message are bounded, and the number of protocol instances and the number of generated nonces are unbounded, then the verification problem is undecidable. If either one of the latter two parameters is bounded, then the verification problem is decidable. There is a typo in the paper: "PSPACE-complete" should be changed to "DEXP-time complete". Mixed Strand Spaces F. Javier Thayer Fabrega, Jonathan Herzog, and Joshua Guttman (speaker) Principals sometimes use multiple protocols with similar message formats and sometimes share keying material among them. This can cause problems. For example, in the Neumann-Stubblebine protocol, the re-authentication protocol introduces a violation of agreement in the authentication protocol. Such problems motivate the study of techniques for proving that different (sub)protocols do not interact in harmful ways. "Mixing conditions" are proposed for this purpose. Mixing conditions are described here in terms of the strand space model, though the idea is fairly model-independent. Mixing conditions are related to the invariants used in Nancy Lynch's approach (described above). Mixing conditions for a protocol P are derived from the correctness proof of P in isolation. If the other protocols used with P satisfy the mixing conditions, then they do not cause P to violate its requirements. Someone asked whether their work considers type-confusion attacks. Joshua said no, but extending it to do so might be possible. Someone asked whether their approach can be used when the correctness requirements include non-repudiation; this might be tricky, because the strand space model distinguishes regular and penetrator strands, and with non-repudiation, this distinction might be blurred. Josh thinks that this is not a problem, because non-repudiation can be expressed as a property of the form "if a bundle contains a strand of the form X, then it also contains a strand of the form Y" (e.g., X involves receipt of evidence that some action occurred, and Y contains such an action), and their approach handles properties of this form. Honest Functions and their Application to the Analysis of Cryptographic Protocols Al Maneki The theory of strand spaces is extended to encompass a broader class of cryptographic protocols. A class of functions, called honest functions, is defined; this class include exclusive-or and exponentiation of integers in a prime number field. Informally, a function f is honest if either (1) f is 1-to-1 and its inverse is not easily computed, or (2) for each y=f(x_1,...,x_n), y has so many pre-images under f that exhaustive search of them is infeasible. Some general theorems are given to facilitate reasoning in the strand space model about protocols that use honest functions. The approach is illustrated by an analysis of Roscoe's version of the TMN protocol. Panel: Formalization and Proof of Secrecy Properties Dennis Volpano (chair), Cathy Meadows, Jon Millen, Martin Abadi, and Riccardo Focardi The first day ended with a panel discussion. Each panelist gave a short presentation before the free-for-all discussion. Dennis Volpano emphasized the importance of considering secrecy of bindings (e.g., of a variable to a value), as opposed to secrecy of values (e.g., private keys). He distinguished three notions of secrecy: Secrecy as a safety property. This notion is used in the Dolev-Yao model and its descendants. It is typically used for expressing secrecy of values. This notion facilitates automated reasoning but does not consider indirect information flow. Unconditional secrecy (non-interference). This approach considers indirect information flow and in some cases can handle probabilistic violations of secrecy, but it does not handle some forms of cryptography (e.g., public-key crypto). Conditional secrecy. In this approach, one shows that obtaining secret information is as difficult as breaking the underlying cryptosystem. Cathy Meadows characterized the Dolev-Yao approach to secrecy as shallow and wide, because the same approach works for a wide variety of properties. In contrast, models of information flow are narrow and deep. Access control is also shallow and wide. Bell and La Padula tried to integrate access control and information flow. That effort foundered on downgrading. This led to notions of intransitive non-interference, and so on. That line of work might be relevant to protocol analysis; for example, it might be possible to analyze subliminal channels in authentication protocols. Jon Millen discussed operating system secrecy vs. protocol secrecy. He expressed an analogy between them by drawing two pyramids: / covert channels \ / cryptanalysis \ / probabilistic models \ / probabilistic models \ / non-interference \ / model checking, inductive proofs \ / access control \ / belief logics \ Non-interference is suitable for proving absence of causal flow of a bit or bits. In protocol analysis, one deals with secrecy of bitstrings large enough to be unguessable, so if those bits appear in two places, causal flow between those places is assumed. This model is attractive because it is simpler, but is it model always adequate for protocol analysis? No: a large bitstring might be compromised through repeated attacks that each obtain partial information. Such attacks are not considered in Dolev-Yao-like models. Martin Abadi advocated expressing secrecy in terms of observational equivalence, as done in the Spi calculus. The Dolev-Yao notion of secrecy is good for expressing secrecy of unguessable values but is not good at expressing secrecy of guessable values (e.g., Booleans). This is a major limitation, because application data, which is what really matters, usually contains guessable values. (One could argue that keeping application data secret is easy if cryptographic keys are kept secret, but it would be nice to prove this.) Secrecy of both kinds of values can be expressed using observational equivalence. Riccardo Focardi described a non-interference-based approach to protocol analysis. The basic idea is to show that the intruder cannot interfere with the protocol. This approach allows general results about non-interference to be used, e.g., results that justify considering only the most powerful intruder. During the free-for-all discussion, John McLean suggested that non-interference is not applied more often to analysis of cryptographic protocols because: (1) we still don't understand the Dolev-Yao model as well as we understand access control, (2) cryptanalytic attacks are probably more important than the information leaks that can be analyzed using non-interference, (3) the theory of non-interference does not handle some forms of cryptography, (4) reasoning about non-interference is difficult, and reasoning about probabilistic non-interference is even more difficult. Martin Abadi said that, if he were deciding how to allocate resources to be spent on verification of a protocol, he would formally state and informally prove the secrecy properties, but he would not spend money on formal verification of them. He would spend that money on formal verification of authenticity properties. Dennis Volpano pointed out that implementations might have information leaks that are not evident in the high-level protocol descriptions commonly used in the protocol analysis community. For example, the possibility of timing attacks on a protocol (or on the underlying cryptosystem) is usually not considered. Jon Millen noted that such analysis would occur at the top level of his pyramid. Authentication via Localized Names Chiara Bodei, Pierpaolo Degano (speaker), Riccardo Focardi and Corrado Priami The goal is to provide a high-level characterization of message authentication and to study how encryption is used to achieve message authentication. The formal framework is a variant of the Spi-calculus in which each sequential process has its own namespace. A Logic for SDSI's Linked Local Name Spaces Joseph Y. Halpern and Ron van der Meyden (speaker) Rivest and Lampson's Simple Distributed Security Infrastructure (SDSI) incorporates linked local namespaces. For example, suppose that in my (local) namespace, "Joe" refers to Joe Halpern (i.e., is bound to Joe Halpern's public key). Then, in my namespace, "Joe's colleagues" refers to the binding of "colleagues" in Joe Halpern's namespace. Bindings are created by issuing certificates. The authors give (1) a semantic characterization of SDSI's name resolution algorithm, (2) a sound and complete axiomatization for proving validity of formulas with respect to that semantics, and (3) a translation of their proof system into Datalog that yields a polynomial-time implementation of the SDSI name resolution algorithm. Martin Abadi had previously proposed a logic for SDSI's local namespaces; however, Abadi's axioms do not correspond to precisely to SDSI's name resolution algorithm. [I missed the session on Interaction and Composition, which contained the next three talks, so I have included abstracts of the papers' abstracts.] Trusted System Construction Colin O'Halloran An important trend is construction of trusted systems from COTS components by encapsulating each component in an appropriate software wrapper. Achieving security without compromising the operational effectiveness of the system is difficult. This work addresses the problem of analyzing such systems to demonstrate that the system is both secure and usable. The proposed approach is illustrated using the X windowing system. Secure Composition of Insecure Components Peter Sewell and Jan Vitek Many contemporary software systems consist of numerous components that interact in intricate ways. Some components are only partially trusted. To ensure security properties of the entire system, components are executed in the context of wrappers that provide fine-grained control over interactions between components. The authors propose a formal model based on the pi-calculus that is suitable for analyzing such systems. Security Function Interactions Pierre Bieber This paper uses a compositional framework to model security architectures involving heterogeneous and distributed security functions. The goal is to assist the ITSEC evaluation of suitability, binding and vulnerability of a set of security functions. The author proposes constraints that security functions should guarantee in order to interact consistently and securely with other functions. These notions are illustrated by studying the interactions of various components of a secure LAN. A Logic-based Knowledge Representation for Authorization with Delegation Ninghui Li, Joan Feigenbaum (speaker), and Benjamin Grosof Trust management systems integrate authentication and access control. Whether this is a good idea is still an open question, according to Joan. Trust management systems, such as KeyNote, are starting to be deployed in commercial systems, but more experience is needed before the benefits of trust management systems can be properly evaluated. Delegation Logic (DL) is proposed to provide a more formal and less ad-hoc foundation for trust management systems. DL can be used to determine whether a request supported by certain credentials should be approved under a certain authorization policy. Logic-programming techniques can be used to automate such authorization decisions. DL treats delegation depth explicitly. This enables expression of policies such as: I give you permission to delegate permission to perform some operation X to anyone you trust, but those principals cannot delegate permission to perform X to other principals. Whether it is useful for a trust management system to support bounded delegation depth greater than one is still an open question, according to Joan. DL supports a general notion of delegation to complex principals; this notion can be used to represent k-out-of-n threshold schemes. DL is based on general ideas from logic programming, so it can cleanly support non-monotonicity (useful for expressing revocation), negation, and prioritized conflict resolution. Joan announced that there is a typo in the paper: on p. 169, column 1, in the numbered list of items, a fifth item was accidentally omitted: 5. Every ground clause that has the form: $$ delegates(A, pred, [params], *, A ,1).$$ Intuitively, this represents the fact that every principal delegates every predicate to itself with depth *. A revised version of the full paper is available from http://www.research.ibm.com/people/g/grosof/papers.html . A Logical Framework for Reasoning on Data Access Control Policies Elisa Bertino, Francesco Buccafuri (speaker), Elena Ferrari, and Pasquale Rullo A logic formalism is proposed for expressing access control policies, e.g., for database security. Authorizations are represented by logic rules. Two forms of negation are distinguished: strong negation, for expressing prohibition (e.g., "Bill is forbidden from accessing that table"), and weak negation, for expressing absence of explicit positive authorization (e.g., "Bill has not explicitly been given permission to access that table"). Priorities can be used to help determine which rules prevail in case of conflicts. Various possible semantics for authorization rules are given, based on semantics of logic programs. Athena: a New Efficient Automatic Checker for Security Protocol Analysis Dawn Xiaodong Song Athena is a tool for automated analysis of security protocols. To verify a property, Athena starts from appropriate states of interest (e.g., states containing a violation of a secrecy requirement) and performs a backward search to determine whether (and, if so, how) the system could have reached such a state. For efficiency, Athena allows states to contain variables; thus, a single "symbolic" state represents a set of concrete states (namely, the states that can be obtained by replacing the variables with type-correct values). In the two aspects just described, Athena is similar to Cathy Meadows' NRL Protocol Analyzer. A significant difference is that Athena is based on the strand space model, and during the backward search, Athena tries to add an entire strand to the state in a single step. Thus, Athena can avoid exploring interleavings of independent events in different strands. This can drastically reduce the number of explored states. Athena embodies a semi-decision procedure; in other words, Athena may diverge. This is unavoidable, given undecidability results such as those in the paper by Cervesato et al. (described above). John Mitchell mentioned that a newer version of the Murphi-based security protocol analyzer by Mitchell, Stern, et al. explores about 500 states when analyzing the Needham-Schroeder-Lowe protocol; the figure of about 500,000 states that appears in Table 1 of this paper is out of date. John said that the most effective optimization they incorporated is forcing alternation between transitions of the intruder and transitions of honest principals. He asked whether Athena exploits a similar optimization. Dawn replied that it is hard to compare the optimizations used in the two systems. Cathy Meadows suggested that it would be interesting to compare Athena's verification of the Needham-Schroeder-Lowe protocol with her analysis of that protocol using the NRL Protocol Analyzer, as described in an ESORICS'96 paper. CVS: A Compiler for the Analysis of Cryptographic Protocols Antonio Durante, Riccardo Focardi, and Roberto Gorrieri (speaker) CVS automatically translates protocols described in VSP, a domain-specific high-level language, into SPA (Security Process Algebra), a CCS-like process algebra. The resulting SPA description of the protocol can be given to the CoSeC tool for verification. (Gavin Lowe developed a similar tool, called Casper, that translates protocols into CSP.) The CoSeC analysis is based on non-interference: it attempts to show that the intruder cannot influence the observable behavior of honest participants in the protocol. If this attempt fails, the user is shown traces in which the honest participants' behavior is influenced by the intruder. The user decides inspection whether those traces represent violations of the protocol's correctness requirements; they are working to automate this step. Using these tools, they found a simple and apparently new attack on the Woo-Lam one-way authentication protocol. Martin Abadi mentioned that it is not clear what that protocol is intended to achieve, hence it is not clear what should be considered an attack. Cathy Meadows suggested that they consider using Millen's language CAPSL (instead of VSP) as an abstract notation for protocols. Process Algebra and Non-Interference Peter Ryan (speaker) and Steve Schneider The information security community has had difficulty giving a precise definition of non-interference, especially for non-deterministic systems. The authors show that non-interference is closely related to equivalence of systems, which is a central concept in the theory of process algebras. Different notions of equivalence lead naturally to different notions of non-interference. Thus, the lack of consensus on the definition of non-interference is closely related to the multiplicity of equivalences in the process-algebra literature. The authors demonstrate a correspondence between some definitions of non-interference and some notions of process equivalence. A benefit of understanding this relationship is that results from the process-algebra community can be exploited, e.g., results regarding composition and unwinding. A process-algebraic proof of completeness of a previously known set of rules for unwinding is given; the process-algebraic proof is cleaner and gives more insight than the original proof. Some ideas are described for generalizing non-interference to handle partial and conditional information flow. John McLean said that the proposed definition of non-interference seems quite natural, and that this was surprising, because the definition is also compositional, and he usually takes compositionality as a sign that a definition does not capture the meaning of non-interference. Peter replied that they could discuss this point in more detail off-line, but in the meantime, John might feel better knowing that their notion of non-interference is not preserved by refinement. What is Intransitive Noninterference? A. W. Roscoe (speaker) and M. H. Goldsmith Intransitive non-interference refers to information flow properties required of systems containing downgraders, in which it may be legitimate for information to flow indirectly between two users but not directly. The concept is illustrated by a secure file system, with a process that can downgrade files from high-security to low-security. Using this example, they show that the standard definition of intransitive non-interference in terms of a purge function is undesirably permissive: it allows the effects of "too many" high-level actions to become visible in the low-level view after a downgrading action. As a remedy, a definition based on determinism is proposed. Roughly, the determinism-based notion of non-interference is as follows: high-level actions are turned into non-deterministic choices, and if the low-level view is deterministic, then there is no information flow from the high level to the low level. This definition can be extended to yield a definition of intransitive non-interference that is not overly permissive.