We carry out an analysis of message-passing concurrency primitives, namely a synchronous channel and an alt (alternation) construct, implemented in Scala. We model these primitives using the process algebra CSP, and analyse them using the model checker FDR. We consider the correctness properties of synchronisation linearisation (informally, that each completed operation execution corresponds to a correct synchronisation) and progressibility (informally, that executions don’t get stuck if they could synchronise): we show how these properties can be captured in CSP. Our initial analysis discovered an error in a previous implementation; our subsequent analysis helped us to produce a correct implementation. It turns out that a direct analysis of the composition of an alt and corresponding channels scales quite poorly. To overcome this, we perform a compositional analysis: we show that a channel and an alt each satisfies a more abstract description; and show that the composition of these abstract descriptions satisfies synchronisation linearisation and progressibility.

Abstract The parameterized verification problem seeks to verify all members of some collection of systems. We consider the parameterized verification problem applied to systems that are composed of an arbitrary number of component processes, together with some fixed processes. The components are taken from one or more families, each family representing one role in the system; all components within a family are symmetric to one another. Processes communicate via synchronous message passing. In particular, each component process has an identity, which may be included in messages, and passed to third parties. We extend Abdulla et al.’s technique of view abstraction, together with techniques based on symmetry reduction, to this setting. We give an algorithm and implementation that allows such systems to be verified for an arbitrary number of components: we do this for both safety and deadlock-freedom properties. We apply the techniques to a number of examples. We can model both active components, such as threads, and passive components, such as nodes in a linked list: thus our approach allows the verification of unbounded concurrent datatypes operated on by an unbounded number of threads. We show how to combine view abstraction with additional techniques in order to deal with other potentially infinite aspects of the analysis: for example, we deal with potentially infinite specifications, such as a datatype being a queue; and we deal with unbounded types of data stored in a datatype.

Abstract We investigate the cause of a deadlock in the implementation of a channel in a message-passing concurrency API. We model the channel implementation using the process algebra CSP, and then use the model checker FDR to find the cause of the deadlock. The bug is rather subtle, and arguably infeasible to spot by hand. We then propose a straightforward fix to the bug, and use CSP and FDR to verify this fix.

We present an extension of FDR, the model checker for the process algebra CSP, that exploits symmetry to reduce the size of the state space searched. We define what it means for a process to be symmetric with respect to a group of permutations on the transition labels. We factor the state space of the search by symmetry equivalence, mapping each state to a representative of its equivalence class, thereby considering all symmetric states together. We prove a powerful syntactic result, identifying conditions under which a process will be symmetric in a particular type. We show how to implement such a search using the powerful technique of supercombinators used in the implementation of FDR: we identify conditions on a supercombinator for it to be symmetric and explain how to apply a permutation to a state. Finally, we present a novel efficient technique for calculating representatives of equivalence classes, which normally finds unique representatives; our experiments suggest that this technique typically works faster than other techniques and in particular scales better.

Summary Linearizability is a well established correctness condition for concurrent datatypes. Informally, a concurrent datatype is linearizable if operation calls appear to have an effect, one at a time, in an order that is consistent with a sequential (specification) datatype, with each operation taking effect between the point at which it is called and when it returns. We present a testing framework for linearizabilty. The basic idea is to generate histories of the datatype randomly, and to test whether each is linearizable. We consider five algorithms—one existing, and four new—for testing whether a history of a concurrent datatype implementation is linearizable. Four of these are generic: they will work with any concurrent datatype for which there is a corresponding sequential specification datatype. The fifth considers specifically a history of a concurrent queue. We also combine algorithms in competition parallel in various ways. We perform an experimental evaluation of the different algorithms. We illustrate that the framework is very effective in finding bugs, and discuss the pragmatics of using the framework. Copyright © 2016 John Wiley & Sons, Ltd.

We consider models of CSP based on recording availability information, i.e. the models record what events could have been performed instead of those that were actually performed. We present many different varieties of such models. For each, we give a compositional semantics, congruent to the operational semantics, and prove full abstraction and no-junk results. We compare the expressiveness of the different models.

