Scalability is a central concern of Byzantine Fault Tolerant (BFT) distributed protocols. The ubiquitous approach to work around the well-known Dolev-Reischuk Ω(n²) communication complexity lower bound is to use a random selection process to draw a hopefully small committee from a population of agents to run the communication-heavy protocol. We propose a notion of hierarchical consensus that combines two sub-protocols: an optimistic primary sub-protocol that can tolerate less than 1/2 failures and a fallback secondary protocol that can tolerate less than 1/3 failures; we achieve the higher failure threshold by requiring a weaker notion of liveness for the primary. This distinction between the level of fault tolerance between primary and secondary is reflected in the size of committees implementing these protocols. For a population of agents with close to 2/3 of honest agents, we need to select a committee with hundreds of agents to reach the level of tolerance expected for the primary, whereas we need thousands to reach the level expected for the secondary with a very small probability of error ε. Our hierarchical construct is such that if the primary comes to a decision, it can simply propagate it to the secondary protocol, so it does not need to properly engage in an agreement protocol independently. Our architecture is flexible and allows us to use our technique for most protocols that are based on random sampling. By studying hierarchical protocols, we discovered new theoretical results of independent interest. Specifically, the ability to handover from a primary protocol requires a new Justifiability property that allows agents to pre-decide on a value, such that if the protocol decides, it must be on that pre-decided value.

Abstract We present a multi-party exchange protocol that achieves optimal partial fairness even in the presence of a dishonest majority. We demonstrate how this protocol can be applied to any type of multi-party exchange scenario where the network topology is complete. When combined with standard secure multi-party computation techniques, our protocol enables SMPC with partial fairness when a dishonest majority is involved. Fairness optimality is proven in an abstract model which applies to all protocols based on the concept of concealing the point when the secrets are exchanged. Our protocol improves known results via the use of timed-release encryption and commutative blinding.

Abstract We propose a new fair exchange protocol that takes advantage of delay encryption and commutative encryption to achieve optimal partial fairness among all protocols involving one-way messages. Our protocol consists of 3 setup messages and $$2N+1$$ 2 N + 1 exchange messages and it is fair against covert adversaries with probability $$1- \frac{1}{2N}$$ 1 - 1 2 N . We prove that this is optimal up to shortening the setup phase which is notably more efficient than existing protocols.

Collaborative development in open-source software (OSS) has long been limited by the lack of participation, i.e., A project is often maintained by an insufficient number of developers, especially for small- and medium-size projects. To establish a sustainable ecosystem for global developers and projects, we propose a decentralised and trustless open-source protocol Committable for all OSS software. The key insight behind Committable is an accountable and trusted tokenisation technology on blockchain that creates the CMT software assets for a variety of artefacts (e.g., document, code, testcase, makefile etc..) across the whole development lifecycle. A CMT token defines an abstraction of commits to OSS and systematically models the contribution from developers, therefore is far more comprehensive than a commit hash that are commonly used to identify software versions. In further, Committable introduces the Problem-Solution-Risk (PSR) framework to evaluate and reward a given set of CMT in an unbiased manner based on their contributions to a project. Owners of CMT are allowed to trade their tokens in the marketplace on blockchain established by Committable. The trading of CMT leads to transfer of token rights (e.g., sell, earn PSR rewards etc.), and more importantly, royalty to the developer for his or her original contribution. This demonstration proposal will introduce Committable on the test net of Ethereum and describe a preliminary case study with the OpenZeppelin project.

Abstract Hoare’s Communicating Sequential Processes (CSP) (Hoare in Communicating Sequential Processes, Prentice-Hall Inc, Upper Saddle River, 1985) admits a rich universe of semantic models closely related to the van Glabbeek spectrum. In this paper we study finite observational models, of which at least six have been studied for CSP, namely traces, stable failures, revivals, acceptances, refusal testing and finite linear observations (Roscoe in Understanding concurrent systems. Texts in computer science, Springer, Berlin, 2010). (Others are known.) We show how to use the relatively recently-introduced priority operator (Roscoe in Understanding concurrent systems. Texts in Computer Science, Springer, Berlin, 2010) to transform refinement questions in these models into trace refinement (language inclusion) tests. Furthermore, we are able to generalise this to any (rational) finite observational model. As well as being of theoretical interest, this is of practical significance since the state-of-the-art refinement checking tool FDR4 (Gibson-Robinson et al. in Int J Softw Tools Technol Transf 18(2):149–167, 2016) currently only supports two such models. In particular we study how it is possible to check refinement in a discrete version of the Timed Failures model that supports Timed CSP.

