Automated anonymity verification of the ThreeBallot and VAV voting systems

In recent years, a large number of secure voting protocols have been proposed in the literature. Often these protocols contain flaws, but because they are complex protocols, rigorous formal analysis has proven hard to come by. Rivest’s ThreeBallot and Vote/Anti-Vote/Vote (VAV) voting systems are important because they aim to provide security (voter anonymity and voter verifiability) without requiring cryptography. In this paper, we construct CSP models of ThreeBallot and VAV, and use them to produce the first automated formal analysis of their anonymity properties. Along the way, we discover that one of the crucial assumptions under which ThreeBallot and VAV (and many other voting systems) operate—the short ballot assumption—is highly ambiguous in the literature. We give various plausible precise interpretations and discover that in each case, the interpretation either is unrealistically strong or else fails to ensure anonymity. We give a revised version of the short ballot assumption for ThreeBallot and VAV that is realistic but still provides a guarantee of anonymity.     

A semantics for Behavior Trees using CSP with specification commands

In this paper we give a formal definition of the requirements translation language Behavior Trees. This language has been used with success in industry to systematically translate large, complex, and often erroneous requirements documents into a structured model of the system. It contains a mixture of state-based manipulations, synchronisation, message passing, and parallel, conditional, and iterative control structures. The formal semantics of a Behavior Tree is given via a translation to a version of Hoare’s process algebra CSP, extended with state-based constructs such as guards and updates, and a message passing facility similar to that used in publish/subscribe protocols. We first provide the extension of CSP and its operational semantics, which preserves the meaning of the original CSP operators, and then the Behavior Tree notation and its translation into the extended version of CSP.     

Probabilistic and nondeterministic aspects of anonymity

The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending emails. The protocols for ensuring anonymity often use random mechanisms which can be described probabilistically, while the agents’ behavior may be totally unpredictable, irregular, and hence expressible only nondeterministically. Formal definitions of the concept of anonymity have been investigated in the past either in a totally nondeterministic framework, or in a purely probabilistic one. In this paper, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the most general situation in which the protocol and the users can have both probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users. We formulate the notions of anonymity in terms of probabilistic automata, and we describe protocols and users as processes in the probabilistic π-calculus, whose semantics is again based on probabilistic automata. Throughout the paper, we illustrate our ideas by using the example of the dining cryptographers.     

Practical Internet voting system

Recently, Internet voting systems have gained popularity and have been used for government elections and referendums in the United Kingdom, Estonia and Switzerland as well as municipal elections in Canada and party primary elections in the United States and France. Current Internet voting systems assume either the voter's personal computer is trusted or the voter is not physically coerced. In this paper, we present an Internet voting system, in which the voter's choice remains secret even if the voter's personal computer is infected by malware or the voter is physically controlled by the adversary. In order to analyze security of our system, we give a formal definition of coercion-resistance, and provide security proof that our system is coercion-resistant. In particular, our system can achieve absolute verifiability even if all election authorities are corrupt. Based on homomorphic encryption, the overhead for tallying in our system is linear in the number of voters. Thus, our system is practical for elections at a large scale, such as general elections.     

Formalizing provable anonymity in Isabelle/HOL

We formalize in a theorem prover the notion of provable anonymity. Our formalization relies on inductive definitions of message distinguishing ability and observational equivalence on traces observed by the intruder. Our theory differs from its original proposal and essentially boils down to the inductive definition of distinguishing messages with respect to a knowledge set for the intruder. We build our theory in Isabelle/HOL to achieve a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through two case studies of the Crowds and Onion Routing protocols.     

Systems engineering principles for the design of biomedical signal processing systems

Systems engineering aims to produce reliable systems which function according to specification. In this paper we follow a systems engineering approach to design a biomedical signal processing system. We discuss requirements capturing, specification definition, implementation and testing of a classification system. These steps are executed as formal as possible. The requirements, which motivate the system design, are based on diabetes research. The main requirement for the classification system is to be a reliable component of a machine which controls diabetes. Reliability is very important, because uncontrolled diabetes may lead to hyperglycaemia (raised blood sugar) and over a period of time may cause serious damage to many of the body systems, especially the nerves and blood vessels. In a second step, these requirements are refined into a formal CSP‖ B model. The formal model expresses the system functionality in a clear and semantically strong way. Subsequently, the proven system model was translated into an implementation. This implementation was tested with use cases and failure cases.Formal modeling and automated model checking gave us deep insight in the system functionality. This insight enabled us to create a reliable and trustworthy implementation. With extensive tests we established trust in the reliability of the implementation.     

Analysis of privacy in mobile telephony systems

We present a thorough experimental and formal analysis of users’ privacy in mobile telephony systems. In particular, we experimentally analyse the use of pseudonyms and point out weak deployed policies leading to some critical scenarios which make it possible to violate a user’s privacy. We also expose some protocol’s vulnerabilities resulting in breaches of the anonymity and/or user unlinkability. We show these breaches translate in actual attacks which are feasible to implement on real networks and discuss our prototype implementation. In order to countermeasure these attacks, we propose realistic solutions. Finally, we provide the theoretical framework for the automatic verification of the unlinkability and anonymity of the fixed 2G/3G procedures and automatically verify them using the ProVerif tool.     

Stochastic cooperative distributed grammar systems and random graphs