Abstract Many security protocols are built as the composition of an application-layer protocol and a secure transport protocol, such as TLS. There are several approaches to proving the correctness of such protocols. One popular approach is verification by abstraction, in which the correctness of the application-layer protocol is proven under the assumption that the transport layer satisfies certain properties, such as confidentiality. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on secure transport protocols; we consider both bilaterally and unilaterally authenticating secure transport protocols, such as bilateral and unilateral TLS. The paper’s main contribution is a proof of the model’s soundness. In particular, we prove that, subject to a suitable independence assumption, if there is an attack against the application-layer protocol when layered on top of a particular secure transport protocol, then there is an attack against the abstracted model of the application-layer protocol. In contrast to existing work in this area, the independence assumption consists of eight statically checkable conditions, meaning that it is not necessary to consider all possible runs of the protocol.

We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in “lassos”. Our algorithms typically exhibit about a four-fold speed-up over the corresponding sequential algorithms on an eight-core machine. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Security contains three papers that originally appeared at the Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS '10).The workshop was held on March 27-28, 2010, in Paphos, Cyprus, and affiliated with ETAPS 2010.The workshop brought together researchers interested in developing and applying formal techniques in the development of security-related applications.The three papers in this issue are significant extensions of the workshop papers, and were reviewed according to the normal Journal of Computer Security procedures.The first paper, "Quantitative information flow in interactive systems", by Mário Alvim, Miguel Andrés and Catuscia Palamidessi, considers information flow in a system where secrets and observables alternate during the computation.The authors show that if secrets can depend on the observables, then the system cannot be modelled validly by a classical information-theoretic channel.Instead, they show that this setting corresponds to the notion of channels with memory and feedback.Finally, they show that the channel capacity is a continuous function of a pseudometric based on the Kantorovich metric.The second paper, "Iterative enforcement by suppression: Towards practical enforcement theories", by Nataliia Bielova and Fabio Massacci, considers run-time security enforcement mechanisms.Such mechanisms aim to suppress bad behaviours of a monitored system (i.e., behaviours that do not satisfy the security policy) while not changing good behaviours.The authors observe that when a system does have a bad behaviour, there may be many ways of suppressing it, some of which may be more desirable than others.They define a notion of "better" enforcement, based on the number of elements from the original execution that should be suppressed in order to obtain a legal execution.They then propose a new class of enforcement mechanism, which they show is better than the previously proposed longest-validprefix mechanism.The final paper, "Modular plans for secure service composition", by Gabriele Costa, Pierpaolo Degano and Fabio Martinelli, considers service networks built from open services, i.e. services with unknown components.The authors model services in a variant of the λ-calculus; compliance of a service to a local policy is established by model checking a safe abstraction of the service obtained from a type-and-effect system.The authors describe orchestration plans, which drives the execution at runtime, mapping requests to services.Finally, they define a composition strategy for safely synthesizing a global orchestration plan.

In this paper, we analyse the Transport Layer Security (TLS) protocol (in particular, bilateral TLS in public-key mode) within the strand spaces setting. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW), IEEE Computer Society, 2003, pp. 141–154, Broadfoot and Lowe suggested an abstraction of TLS. The abstraction models the security services that appear to be provided by the protocol to the high-level security layers. The outcome of our analysis provides a formalisation of the security services provided by TLS and proves that, under reasonable assumptions, the abstract model suggested by Broadfoot and Lowe is correct. To that end, we reduce the complexity of the protocol using fault-preserving simplifying transformations. We extend the strand spaces model in order to include the cryptographic operations used in TLS and facilitate its analysis. Finally, we use the extended strand spaces model to fully analyse the public-key mode of bilateral TLS with its two main components: the Handshake and Record Layer protocols.