Abstract This work develops a type of local analysis that can prove concurrent systems deadlock free. As opposed to examining the overall behaviour of a system, local analysis consists of examining the behaviour of small parts of the system to yield a given property. We analyse pairs of interacting components to approximate system reachability and propose a new sound but incomplete/approximate framework that checks deadlock and local-deadlock freedom. By replacing exact reachability by this approximation, it looks for deadlock (or local-deadlock) candidates, namely, blocked (locally-blocked) system states that lie within our approximation. This characterisation improves on the precision of current approximate techniques. In particular, it can tackle non-hereditary deadlock-free systems, namely, deadlock-free systems that have a deadlocking subsystem. These are neglected by most approximate techniques. Furthermore, we demonstrate how SAT checkers can be used to efficiently implement our framework, which, typically, scales better than current techniques for deadlock-freedom analysis. This is demonstrated by a series of practical experiments.

This article investigates how the use of approximations can make the formal verification of concurrent systems scalable. We propose the idea of synchronisation analysis to automatically capture global invariants and approximate reachability. We calculate invariants on how components participate on global system synchronisations and use a notion of consistency between these invariants to establish whether components can effectively communicate to reach some system state. Our synchronisation-analysis techniques try to show either that a system state is unreachable by demonstrating that components cannot agree on the order they participate in system rules or that a system state is unreachable by demonstrating components cannot agree on the number of times they participate on system rules. These fully automatic techniques are applied to check deadlock and local-deadlock freedom in the PairStatic framework. It extends Pair (a recent framework where we use pure pairwise analysis of components and SAT checkers to check deadlock and local-deadlock freedom) with techniques to carry out synchronisation analysis. So, not only can it compute the same local invariants that Pair does, it can leverage global invariants found by synchronisation analysis, thereby improving the reachability approximation and tightening our verifications. We implement PairStatic in our DeadlOx tool using SAT/SMT and demonstrate the improvements they create in checking (local) deadlock freedom.

Modern life is permeated by software which provides a large attack surface, ranging from generic malware attacks that can be classed as mere nuisance to sophistically created and targeted code touted as a next generation of weapons. Although some research on this broad area of cyber weapons exists, the solicitation of public opinion through surveys is lacking. This paper presents the results of a questionnaire concerning the attitudes and understanding of cyber weapons in relation to international security. The results of the study suggest that there is a statistically significant difference between respondents employed in the 'Military', 'Academia', or 'Other' professions concerning questions of capabilities and the demise of the state-centric model.

Abstract We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.

Abstract In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties (particularly deadlock freedom) by construction in component composition. Nevertheless, their application is allowed only under certain conditions whose verification via model checking turned out impracticable even for some simple designs, and particularly those involving cyclic topologies. In this paper, we address the performance of the analysis and present a significantly more efficient alternative to the verification of the rule side conditions, which are improved by carrying out partial verification on component metadata throughout component compositions and by using behavioural patterns. The use of metadata, together with behavioural patterns, demands new composition rules, which allow previous exponential time verifications to be carried out now in linear time. Two case studies (the classical dining philosophers, also used as a running example, and an industrial version of a leadership election algorithm) are presented to illustrate and validate the overall approach.

Abstract A well-established specification of noninterference in CSP is that, when high-level events are appropriately abstracted, the remaining low-level view is deterministic. This is not a workable definition in Timed CSP, where many processes cannot be refined to deterministic ones. We argue that in fact “deterministic” should be replaced by “maximally refined” in the definition above. We show how to automate the resulting timed noninterference check within the context of the recent extension of FDR to analyse a discrete version of Timed CSP, and how an extended theory of digitisation has the potential both to create more accurate specifications and to infer when processes are noninterfering in the more usual continuous-time semantics.

