We present a methodology for the probabilistic modeling of failure dependencies in large, complex systems using Markov Logic Networks (MLNs), a state-of-the-art probabilistic relational modeling technique in machine learning. We illustrate this modeling methodology on example system architectures, and show how the the Probabilistic Consistency Engine (PCE) tool can create and analyze failure-dependency models. We compare MLN-based analysis with analytical symbolic analysis to validate our approach. The latter method yields bounds on the expected system behaviors for different component-failure probabilities, but it requires closed-form representations and is therefore often an impractical approach for complex system analysis. The MLN-based method facilitates techniques of early design analysis for reliability (e.g., probabilistic sensitivity analysis). We analyze two examples - a portion of the Time-Triggered Ethernet (TTEthernet) communication platform used in space, and an architecture based on Honeywell's Cabin Air Compressor(CAC) - that highlight the value of the MLN-based approach for analyzing failure dependencies in complex cyber-physical systems.

Formal analysis of security protocols is largely based on a set of assumptions commonly referred to as the Dolev–Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiset rewriting with existential quantification. Strand spaces provide a simple and economical approach to analysis of completed protocol runs by emphasizing causal interactions among protocol participants. The multiset rewriting formalism provides a very precise way of specifying finite-length protocols with unboundedly many instances of each protocol role, such as client, server, initiator, or responder. A number of modifications to each system are required to produce a meaningful comparison. In particular, we extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands. The relationship we illustrate here between multiset rewriting specifications and strand spaces thus suggests refinements to both frameworks, and deepens our understanding of the Dolev–Yao model.

We formalize the Dolev–Yao model of security protocols, using a notation based on multiset rewriting with existentials. The goals are to provide a simple formal notation for describing security protocols, to formalize the assumptions of the Dolev–Yao model using this notation, and to analyze the complexity of the secrecy problem under various restrictions. We prove that, even for the case where we restrict the size of messages and the depth of message encryption, the secrecy problem is undecidable for the case of an unrestricted number of protocol roles and an unbounded number of new nonces. We also identify several decidable classes, including a DEXP-complete class when the number of nonces is restricted, and an NP-complete class when both the number of nonces and the number of roles is restricted. We point out a remaining open complexity problem, and discuss the implications these results have on the general topic of protocol analysis.

A scalable and expressive peer-to-peer (P2P) networking and computing framework requires efficient resource discovery services. Here we propose NEVRLATE, for Network-Efficient Vast Resource Lookup At The Edge, an efficient organization of directories or directory mirrors, providing a scalable distributed resource discovery service. NEVRLATE organizes directory servers in an approximate two-dimensional grid, or a set of sets of servers, for registration to occur in one 'horizontal' dimension, and lookup to occur in the other 'vertical' dimension. The payoff of organizing n servers into a structure like this is to achieve O(pn) message complexity for registration, and nearly constant complexity lookup. At extra cost NEVRLATE can provide fault tolerance, high availability and security, anonymity, and privacy. The protocol described can be seen as a way to organize Gnutella supernodes, or as a performance extension of Freenet's architecture. In addition, it supports expressive lookup mechanisms, and may provide a basis for a truly scalable worldwide infrastructure for the semantic and the extended web.

The development of new classes of distributed applications such as telephony, remote video, and virtual reality introduces new quality requirements that make inadequate even the current best-effort service model provided by international networks. Re

We consider scalable certificate revocation in a public-key infrastructure (PKI). We introduce depender graphs, a new class of graphs that support efficient and fault-tolerant revocation. Nodes of a depender graph are participants that agree to forward revocation information to other participants. Our depender graphs are k-redundant, so that revocations are provably guaranteed to be received by all non-failed participants even if up to k−1 participants have failed. We present a protocol for constructing k-redundant depender graphs that has two desirable properties. First, it is load-balanced, in that no participant need have too many dependers. Second, it is localized, in that it avoids the need for any participant to maintain the global state of the depender graph. We also give a localized protocol for restructuring the graph in the event of permanent failures.

Although there have been attempts to develop code transformations that yield tamper-resistant software, no reliable software-only methods are know. This paper studies the hardware implementation of a form of execute-only memory (XOM) that allows instructions stored in memory to be executed but not otherwise manipulated. To support XOM code we use a machine that supports internal compartments---a process in one compartment cannot read data from another compartment. All data that leaves the machine is encrypted, since we assume external memory is not secure. The design of this machine poses some interesting trade-offs between security, efficiency, and flexibility. We explore some of the potential security issues as one pushes the machine to become more efficient and flexible. Although security carries a performance penalty, our analysis indicates that it is possible to create a normal multi-tasking machine where nearly all applications can be run in XOM mode. While a virtual XOM machine is possible, the underlying hardware needs to support a unique private key, private memory, and traps on cache misses. For efficient operation, hardware assist to provide fast symmetric ciphers is also required.