Security architectures often make use of secure transport protocols to protect network messages: the transport protocols provide secure channels between hosts. In this paper we present a hierarchy of specifications for secure channels. We give trace specifications capturing a number of different confidentiality and authentication properties that secure channels might satisfy, and compare their strengths. We use the various modes of TLS as a running example, and we give examples of single-message protocols that we believe satisfy the channel specifications.

Abstract In this paper we consider the relationship between refinement-oriented specification and specifications using a temporal logic. We investigate the extent to which one can check whether a program in a process algebra, such as Communicating Sequential Processes (CSP), satisfies a temporal logic specification using a refinement-based model checker, such as FDR. We consider what atomic formulae are appropriate in a temporal logic for specifying communicating processes, in particular where one wants to talk about the availability of events. We then show that, perhaps surprisingly, the standard stable failures model is not adequate for capturing specifications in such a logic: instead the refusal traces model must be used. We formalise the logic by giving it a semantics in this model. We show that the temporal operators eventually and until , and negation, cannot, in general, be tested for via simple refinement checks. For the remaining fragment of the logic, we present a translation into simple refinement checks. Finally, we show that refusal traces equivalence is characterised by a slightly augmented version of that fragment.

The reverse path forwarding algorithm is a protocol for distributing messages throughout networks. The intention is to preserve correctness - messages sent will eventually be received by all nodes in the originator's connected component - whilst minimising the number of propagations of each message. We use a variety of analysis techniques to identify necessary additional constraints, and to prove correctness under these conditions. In particular we present counter examples found by the model-checkers FDR and the Alloy Analyzer, illustrating that the protocol is incorrect if the cost of links is dependent upon the node using that link. We then consider the case where the cost of links is independent of the node using that link; we use a special-purpose network sampling program to increase confidence in the correctness of this stricter protocol, and then perform a hand-proof to verify correctness. We conclude with a discussion of the suitability of these techniques for reasoning about protocols of this complexity.

In this paper we consider guessing attacks upon security protocols, where an intruder guesses one of the values used (typically a poorly-chosen password) and then seeks to verify that guess. We formalise such attacks, and in particular the way in whi

We extend definitions of information flow so as to quantify the amount of information passed; in other words, we give a formal definition of the capacity of covert channels. Our definition uses the process algebra CSP, and is based upon counting the

In this paper, we consider techniques for designing and analyzing distributed security transactions. We present a layered approach, with a high-level security transaction layer running on top of a lower-level secure transport protocol. The secure transport protocol provides protection against dishonest outsiders, while the transaction layer can be designed to provide protection against dishonest insiders. We specify generic services that one might expect such secure transport protocols to provide. We give examples of this layered approach, with the aim of demonstrating that the separation of concerns allows for a cleaner, more intuitive design. We consider how to analyze such a layered security architecture.

A type flaw attack on a security protocol is an attack where a field that was originally intended to have one type is subsequently interpreted as having another type. A number of type flaw attacks have appeared in the academic literature. In this paper we prove that type flaw attacks can be prevent ed using a simple technique of tagging each field with some information indicating its intended type.

Recent techniques for analyzing security protocols have tended to concentrate upon the small protocols that are typically found in the academic literature. However, there is a huge gulf between these and most large commercial protocols: the latter typically have many more fields, and much higher le vels of nested encryption. As a result, existing techniques are difficult to apply directly to these large protocols. In this paper we develop the notion of fault-preserving simplifying transformations: transformations that have the property of preserving insecurities; the effect of such transformations is that if we can verify the transformed protocol, then we will have verified the original protocol. We identify a number of such fault-preserving simplifying transformations, and use them in the analysis of a commercial protocol.

A type flaw attack on a security protocol is an attack where a field that was originally intended to have one type is subsequently interpreted as having another type. A number of type flaw attacks have appeared in the academic literature. In this paper we prove that type flaw attacks can be prevented using a simple technique of tagging each field with some information indicating its intended type.