A body sensor network (BSN) is typically a wearable wireless sensor network. Security protection is critical to BSNs, since they collect sensitive personal information. Generally speaking, security protection of BSN relies on identity (ID) and key distribution protocols. Most existing protocols are designed to run in general wireless sensor networks, and are not suitable for BSNs. After carefully examining the characteristics of BSNs, the authors propose human interactive empirical channel‐based security protocols, which include an elliptic curve Diffie–Hellman version of symmetric hash commitment before knowledge protocol and an elliptic curve Diffie–Hellman version of hash commitment before knowledge protocol. Using these protocols, dynamically distributing keys and IDs become possible. As opposite to present solutions, these protocols do not need any pre‐deployment of keys or secrets. Therefore compromised and expired keys or IDs can be easily changed. These protocols exploit human users as temporary trusted third parties. The authors, thus, show that the human interactive channels can help them to design secure BSNs.

One of the main challenges in pervasive computing is how we can establish secure communication over an untrusted high-bandwidth network without any initial knowledge or a Public Key Infrastructure. An approach studied by a number of researchers is building security though human work creating a low-bandwidth empirical (or authentication) channel where the transmitted information is authentic and cannot be faked or modified. In this paper, we give an analytical survey of authentication protocols of this type. We start with non-interactive authentication schemes, and then move on to analyse a number of strategies used to build interactive pair-wise and group protocols that minimise the human work relative to the amount of security obtained as well as optimising the computation processing. In studying these protocols, we will discover that their security is underlined by the idea of commitment before knowledge, which is refined by two protocol design principles introduced in this survey.

The differences between the fields of Human-Computer Interaction and Security (HCISec) and Human-Computer Interaction (HCI) have not been investigated very closely. Many HCI methods and procedures have been adopted by HCISec researchers, however the extent to which these apply to the field of HCISec is arguable given the fine balance between improving the ease of use of a secure system and potentially weakening its security. That is to say that the techniques prevalent in HCI are aimed at improving users' effectiveness, efficiency or satisfaction, but they do not take into account the potential threats and vulnerabilities that they can introduce. To address this problem, we propose a security and usability threat model detailing the different factors that are pertinent to the security and usability of secure systems, together with a process for assessing these.

We analyse and evaluate the usability and security of the process of bootstrapping security among devices in group scenarios. While a lot of work has been done in single user scenarios, we are not aware of any that focusses on group situations. Unlike in single user scenarios, bootstrapping security in a group requires coordination, attention, and cooperation of all group members. In this paper, we provide an analysis of the security and usability of bootstrapping security in group scenarios and present the results of a usability study on these scenarios. We also highlight crucial factors necessary for designing for secure group interactions.

Initiating and bootstrapping secure, yet low-cost, ad-hoc transactions is an important challenge that needs to be overcome if the promise of mobile and pervasive computing is to be fulfilled. For example, mobile payment applications would benefit from the ability to pair devices securely without resorting to conventional mechanisms such as shared secrets, a Public Key Infrastructure (PKI), or trusted third parties. A number of methods have been proposed for doing this based on the use of a secondary out-of-band (OOB) channel that either authenticates information passed over the normal communication channel or otherwise establishes an authenticated shared secret which can be used for subsequent secure communication. A key element of the success of these methods is dependent on the performance and effectiveness of the OOB channel, which usually depends on people performing certain critical tasks correctly.

Abstract Individual components in an inter-operating system require assurance from other components both of appropriate functionality and of suitable responsiveness. We have developed properties which capture the notion of non-blocking responsive behaviour, together with machine-based checks implemented in the CSP model-checker, FDR. In this paper we illustrate the use of our responsiveness properties with a small example, and provide a detailed comparison to related work in CCS. This work has led to the discovery of a new semantic model for CSP with respect to which such properties are fully abstract. We present the new stable revivals model and discuss implications for responsiveness checking.

