%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % Foundations of Computer Security - FCS'03 % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Editor: Iliano Cervesato, iliano at itd.nrl.navy.mil Last Updated: Fri Jun 6 2003 Size: 13 entries Source: electronic proceedings LICS'03 Workshop on Foundations of Computer Security --- FCS'03 Ottawa, Canada 26-27 June 2003 ISBN: none @InProceedings{Kuster:FCS:2003, author = "Dale Miller", institution = "INRIA/Futurs \& \'Ecole polytechnique, France", title = "Encryption as an abstract data-type: An extended abstract", abstract = "At the Dolev-Yao level of abstraction, security protocols can be specified using multisets rewriting. Such rewriting can be modeled naturally using proof search in linear logic. The linear logic setting also provides a simple mechanism for generating nonces and session and encryption keys via eigenvariables. We illustrate several additional aspects of this direct encoding of protocols into logic. In particular, encrypted data can be seen naturally as an abstract data-type. Entailments between security protocols as linear logic theories can be surprisingly strong. We also illustrate how the well-known connection in linear logic between bipolar formulas and general formulas can be used to show that the asynchronous model of communication given by multiset rewriting rules can be understood, more naturally as asynchronous process calculus (also represented directly as linear logic formulas). The familiar proof theoretic notion of interpolants can also serve to characterize communication between a role and its environment.", pages = "3--14", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{Ktari:FCS:2003, author = "B\'echir Ktari", institution = "Laval University, Canada", title = "A 3-Valued Logic for the Specification and the Verification of Security Properties", abstract = "The main intent of this paper is the definition of a 3-valued logic for the specification and the verification of security properties. This is a part of a large initiative that we undertook a few years ago to address malicious code detection in commercial off-the-shelf software products. Building on top of the existing approaches, we have established a framework that stems from a combination of self-certified code technology and model-checking techniques. In this paper, we propose a logic with a 3-valued semantics in order to be able to reason under uncertainty. We also endow our logic with a tableau-based proof system that is proven to be finite, and to be sound and complete with respect to the denotational semantics of the logic. Furthermore, we propose some ideas that may lead to important future extensions. For instance, we show how the use of variables and types can lead to a more efficient verification.", booktitle = "Foundations of Computer Security", pages = "15--25", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{HarrisonTullsenHook:FCS:2003, author = "William Harrison and Mark Tullsen, and James Hook", institution = "Oregon Graduate Institute, USA", title = "Domain Separation by Construction", abstract = "This paper advocates a novel approach to language-based security: by structuring software with monads (a form of abstract data type for effects), we are able to maintain separation of effects by construction. The thesis of this work is that well-understood properties of monads and monad transformers aid in the construction and verification of secure software. We introduce a formulation of non-interference based on monads rather than the typical trace-based formulation. Using this formulation, we prove a non-interference style property for a simple instance of our system model. Because monads may be easily and safely represented within any pure, higher-order, typed functional language, the resulting system models may be directly realized within such a language.", booktitle = "Foundations of Computer Security", pages = "29--42", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{MalladiAlves-Foss:FCS:2003, author = "Sreekanth Malladi and Jim Alves-Foss", institution = "University of Idaho, USA", title = "How to prevent type-flaw guessing attacks on password protocols", abstract = "A message in a protocol is said to have a type-flaw if it was created with some intended type, but is later received and treated as a different type. A type-flaw guessing attack is an attack where a password is guessed and verified by inducing type-flaws in a protocol. Heather et al. prove that attacks that use type-flaws can be prevented if honest agents tag messages with their intended types. However, their tagging scheme cannot be used in a password protocol since it allows a guess to be directly verified using the tags inside password encryptions. In this paper we prove that, by following a modification of Heather et al.'s scheme, most type-flaw guessing attacks can still be prevented.", booktitle = "Foundations of Computer Security", pages = "43--57", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{HoumaniMejri:FCS:2003, author = "Hanane Houmani and Mohamed Mejri", institution = "Laval University, Canada", title = "Secure Protocols for Secrecy", abstract = "This paper aims to ensure the correctness of cryptographic protocols with respect to the secrecy property. The idea is to establish some sufficient conditions (hypotheses) under which the correctness of a given protocol is guaranteed. Intuitively, a protocol is said to be correct with respect to the secrecy property if every valid trace (a trace in which all honest agents act according to the protocols specification and any message used by the intruder is previously defined) does not leak any sensitive information. To this end, we give some conditions that restrict what honest users participating in the protocol can send as messages.", booktitle = "Foundations of Computer Security", pages = "59--68", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{Wright:FCS:2003, author = "Rebecca Wright", institution = "Stevens Institute, USA", title = "Privacy in Today's World: Solutions and Challenges", abstract = "Privacy is being increasingly eroded as technological advances make it possible to capture, store, and process large amounts of personal data. In this talk, I will overview the current privacy landscape and outline some of the important problems in this area. I will also describe some of my work in this area, on privacy-protecting statistical analysis. Suppose a client wishes to compute some aggregate statistics on a privately-owned data base. The data owner wants to protect the privacy of the personal information in the data base, while the client does not want to reveal his selection criteria. Privacy-protecting statistical analysis allows the client and data owner to interact in such a way that the client learns the desired aggregate statistics, but does not learn anything further about the data; the data owner leans nothing about the client's query. Motivated by this application, we consider the more general problem of ''selective private function evaluation,'' in which a client can privately compute an arbitrary function over a database. We present various approaches for constructing efficient selective private function evaluation protocols, both for the general problem and for privacy-protecting statistical analysis.", booktitle = "Foundations of Computer Security", pages = "71", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June", note = "Invited Talk" } @InProceedings{Kikuchi:FCS:2003, author = "Hiroaki Kikuchi", institution = "Tokai University, Japan", title = "Oblivious Comparator and its Application to Secure Auction Protocol", abstract = "This paper presents a protocol for Secure Function Evaluation (SFC) in which n players have secret inputs E[a1], E[a2], ... , E[an], of a known boolean function f, and they collaborate to compute the ciphertext of the output of the boolean function, E[f(a1, ... , an)] . The main result is a completeness theorem (Theorem 3.1) which states that an arbitrary function can be evaluated at the oblivious party without help ofprivate information. The proposed protocol is based on the Jakobsson and Juels's Mix-and-Match scheme in which the truth table of a target function is row-wise randomized (mixing) using a Mix network, and then players perform ``matching'' the designated output ciphertext and the corresponding rows. The biggest difference between the proposed SFC and the Mix-and-Match is that the proposed protocol does not require any involution of key holders to evaluate function, while the Mix-and-Match needs key holders to perform threshold decryptions at every step of evaluation of boolean gates. One disadvantage of the proposed scheme is the Reed-Muller expansion involves an exponential blow-up in the number of input, n, as conventional schemes such as CyptoComputer proposed by Sander, Young, and Yung. This paper presents an efficient construction for a primitive called `oblivious comparator' with n-round complexity between the comparator and n players but the bandwidth spent by one communication is independent from n (linear to the size of values to be compared), and hence it does not suffer the blow-up in n. The oblivious comparator is suitable to implement a secure auction because an auctioneer communicates with bidders once at time, and performs evaluation without help of trusted key holders. In addition, the proposed construction allows arbitrary complicated functions including a search for second highest, a resolution the winner, and a dynamic programming (for combinatorial auction).", pages = "75--84", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{BorealeBuscemi:FCS:2003, author = "Michele Boreale and Maria Grazia Buscemi", institution = "Universit\`a di Firenze, Italy and Universit\`a di Pisa, Italy", title = "On the Symbolic Analysis of Low-Level Cryptographic Primitives: Modular Exponentiation and the Diffie-Hellman Protocol", abstract = "Automatic methods developed so far for analysis of security protocols only model a limited set of cryptographic primitives (often, only encryption and concatenation) and abstract from low-level features of cryptographic algorithms. This paper is an attempt towards closing this gap. We propose a symbolic technique and a decision method for analysis of protocols based on modular exponentiation, such as Diffie-Hellman key exchange. We introduce a protocol description language along with its semantics. Then, we propose a notion of symbolic execution and, based on it, a verification method. We prove that the method is sound and complete with respect to the language semantics.", booktitle = "Foundations of Computer Security", pages = "85--96", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{Sabelfeld:FCS:2003, author = "Andrei Sabelfeld", institution = "Cornell University, USA", title = "Language-Based Information Security", abstract = "Modern computing systems are increasingly vulnerable to application-level attacks. These attacks are particularly dangerous because they circumvent the standard low-level protection mechanisms (such as OS-based monitors and access control). Furthermore, application-level attacks are often easy to create (or simply download and launch) - exactly because of their high-level nature. Because standard security low-level enforcement mechanisms offer only limited protection against application-level attacks, there is high demand for models of language-based security aimed at defending against threats at the programming-language and, hence, application level. This talk concentrates on the preservation of information confidentiality by potentially malicious and/or buggy applications. Building on the technology of programming languages (such as programming-language semantics, type-based analysis, and program transformation) we develop a series of security policies and enforcement mechanisms for sequential, concurrent, and distributed programs that allow for modeling and statically analyzing information flow in a given program. The soundness of our security analyses guarantees the absence of insecure information flows. This means that if a program passes the analysis then it may not compromise confidentiality during the execution. We show that our approach is capable of detecting timing and probabilistic covert channels, i.e., the attacker is prevented from learning sensitive information by making timing and stochastic observations about secure programs. Joint work with David Sands and Heiko Mantel.", pages = "99", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June", note = "Invited Talk" } @InProceedings{XiaHook:FCS:2003, author = "Songtao Xia and James Hook", institution = "Oregon Graduate Institute, USA", title = "An Implementation of Abstraction-carrying Code", abstract = "Abstraction-carrying code (ACC) provides a mechanism to certify temporal properties of mobile programs. This certification has many potential applications, including high confidence extension of an operating system kernel. The size of a traditional, proof-based certificate tends to expand drastically because of the state explosion problem. In ACC, we use an abstract interpretation of the mobile program as a certificate. A client receiving the code and the certificate will first validate the abstraction and then run a model checker to verify the temporal property. The size of a typical certificate for a non-trivial temporal property is usually significantly smaller than the size of the program. We have developed ACCEPT, a prototype certifier for programs whose properties can be expressed as LTL formulas which do not use the next-operator. ACCEPT produces certificates for assembly programs; but it also assumes access to the higher level language source code as well. Several novel aspects of ACCEPT are: 1) the certifier produces a predicate abstraction which is used as a certificate; 2) the abstraction is valid for the source level program and the compiler maintains this validity for the assembly level program; 3) an index-typed assembly language SDTAL is adopted to encode the certificate; and 4) the abstraction is validated by type-checking the SDTAL program. This paper focuses on the representation of a predicate abstraction as type annotations on the assembly level program. The soundness of SDTAL's type system guarantees the soundness of the abstraction validation. We also report on our initial experience with ACCEPT.", pages = "103--115", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" } @InProceedings{LafranceMullins:FCS:2003, author = "St\'ephane Lafrance and John Mullins", institution = "'Ecole Polytechnique de Montr\'eal, Canada", title = "Symbolic Approach to the Analysis of Security Protocols", abstract = "The specification and validation of security protocols often requires viewing function calls - like encryption/decryption and the generation of fake messages - explicitly as actions within the process semantics. Following this approach, this paper introduces a symbolic framework based on value-passing processes able to handle symbolic values like fresh nonces, fresh keys, fake address and fake messages. The main idea in our approach is to assign to each value-passing process a formula describing the symbolic values conveyed by its semantics. In such symbolic processes, called processes, the formulas are drawn from a logic based on a message algebra equipped with encryption, signature and hashing primitives. The symbolic operational semantics of a process is then established through semantic rules updating formulas by adding restrictions over the symbolic values, as required for the process to evolve. We then prove that the logic required from the semantic rules is decidable. We also define a bisimulation equivalence between processes; this amounts to a generalisation of the standard bisimulation equivalence between (non-symbolic) value-passing processes. Finally, we provide a complete symbolic bisimulation method for constructing the bisimulation between processes.", booktitle = "Foundations of Computer Security", pages = "117--135", year = "2003", editor = "Iliano Cervesato", address = "Ottawa, Canada", month = "26--27 June" }