We consider scalable certificate revocation in a public-key infrastructure (PKI). We introduce depender graphs, a new class of graphs that support efficient and fault-tolerant revocation. Nodes of a depender graph are participants that agree to forward revocation information to other participants. Our depender graphs are k-redundant, so that revocations are provably guaranteed to be received by all nonfailed participants even if up to k \\Gamma1 participants have failed. We present a protocol for constructing k-redundant depender graphs that has two desirable properties. First, it is load-balanced, in that no participant need have too many dependers. Second, it is localized, in that it avoids the need for any participant to maintain the global state of the depender graph. We also give a localized protocol for restructuring the graph in the event of permanent failures. 1. INTRODUCTION Public keys and their certificates eventually become invalid. Most certificates have an expiration dat...

Formal analysis of security protocols is largely based on an set of assumptions commonly referred to as the Dolev-Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiuser rewriting with existential quantification. Although it is fairly intuitive that these two languages should be equivalent in some way, a number of modifications to each system are required to obtain a meaningful equivalence. We extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. We omit the initialization part of the multiset rewriting setting, which formalizes the choice of initial data, such as shared public or private keys, and which has no counterpart in the stand space setting. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands.

Most formal approaches to security protocol analysis are based on a set of assumptions commonly referred to as the "Dolev-Yao model". In this paper, we use a multiset rewriting formalism, based on linear logic, to state the basic assumptions of this model. A characteristic of our formalism is the way that existential quantification provides a succinct way of choosing new values, such as new keys or nonces. We define a class of theories in this formalism that correspond to finite-length protocols, with a bounded initialization phase but allowing unboundedly many instances of each protocol role (e.g., client, sewer; initiator or responder). Undecidability is proved for a restricted class of these protocols, and PSPACE-completeness is claimed for a class further restricted to have no new data (nonces). Since it is a fragment of linear logic, we can use our notation directly as input to linear logic tools, allowing us to do proof search for attacks with relatively little programming effort, and to formally verify protocol transformations and optimizations.

Despite advances in recent years in the area of mandatory access control in database systems, today's information repositories remain vulnerable to inference and data association attacks that can result in serious information leakage.Such information leakage can be prevented by properly classifying information according to constraints that express relationships among the security levels of data objects.In this paper we address the problem of classifying information by enforcing explicit data classification as well as inference and association constraints.We formulate the problem of determining a classification that ensures satisfaction of the constraints, while at the same time guaranteeing that information will not be unnecessarily overclassified.We present an approach to the s;olution of this problem and give an algorithm implementing it which is linear in simple cases, and low-order polynomial (n") in the general case.We also analyze a variant of the problem that is NP-hard. IntroductionMandatory policies control access to information on the basis of classifications, taken from a partially ordered set, assigned to data objects and subjects requesting access to them.Classifications assigned to information reflect the sensitivity of that information, while classifications assigned to subjects reflect their trustworthiness not to disclose the information they access to subjects not cleared to see it.By controlling read and write operations accordingly -allowing subjects to read information whose classification is dominated by their level #and write information only at a level that dominates theirs -mandatory policies provide a sim-

A class of linear logic proof games is developed, each with a numeric score that depends on the number of preferred axioms used in a complete or partial proof tree. The complexity of these games is analyzed for the NP-complete multiplicative fragment (MLL) extended with additive constants and the PSPACE-complete multiplicative, additive fragment (MALL) of propositional linear logic. In each case, it is shown that it is as hard to compute an approximation of the best possible score as it is to determine the optimal strategy. Furthermore, it is shown that no efficient heuristics exist unless there is an unexpected collapse in the complexity hierarchy.

We develop a framework for analyzing security protocols in which protocol adversaries may be arbitrary probabilistic polynomial-time processes. In this framework, protocols are written in a form of process calculus where security may be expressed in terms of observational equivalence, a standard relation from programming language theory that involves quantifying over possible environments that might interact with the protocol. Using an asymptotic notion of probabilistic equivalence, we relate observational equivalence to polynomial-time statistical tests and discuss some example protocols to illustrate the potential of this approach. 1 Introduction Protocols based on cryptographic primitives are commonly used to protect access to computer systems and to protect transactions over the internet. Two well-known examples are the Kerberos authentication scheme [15, 14], used to manage encrypted passwords, and the Secure Sockets Layer [12], used by internet browsers and servers to carry out...