Recent techniques for analyzing security protocols have tended to concentrate upon the small protocols that are typically found in the academic literature. However there is a huge gulf between these and most large commercial protocols: the latter typically have many more fields, and much higher levels of nested encryption. As a result, existing techniques are difficult to apply directly to these large protocols. In this paper we develop the notion of safe simplifying transformations: transformations that have the property of preserving insecurities; the effect of such transformations is that if we can verify the transformed protocol, then we will have verified the original protocol. We identify a number of such safe simplifying transformations, and use them in the analysis of a commercial protocol.

Model checking approaches to the analysis of security protocols have proved remarkably successful. The basic approach is to produce a model of a small system running the protocol, together with a model of the most general intruder who can interact wi

Model checking approaches to the analysis of security protocols have proved remarkably successful. The basic approach is to produce a model of a small system running the protocol, together with a model of the most general intruder who can interact with the protocol, and then to use a state exploration tool to search for attacks. This has led to a number of new attacks upon protocols being discovered. However if no attack is found, this only tells one that there is no attack upon the small system modelled; there may be an attack upon some larger system. This is the question considered in the paper: the author presents sufficient conditions on the protocol and its environment such that if there is no attack upon a particular small system (with one honest agent for each role of the protocol) leading to a breach of secrecy (using a fairly strong definition of secrecy), then there is no attack on any larger system leading to a breach of secrecy (using a more general definition of secrecy).

In recent years, a method for analyzing security protocols using the process algebra CSP (Hoare, 1985) and its model checker FDR (Roscoe, 1994) has been developed. This technique has proved remarkably successful, and has been used to discover a numbe

In recent years, a method for analyzing security protocols using the process algebra CSP (C.A.R. Hoare, 1985) and its model checker FDR (A.W Roscoe, 1994) has been developed. This technique has proved successful, and has been used to discover a number of attacks upon protocols. However the technique has required producing a CSP description of the protocol by hand; this has proved tedious and error prone. We describe Casper, a program that automatically produces the CSP description from a more abstract description, thus greatly simplifying the modelling and analysis process.

Many security protocols have the aim of authenticating one agent to another. Yet there is no clear consensus in the academic literature about precisely what "authentication" means. We suggest that the appropriate authentication requirement will depend upon the use to which the protocol is put, and identify several possible definitions of "authentication". We formalize each definition using the process algebra CSP, use this formalism to study their relative strengths, and show how the model checker FDR can be used to test whether a system running the protocol meets such a specification.

We use FDR (Failures Divergence Refinement), a model checker for CSP, to detect errors in the TMN protocol (M. Tatebayashi et al., 1990). We model the protocol and a very general intruder as CSP processes, and use the model checker to test whether the intruder can successfully attack the protocol. We consider three variants on the protocol, and discover a total of 10 different attacks leading to breaches of security.

Many security protocols have appeared in the literature, with aims such as agreeing upon a cryptographic key, or achieving authentication. However, many of these have been shown to be flawed. In this paper we present a number of new attacks upon security protocols, and discuss ways in which we may avoid designing incorrect protocols in the future.

In this paper, we define a formal model for reasoning about resource allocation and scheduling in real-time systems. We extend the model of Scholefield, Zedan and He [3], which models the functionality of agents in the language TAM. Our extended model allows us to argue about the resource requirements of real-time distributed systems, and so identify conflicts upon resources. We can use the model to define and reason about schedulers that map jobs onto resources. The model will aid in the important transformation from an initial design for a system to an actual implementation with jobs scheduled on processors.

We describe the Temporal Agent Model (TAM) together with its associated refinement calculus. The calculus is based on a wide-spectrum language within which functional and temporal properties can be expressed in either abstract (i.e. specification) or concrete (i.e. design) terms. The refinement process transforms abstract specifications to concrete designs through successive applications of sound refinement laws. An extension to the calculus allows us to calculate a scheduler for the resulting design. We present a specification paradigm based on splitting the functional and temporal requirements, and describe refinement techniques based on this paradigm. We illustrate the calculus with an example taken from the avionics industry.