Abstract We show that wide-ranging classes of predicates on the failures-divergences model for CSP can be represented by refinement checks in a general form. These are predicates of a process P expressible as F ( P )⊏ G ( P ), where F and G are CSP contexts and ⊏ is refinement. We use ideas similar to full abstraction, but achieve a stronger property than that. Our main result is that topologically-closed predicates are precisely those representable when F and G are both uniformly continuous. We show that sub-classes of predicates such as refinement-closed and distributive ones are represented by special forms of this check.

Abstract. This paper investigates the issue of responsiveness of interoperating components: one not causing the other to deadlock. This is obviously related to the question of whether the two deadlock when put in parallel. However, it is different in that we require that a specific process P is not itself blocked by a plugin Q when it could otherwise have progressed, instead of asking that either process can always proceed (deadlock freedom). The issue becomes yet more subtle when dealing with processes which can nondeterministically block, either through graceful termination or unfortunate deadlock. The relational predicate, that is, binary relation on processes, which we provide is refinement-closed. This is significant as it allows components to be developed independently. In addition, it can be mechanically verified. The contribution of this paper is to identify the issue of responsiveness; to define appropriate properties; to demonstrate the suitability of these properties and consider how they can be mechanically verified. The notation used is CSP with automatic model-checking provided by the FDR tool.