A reconfigurable fault tolerant system achieves the attributes of dependability of operations through fault detection, fault isolation and reconfiguration, typically referred to as the FDIR paradigm. Fault diagnosis is a key component of this approach, requiring an accurate determination of the health and state of the system. An imprecise state assessment can lead to catastrophic failure due to an optimistic diagnosis, or conversely, result in underutilization of resources because of a pessimistic diagnosis. Differing from classical testing and other off-line diagnostic approaches, we develop procedures for maximal utilization of the system state information to provide for continual, on-line diagnosis and reconfiguration capabilities as an integral part of the system operations. Our diagnosis approach, unlike existing techniques, does not require administered testing to gather syndrome information but is based on monitoring the system message traffic among redundant system functions. We present comprehensive on-line diagnosis algorithms capable of handling a continuum of faults of varying severity at the node and link level. Not only are the proposed algorithms on-line in nature, but are themselves tolerant to faults in the diagnostic process. Formal analysis is presented for all proposed algorithms. These proofs offer both insight into the algorithm operations and facilitate a rigorous formal verification of the developed algorithms.

The decision problem is studied for fragments of second order linear logic without modalities. It is shown that the structural rules of contraction and weakening may be simulated by second order propositional quantifiers and the multiplicative connectives. Among the consequences are the undecidability of the intuitionistic second order fragment of propositional multiplicative linear logic and the undecidability of multiplicative linear logic with first order and second order quantifiers.

We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Herbrand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for first-order MALL is in NEXPTIME, and first-order MLL is in NP. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability.>

It is proved that the standard sequent calculus proof system of linear logic is equivalent to a natural deduction style proof system. The natural deduction system is used to investigate the pragmatic problems of type inference and type safety for a linear lambda calculus. Although terms do not have a single most-general type (for either the standard sequent presentation or the natural deduction formulation), there is a set of most-general types that may be computed using unification. The natural deduction system also facilitates the proof that the type of an expression is preserved by any evaluation step. An execution model and implementation is described, using a variant of the three-instruction machine. A novel feature of the implementation is that garbage-collected nonlinear memory is distinguished from linear memory, which does not require garbage collection and for which it is possible to do secure update in place.>

We study the complexity of type inference for programming languages with subtypes. There are three language variations that effect the problem: (i) basic functions may have polymorphic or more limited types, (ii) the subtype hierarchy may be fixed or vary as a result of subtype declarations within a program, and (iii) the subtype hierarchy may be an arbitrary partial order or may have a more restricted form, such as a tree or lattice. The naive algorithm for infering a most general polymorphic type, undervariable subtype hypotheses, requires deterministic exponential time. If we fix the subtype ordering, this upper bound grows to nondeterministic exponential time. We show that it is NP-hard to decide whether a lambda term has a type with respect to a fixed subtype hierarchy (involving only atomic type names). This lower bound applies to monomorphic or polymorphic languages. We give PSPACE upper bounds for deciding polymorphic typability if the subtype hierarchy has a lattice structure or the subtype hierarchy varies arbitrarily. We also give a polynomial time algorithm for the limited case where there are of no function constants and the type hierarchy is either variable or any fixed lattice.

An embedding of the implicational propositional intuitionistic logic (IIL) into the nonmodal fragment of intuitionistic linear logic (IMALL) is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofs.>

It is shown that, unlike most other propositional (quantifier-free) logics, full propositional linear logic is undecidable. Further, it is provided that without the model storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. Also established are membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for certain fragments of noncommutative propositional linear logic.>

We have discovered an efficient algorithm for matching and unification in associative-commutative (AC) equational theories. In most cases of AC unification our method obviates the need for solving diophantine equations, and thus avoids one of the bottlenecks of other associative-commutative unification techniques. The algorithm efficiently utilizes powerful constraints to eliminate much of the search involved in generating valid substitutions. Moreover, it is able to generate solutions lazily, enabling its use in an SLD-resolution-based environment like Prolog. We have found the method to run much faster and use less space than other associative-commutative unification procedures on many commonly encountered AC problems.

Lattice operations such as greatest lower bound (GLB), least upper bound (LUB), and relative complementation (BUTNOT) are becoming more and more important in programming languages supporting object inheritance. We present a general technique for the efficient implementation of such operations based on an encoding method. The effect of the encoding is to plunge the given ordering into a boolean lattice of binary words, leading to an almost constant time complexity of the lattice operations. A first method is described based on a transitive closure approach. Then a more space-efficient method minimizing code-word length is described. Finally a powerful grouping technique called modulation is presented, which drastically reduces code space while keeping all three lattice operations highly efficient. This technique takes into account idiosyncrasies of the topology of the poset being encoded that are quite likely to occur in practice. All methods are formally justified. We see this work as an original contribution towards using semantic (vz., in this case, taxonomic) information in the engineering pragmatics of storage and retrieval of (vz., partially or quasi-ordered) information.