We introduce an alternative definition of random graphs as a language generated by a stochastic cooperating distributed grammar system. We show a relationship between our definition and four known definitions of random graphs, an example of using our model to prove graph-theoretic properties, and we define k-probabilistic model of random graphs as an extension. The first important acquisition of our definition is that only a small modification of a stochastic cooperating distributed grammar system may effect the substantial change of the generated random graph model. Other important result resides in the fact that our approach enables the use of a new proving technique in the random graph theory which is based on the generative paradigm inherent in the formal languages theory. Received: 14 May 2002 / 30 October 2002 RID="*" ID="*" Supported by the VEGA grant No. 1/7152/20.     

An Overview of the Integrated Formalism RT-Z

We present an integration of the formal specification languages Z and timed CSP, called RT-Z, incorporating their combined strengths in a coherent frame. To cope with complex systems, RT-Z is equipped with structuring constructs built on top of the integration, because both Z and timed CSP lack appropriate facilities. The formal semantics of RT-Z, based on the denotational semantics of Z and timed CSP, is a prerequisite for preciseness and mathematical rigour. RT-Z is intended to be used in the requirements definition and design phases of the system and software development process. The envisaged application area is the development of real-time embedded systems. Received September 2000 / Accepted in revised form June 2001     

A Taxonomy of Web Services Using CSP

Terms such as conversational and stateless are widely used in the taxonomy of web services. We give formal definitions of these terms using the CSP process algebra. Within this framework we also define the notion of Service-Oriented Architecture. These definitions are then used to prove important scalability properties of stateless services. The use of formalism should allow recent debates, concerning how and whether web services provide standardized access to state, to progress more rigorously.     

Quantitative Analysis With the Probabilistic Model Checker PRISM

Probabilistic model checking is a formal verification technique for establishing the correctness, performance and reliability of systems which exhibit stochastic behaviour. As in conventional verification, a precise mathematical model of a real-life system is constructed first, and, given formal specifications of one or more properties of this system, an analysis of these properties is performed. The exploration of the system model is exhaustive and involves a combination of graph-theoretic algorithms and numerical methods. In this paper, we give a brief overview of the probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism) implemented at the University of Birmingham. PRISM supports a range of probabilistic models and specification languages based on temporal logic, and has been recently extended with costs and rewards. We describe our experience with using PRISM to analyse a number of case studies from a wide range of application domains. We demonstrate the usefulness of probabilistic model checking techniques in detecting flaws and unusual trends, focusing mainly on the quantitative analysis of a range of best, worst and average-case system characteristics.     

形式化语言RT-Z的合成及其应用

Z是一种确定相关数据特征的非常成功的形式化语言，却在构造动态行为方面的模型缺乏相应的功能；而Timed CSP是一种确定动态行为的功能强大的语言，但它没提供适当的结构来构造相关数据特征。文中通过形式化语言Z和过程代数Timed CSP合成一种新的形式化方法RT-Z，使得RT-Z在软件系统开发过程的需求定义和设计阶段能书写软件系统一致、简单的规格说明。     

Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks

We consider the problem of formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well-studied deduction rules for symmetric and public key encryption, often called Dolev–Yao rules, with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in the presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables that represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.     

Design and Verification of Distributed Recovery Blocks with CSP

A case study on the application of Communicating Sequential Processes (CSP) to the design and verification of fault-tolerant real-time systems is presented. The distributed recovery block (DRB) scheme is a design technique for the uniform treatment of hardware and software faults in real-time systems. Through a simple fault-tolerant real-time system design using the DRB scheme, the case study illustrates a paradigm for specifying fault-tolerant software and demonstrates how the different behavioural aspects of a fault-tolerant real-time system design can be separately and systematically specified, formulated, and verified using an integrated set of formal techniques based on CSP.     

Qualitative and quantitative conditions for the transitivity of perceived causation:

If A caused B and B caused C, did A cause C? Although laypersons commonly perceive causality as being transitive, some philosophers have questioned this assumption, and models of causality in artificial intelligence are often agnostic with respect to transitivity. We consider two formal models of causation that differ in the way they represent uncertainty. The quantitative model uses a crude probabilistic definition, arguably the common core of more sophisticated quantitative definitions; the qualitative model uses a definition based on nonmonotonic consequence relations. Different sufficient conditions for the transitivity of causation are laid bare by the two models: The Markov condition on events for the quantitative model, and a so-called saliency condition (A is perceived as a typical cause of B) for the qualitative model. We explore the formal and empirical relations between these sufficient conditions, and between the underlying definitions of perceived causation. These connections shed light on the range of applicability of each model, contrasting commonsense causal reasoning (supposedly qualitative) and scientific causation (more naturally quantitative). These speculations are supported by a series of three behavioral experiments.     

On stability of formal fuzziness systems

The structure of formal fuzziness systems as some abstraction on real fuzziness systems is debated. Then the global definition of α-stability is given. First some necessary and sufficient conditions for α-stability are given for the case of R = A ? B (Sec. 2) and later for the case of R defined by an implication chain of any finite length (Sec. 4). In Secs. 5 and 6 notions of α-stability and α-β strong decision stability are introduced, and some theorems on necessary or sufficient (or both) conditions for these kinds of stability, imposed on the structure of an implication chain, are proved. In Sec. 3 the good-mapping property of a fuzzy relation matrix is analyzed, and because of its heuristic importance it is assumed in further sections. In many cases examples are given to illustrate definitions and theorems or conclusions.