Test isolation is a prerequisite for the correct execution of test suites on web applications. We present Test Execution Checkpointing, a method for efficient test isolation. Our method instruments web applications to support checkpointing and exploits this support to isolate and optimize tests. We have implemented and evaluated this method on five popular PHP web applications. The results show that our method not only provides test isolation essentially for free, it also reduces testing time by 44% on average.

Access-control requirements for physical spaces, like office buildings and airports, are best formulated from a global viewpoint in terms of system-wide requirements. For example, "there is an authorized path to exit the building from every room." In contrast, individual access-control components, such as doors and turnstiles, can only enforce local policies, specifying when the component may open. In practice, the gap between the system-wide, global requirements and the many local policies is bridged manually, which is tedious, error-prone, and scales poorly. We propose a framework to automatically synthesize local access control policies from a set of global requirements for physical spaces. Our framework consists of an expressive language to specify both global requirements and physical spaces, and an algorithm for synthesizing local, attribute-based policies from the global specification. We empirically demonstrate the framework's effectiveness on three substantial case studies. The studies demonstrate that access control synthesis is practical even for complex physical spaces, such as airports, with many interrelated security requirements.

The vacuous satisfaction of a temporal formula with respect to a model has been extensively studied in the literature. Although a universally accepted definition of vacuity does not yet exist, all existing proposals generalize, in one way or another, the antecedent failure of an implication to the syntax of a temporal logic. They are therefore syntactic: whether a model vacuously satisfies a formula is affected by semantics-preserving changes to the formula. This leads to inconsistent and counter-intuitive results. We propose an alternative: a semantic definition of vacuity for LTL where either two semantically equivalent LTL formulas are both satisfied vacuously in a model, or neither of them are. Our definition is based on a syntactic-invariant separation of LTL formulas, which gives rise to an algorithm for detecting semantic vacuity using trap properties. We also propose an alternative algorithm for Buchi automata, which can be used to detect the vacuous satisfaction of omega-regular properties as well as LTL formulas. We analyze this algorithm's worst-case complexity and, using real-world examples, demonstrate that semantic vacuity can be efficiently decided in practice.

Summary It is now possible to embed radio‐frequency identification tags into almost any physical device. However, issues regarding privacy remain a concern and limit their widespread use. We propose a scalable anonymous radio‐frequency identification authentication protocol using what we refer to as anonymous tickets. These tickets uniquely identify tags and are reusable. This considerably strengthens its non‐traceability and requires just search/query time, with minimal storage overhead on the back‐end system. We formally prove the protocol and compare the performance of the proposed protocol with selected works found in literature. Copyright © 2013 John Wiley & Sons, Ltd.

Decentralized and distributed access control systems are subject to communication and component failures. These can affect access decisions in surprising and unintended ways, resulting in insecure systems. Existing analysis frameworks however ignore the influence of failure handling in decision making. Thus, it is currently all but impossible to derive security guarantees for systems that may fail. To address this, we present (1) a model in which the attacker can explicitly induce failures, (2) failure-handling idioms, and (3) a method and an associated tool for verifying fail-security requirements, which describe how access control systems should handle failures. To illustrate these contributions, we analyze the consequences of failure handling in the XACML 3 standard and other domains, revealing security flaws.

There exist an abundant number of tools for aiding developers and penetration testers to spot common software security vulnerabilities. However, testers are often confronted with situations where existing tools are of little help because a) they do not account for a particular configuration of the SUT and b) they do not include tests for certain vulnerabilities. To cope with this we propose a tool that allows users to define attacker models where the payloads and the behavior are cleanly separated and that abstract away from low-level implementation details such as HTTP requests.

We define semi-valid input coverage (SVCov), the first coverage criterion for fuzz testing. Our criterion is applicable whenever the valid inputs can be defined by a finite set of constraints. SVCov measures to what extent the tests cover the domain of semi-valid inputs, where an input is semi-valid if and only if it satisfies all the constraints but one.

Efficiency of asynchronous optimistic fair exchange using trusted devices is studied. It is shown that three messages in the optimistic subprotocol are sufficient and necessary for exchanging idempotent items. When exchanging nonidempotent items, however, three messages in the optimistic subprotocol are sufficient only under the assumption that trusted devices have unbounded storage capacity. This assumption is often not satisfiable in practice. It is then proved that exchanging nonidempotent items using trusted devices with a bounded storage capacity requires exactly four messages in the optimistic subprotocol.

We propose a language for formal specification of service-oriented architectures. The language supports the integrated specification of communication level events, policy level decisions, and the interaction between the two. We show that the reach ability problem is decidable for a fragment of service-oriented architectures. The decidable fragment is well suited for specifying, and reasoning about, security-sensitive architectures. In the decidable fragment, the attacker controls the communication media. The policies of services are centered around the trust application and trust delegation rules, and can also express RBAC systems with role hierarchy. The fragment is of immediate practical relevance: We report on the specification and verification of two security-sensitive architectures, stemming from the e-government and e-health domains.

A majority of the existing privacy-friendly RFID protocols use the output of a cryptographic hash function in place of real identity of an RFID tag to ensure anonymity and untraceability. In order to provide unique identification for the tags, these protocols assume that the hash functions are collision resistant. We show that, under this assumption on the hash functions, a substantial number of the existing protocols suffer from a traceability problem that causes differentiating a tag from another. We propose a scalable privacy-friendly RFID protocol and describe its design and implementation issues. Our protocol substitutes the hash functions used for identification with anonymous tickets, thus avoiding the aforementioned traceability problem. The anonymous tickets are reusable. They nevertheless identify the tags uniquely, at any given point in time. The query and search algorithm of our proposed protocol is of O(1) time complexity, and it imposes small storage overhead on the back- end database. We show that the protocol is scalable, and compare its storage and computational requirements to some existing protocols. We formally prove the security requirements of our protocol, and mechanically analyze some of its requirements using the model checker OFMC.

Multi-party contract signing protocols specify how a number of signers can cooperate in achieving a fully signed contract, even in the presence of dishonest signers. This problem has been studied in different settings, yielding solutions of varying complexity. Here we assume the presence of a trusted third party that will be contacted only in case of a conflict, asynchronous communication, and a total ordering of the protocol steps. Our goal is to develop a lower bound on the number of messages in such a protocol. Using the notion of abort chaining, a specific type of attack on fairness of signing protocols, we derive the lower bound alpha^2 + 1, with alpha being the number of signers involved. We obtain the lower bound by relating the problem of developing fair signing protocols to the open combinatorial problem of finding shortest permutation sequences. This relation also indicates a way to construct signing protocols which are shorter than state-of-the-art protocols. We illustrate our approach by presenting the shortest three-party fair contract signing protocol.

A fuzzy automaton which handles real-valued data has been of interest to control society as a mean to tackle identification problem of dynamical systems. A firm basis to apply fuzzy automata (FA) with fuzzy alphabet is investigated, in a systematic way, to control and modeling applications within real-valued environments. In this way, a novel definition of transducer FA and its operating environment will be devised. The new definition yields a close connection between FA and rule-based fuzzy inference systems which provides an induction algorithm for FA. Despite of similarity in design phase, FA and rule-based inference engines have totally different behavior due to the effect of state dynamics. The latter concept will be discussed through a case study on modeling a time-dynamic process.