We carry forward the work described in our previous papers [5,18,20] on the application of data independence to the model checking of security protocols using CSP [19] and FDR [10]. In particular, we showed how techniques based on data independence [

A system is data-independent with respect to a data type $X$ iff the operations it can perform on values of type $X$ are restricted to just equality testing. The system may also store, input and output values of type $X$ . We study model checking of systems which are data-independent with respect to two distinct type variables $X$ and $Y$ , and may in addition use arrays with indices from $X$ and values from $Y$ . Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty finite instances of $X$ and $Y$ . Initially, we consider instead the abstraction where $X$ and $Y$ are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the $\mu$ -calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of $X$ and $Y$ . We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the $\mu$ -calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the $\mu$ -calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where $X$ is the type of memory addresses, and $Y$ the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.

We carry forward the work described in our previous papers (Broadfoot et al., 2000, Broadfoot and Roscoe, 2002, and Roscoe, 1998) on the application of data independence to the model checking of cryptographic protocols using CSP and FDR. In particular, we showed how techniques based on data independence could be used to justify, by means of a finite FDR check, systems where agents can perform an unbounded number of protocol runs. Whilst this allows for a more complete analysis, there was one significant incompleteness in the results we obtained: While each individual identity could perform an unlimited number of protocol runs sequentially, the degree of parallelism remained bounded. We report significant progress towards the solution of this problem, by "internalising" all or part of each agent identity within the "intruder" process. We consider the case where internal agents do introduce fresh values and address the issue of capturing the state of mind of internal agents (for the purposes of analysis).

The term "intransitive noninterference" refers to the information flow properties required of systems like downgraders, in which it may be legitimate for information to flow indirectly, between two users but not directly. We examine the usual definition of this property in terms of a modified purge function, and show that this is a distinctly weaker property than an alternative we derive from considerations of determinism.

Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols – see, for example, and many of the papers in . Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually res tricted by the finiteness of some set of resources such as keys and nonces, is free of attacks. While for specific protocols there are frequently good reasons for supposing that this will find any attack, it leaves a substantial gap in the method. The purpose of this paper is to show how techniques borrowed from data independence and related fields can be used to achieve the illusion that nodes can call upon an infinite supply of different nonces, keys, etc., even though the actual types used for these things remain finite. It is thus possible to create models of protocols in which nodes do not have to stop after a small number of runs, and to claim that a finite-state run on a model checker has proved that a given protocol is free from attacks which could be constructed in the model used. We develop our methods via a series of case studies, discovering a number of methods for restricting the number of states generated in attempted proofs, and using two distinct approaches to protocol specification.

Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols. Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually restricted by the finiteness of some set of resources such as keys and nonces, is free of attacks. While for specific protocols there are frequently good reasons for supposing that this will find any attack, it leaves a substantial gap in the method. The purpose of this paper is to show how techniques borrowed from data independence and related fields can be used to achieve the illusion, that nodes can call upon an infinite supply of different nonces, keys, etc., even though the actual types used for these things remain finite. It is thus possible to create models of protocols in which nodes do not have to stop after a small number of runs and to claim that, within certain limits, a finite-state run on a model checker has proved that a given protocol is secure from attack. The author uses a single protocol as a case study, but believe our techniques are much more widely applicable.

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.

It is often difficult to specify exactly what a security protocol is intended to achieve, and there are many example of attacks on protocol which have been proved to satisfy the 'wrong', or too unreal a specification. Contrary to the usual approach of attempting to capture what it is that protocol achieves in abstract terms, we propose a readily automatable style of specification which simply asserts that a node can only complete its part in a protocol run if the pattern of messages anticipated by the designer has occurred. While this intensional style of specification does not replace more abstract ones such as confidentiality, it does appear to preclude a wide range of the styles of attack that are hardest to exclude by other means.

The standard approach to the specification of a secure system is to present a (usually state-based) abstract security model separately from the specification of the system's functional requirements, and establishing a correspondence between the two specifications. This complex treatment has resulte d in development methods distinct from those usually advocated for general applications. We provide a novel and intellectually satisfying formulation of security properties in a process algebraic framework, and show that these are preserved under refinement. We relate the results to a more familiar state-based (Z) specification methodology. There are efficient algorithms for verifying our security properties using model checking.

We investigate the formal relationship between separability of processes and the types of non-interference properties they enjoy. Though intuitively appealing, separability-the ability to define a process as a parallel composition of disjoint components-alone cannot adequately prove the absence of information flow. We present a number of laws for the composition of secure systems, and an example to show how such laws can be applied.

We show how a variety of confidentiality properties can be expressed in terms of the abstraction mechanisms that CSP provides. We argue that determinism of the abstracted low-security viewpoint provides the best type of property. By changing the form of abstraction mechanism we are able to model different assumptions about how systems behave, including handling the distinction between input and output actions. A detailed analysis of the nature of nondeterminism shows why certain security properties have had the paradoxical property of not being preserved by refinement-a disadvantage not shared by the determinism-based conditions. Finally we give an efficient algorithm for testing the determinism properties on a model-checker.>

We show how the standard failures/divergences model for CSP can be extended by adding to each process' representation the set of all infinite traces it can perform. This allows a full and compositional treatment of unboundedly non-deterministic constructs such as πS and P/X for infinite S and X. By allowing unbounded non-determinism we lose two of the main properties of semantics we have become used to: completeness of the model and continuity of the language constructs. Thus the existence and analysis of fixed points required for recursion becomes much less straightforward than we are used to. A novel technique is used to demonstrate the existence of the fixed points: an operational semantics is constructed for unboundedly non-deterministic CSP and proved congruent to the denotational one. A corollary to this proof is the existence of the required fixed points. It also demonstrates that the least fixed point remains the natural denotation of a recursion, even though recursions no longer reach their fixed points in ω iterations from ⊥.

The failures-divergences model for CSP is usually presented with the refinement order being the one used for fixed points in the semantics of recursion. The requirement that this order be complete means that the model needs a compactness axiom closely related to an assumption of finite non-determinism. We show that a second and stronger order exists which does not need compactness to make it complete, but which gives exactly the same least fixed points as the refinement order. The new order allows us to prove some new results about the semantics, and to justify versions of recursion induction. In pursuit of this last topic we develop various topologies over the model.

We solve the problem of decomposing a rectangle R into p rectangles of equal area so that the maximum rectangle perimeter is as small as possible. This work has applications in areas such as flexible object packing and data allocation. Our solution requires only a constant number of arithmetic operations and integer square roots to characterize the decomposition, and linear time to print the decomposition. The discrete analogue of the problem in which the rectangle R is replaced by a rectangular array of lattice points is also considered, and three heuristic methods of solution are given. All of the heuristic methods operate by finding a discrete approximation to our optimal decomposition of R, but with different tradeoffs between the accuracy of the approximation and running time.

A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved. The possibilities of nondetermimsm are fully taken into account.