Search

In this manuscript we propose and implement a dimension reduction algorithm of AND-NOT networks for the purpose of steady state computation. Our method of network reduction consists in using “steady state approximations” that do not change the number of steady states. The algorithm is designed to work at the wiring diagram level without the need to evaluate or simplify Boolean functions. Also, our implementation of the algorithm takes advantage of the sparsity typical of discrete models of biological systems. The main features of our reduction algorithm are that it works at the wiring diagram level and it preserves the number of steady states. Furthermore, the steady states of the original network can be recovered from the steady states of the reduced network; thus, all steady states are found. Also, heuristic analysis and simulations show that it runs in polynomial time. We used our results to study AND-NOT network models of gene networks and showed that our algorithm greatly simplifies steady state analysis. Furthermore, our algorithm can handle sparse AND-NOT networks with up to 1,000,000 nodes. [ABSTRACT FROM AUTHOR]

Radio Block Center (RBC) is a core part of the Chinese Train Control System level 3 (CTCS-3) which is a protocol for safety critical systems. The correctness of the RBC handover protocol is one of the most important factors affecting the safety of systems. Hence, it is of great importance to ensure the correctness of the protocol. To this end, some formal methods have been used to model and verify the protocol. In this paper, we use Modeling, Simulation and Verification Language (MSVL) as the formal language to model and verify the protocol. The result shows that the behavior of RBC handover is consistent with the specification. [ABSTRACT FROM AUTHOR]

Controller Area Network (CAN) is a high-speed serial bus system with real-time capability. In this paper, we present a formal model of the CAN bus protocol, mainly focusing on the arbitration process, transmission process, and fault confinement mechanism. Moreover, 11 important properties are formalized in terms of the protocol. Based on the verification tool UPPAAL, we describe the system model and properties for performing verification work of the CAN bus protocol. The verification results indicate that some properties are not satisfied in CAN bus system, most of which are caused by the starvation and bus-off nodes. On this basis, the dynamic priority scheduling algorithm and bus-off recovery mechanism are applied, which indicates that some problems can be solved on the application layer. [ABSTRACT FROM AUTHOR]

Abstract: This paper presents a rule-based algorithm for performing order-sorted E-unification using an unsorted E-unification decision procedure under assumptions about E that are commonly satisfied in practice. We have implemented this algorithm in Maude for use with the Maude-NRL protocol analyzer and have used CiME for unsorted E-unification for E any set of AC and ACU axioms. In many examples of interest, using order-sorted unification over unsorted unification is able to reduce the total number of unifiers considered, and dramatically improve the performance of the Maude-NRL tool. [Copyright &y& Elsevier]

Abstract: Event-B∥CSP is a combination of Event-B and CSP in which CSP controllers are used in conjunction with Event-B machines to allow a more explicit approach to control flow. Recent results have provided an approach to stepwise refinement of such combinations. This paper presents a simplified Bounded Retransmission Protocol case study, inspired by Abrialʼs treatment of this example, to illustrate several aspects new in the approach. The case study includes refinement steps to illustrate four different aspects of this approach to refinement: (1) splitting events; (2) introducing convergent looping behaviour; (3) the relationship between anticipated, convergent, and devolved events; and (4) converging anticipated events. [Copyright &y& Elsevier]

Abstract: In certified email (CEM) protocols, TTP transparency is an important security requirement which helps to avoid bad publicity as well as protecting individual usersʼ privacy. Recently we have extended the CEM protocol of Cederquist et al. to satisfy TTP transparency. As a continuation, in this paper, we formally verify the security requirement in the exteded protocol. The properties of fairness, effectiveness and timeliness are checked in the model checker Mocha, and TTP transparency is analysed in the toolsets μCRL and CADP. The results confirm that our proposed extension achieves our design goals. [Copyright &y& Elsevier]

Abstract: We propose a decision procedure for analysing security of quantum cryptographic protocols, combining an algebraic logic rewrite system with an operational semantics for quantum distributed computations. We apply our approach to reasoning about security properties of a recently developed quantum secret sharing protocol. [Copyright &y& Elsevier]

Abstract: Channel modeling is crucial for studying the behavior of quantum channels in order to build an efficient error correction scheme in addition to security verification of different protocols. While most current analyses of quantum protocols use a traditional mathematical approach, we employ a simpler probabilistic model checking which is more compatible with classical implementations to investigate the dependency of the security on the quantum channel noise. We also compare a couple of eavesdropping strategies from the security point of view. [Copyright &y& Elsevier]

Abstract: As mobile devices pervade physical space, the familiar authentication patterns are becoming insufficient: besides entity authentication, many applications require, e.g., location authentication. Many interesting protocols have been proposed and implemented to provide such strengthened forms of authentication, but there are very few proofs that such protocols satisfy the required security properties. In some cases, the proofs can be provided in the symbolic model. More often, various physical factors invalidate the perfect cryptography assumption, and the symbolic model does not apply. In such cases, the protocol cannot be secure in an absolute logical sense, but only with a high probability. But while probabilistic reasoning is thus necessary, the analysis in the full computational model may not be warranted, since the protocol security does not depend on any computational assumptions, or on attacker''s computational power, but only on some guessing chances. We refine the Dolev-Yao algebraic method for protocol analysis by a probabilistic model of guessing, needed to analyze protocols that mix weak cryptography with physical properties of nonstandard communication channels. Applying this model, we provide a precise security proof for a proximity authentication protocol, due to Hancke and Kuhn, that uses probabilistic reasoning to achieve its goals. [Copyright &y& Elsevier]

Abstract: Service oriented computing is an accepted architectural style for developing large, distributed software systems. A particular promise of such architectures is service orchestration, i.e. the ability to combine existing services to create more complex functionality, thereby yielding new services. In this paper, we discuss application-level protocol compliance checking of service orchestrations and service protocols using the semantic domain of modal input/output automata (MIOs). Based on a practical example, we motivate and introduce new notions of refinement and compatibility, and prove that they constitute a valid interface theory. With this domain-specific interface theory, we provide a framework for application-level analysis of service orchestrations, thus complementing existing work on compatibility analysis. Our theory is tool-supported through the MIO Workbench, a verification tool for modal input/output automata. [ABSTRACT FROM AUTHOR]

Abstract: In past years, a number of works considered behavioral protocols of components and discussed approaches for automatically checking of compatibality of protocols (protocol conformance) in component-based systems. The approaches are usually model-checking approaches, i.e., a positive answer guarantees protocol conformance for all executions while a negative answer provides example executions that may lead to protocol violations. It turned out that if behavioral abstractions take into account unbounded concurrency and unbounded recursion, the protocol conformance checking problem becomes undecidable. There are two possibilities to overcome this problem: (i) further behavioral abstraction to finite state systems or (ii) a conservative approximation of the protocol conformance checking problem. Both approaches may lead to spurious counterexamples, i.e., due to abstractions or approximations the shown execution can never happen. This work considers the second approach and shows a heuristics that reduces the number of spurious counterexamples by cutting off search branches that definitely do not contain real counterexamples. [Copyright &y& Elsevier]

Abstract: We propose a formal foundation for behaviour protocols of interacting, concurrent components with data states. Formally, behaviour protocols are given by labelled transition systems which specify the order of operation invocations as well as the allowed changes of data states of components in terms of pre- and postconditions. We study the compatibility of protocols and we consider their composition which yields a behaviour protocol for a component assembly. Behaviour protocols are equipped with a model-theoretic semantics which describes the class of all correct component or assembly implementations. Implementation models are again formalised in terms of labelled transition systems and the correctness notion is based on an alternating simulation relation between protocol and implementation which takes into account concrete control and data states. As a major result we show that our approach is compositional, i.e. that locally correct implementation models of compatible protocols compose to a globally correct implementation, thus ensuring independent implementability. [Copyright &y& Elsevier]

Abstract: This paper presents a graphical user interface (GUI) for the Maude-NPA, a crypto protocol analysis tool that takes into account algebraic properties of cryptosystems not supported by other tools, such as cancellation of encryption and decryption, Abelian groups (including exclusive or), and modular exponentiation. Maude-NPA has a theoretical basis in rewriting logic, unification and narrowing, and performs backwards search from a final attack state to determine whether or not it is reachable from an initial state. The GUI animates the Maude-NPA verification process, displaying the complete search tree and allowing users to display graphical representations of final and intermediate nodes of the search tree. One of the most interesting points of this work is that our GUI has been developed using the framework for declarative graphical interaction associated to Maude that includes IOP, IMaude and JLambda. This framework facilitates the interaction and the interoperation between formal reasoning tools (Maude-NPA in our case) and allows Maude to communicate easily with other tools. [Copyright &y& Elsevier]

Abstract: A choreography specifies activities and interactions among a set of services from a global point of view. From this specification, local implementations or peers can be automatically generated. Generation of peers that precisely implement the choreography specification is not always possible: this problem is known as realizability. This paper presents an encoding of the Chor choreography calculus into the FSP process algebra. This encoding allows to: (i) validate and verify Chor specifications using the FSP toolbox (LTSA), (ii) generate peer protocols from its choreography specified in Chor, (iii) test for realizability of the Chor specification, and (iv) generate Java code from FSP for rapid prototyping purposes. Our proposal is supported and completely automated by a prototype tool we have implemented. [Copyright &y& Elsevier]

Abstract: Checking compatibility of services accessed through their behavioural interfaces is a crucial issue in Service Oriented Computing which aims at building new systems from existing software services. In this paper, we consider a model of services which takes value passing and non-observable actions into account. We propose an approach to check in a unified way several compatibility notions between two service protocols using the rewriting logic system Maude. In particular, we illustrate our approach with three widely used compatibility notions, namely opposite behaviours, unspecified receptions and deadlock freeness. These notions as well as several strategies to handle non-observable actions have been formalised and fully implemented into a prototype tool which is able to automatically detect whether two services are compatible, and return a counterexample if they are not. [Copyright &y& Elsevier]

Abstract: We propose a probabilistic framework for the analysis of security protocols. The proposed framework allows one to model and reason about attackers that extend the usual Dolev-Yao adversary with explicit probabilistic statements representing properties of cryptographic primitives and the attacker''s (partial) information about secret messages. The expressive power of these probabilistic statements is illustrated, namely by representing a standard security notion like indistinguishability under chosen plaintext attacks. We present an entropy-based approach to estimate the probability of a successful attack on a protocol given the prescribed knowledge of the attacker. We prove that, for an attacker whose knowledge increases with the security parameter, computing this quantity is NP-hard in the security parameter. However, we are still able to analyze a few meaningful and illustrative examples. Finally, we obtain a result which may be used to prove that a certain amount of probabilistic knowledge (about the properties of the cryptography being used) is not enough for allowing an attacker to correctly uncover a secret with non-negligible probability. [Copyright &y& Elsevier]

Abstract: This work develops a formal framework for specifying, implementing, and analysing quantum communication protocols. We provide tools for developing simple proofs and analysing programs which involve communication, both via quantum channels and exhibiting the LOCC (local operations, classical communication) paradigm. [Copyright &y& Elsevier]

Abstract: At the highest level of formal certification, the current research trend consists in providing evaluators with a formal checkable proof produced by automatic verification tools. The aim is to reduce the certification process to verifying the provided proof using a proof-checker. However, to date, no certified proof-checker has emerged. In addition, checkable proofs do not eliminate the need to validate the formalization of the verification problem. In this paper we consider the point of view of evaluators. We elaborate criteria that must be fulfilled by a formal proof in order to convince skeptical evaluators. Then, we present a methodology based on this notion of convincing proofs that requires simple formalizations to reach the level of confidence of formal certification. The key idea is to build a certified proof-checker – in collaboration with the evaluators – which is finally used to validate the proof provided by developers. We illustrate our approach on the correctness proof of a buffering protocol written in c that manages the data exchanges between concurrent tasks in avionics control systems. [Copyright &y& Elsevier]

Abstract: The need for a formal verification process in System on Chip (SoC) design and Intellectual Property (IP) integration has been recognized and investigated significantly in the past. A major drawback is the lack of a suitable specification language against which definitive and efficient verification of inter-core communication can be performed to prove compliance of an IP block against the protocol specification. Previous research has yielded positive results of verifying systems against the graphical language of Live Sequence Charts (LSCs) but has identified key limitations of the process that arise from the lack of support for important constructs of LSCs such as Kleene stars, subcharts, and hierarchical charts. In this paper we further investigate the use of LSCs as a specification language and show how it can be formally translated to automata suitable for input to a model checker for automatic verification of the system under test. We present the translation for subcharts, Kleene stars, and hierarchical charts that are essential for protocol specification and have not been translated to automata before. Further, we successfully translate the BVCI protocol (point to point communication protocol) specification from LSC to an automaton and present a case study of verifying models using the resulting automaton. [Copyright &y& Elsevier]

Abstract: Recently, the notion of an array-based system has been introduced as an abstraction of infinite state systems (such as mutual exclusion protocols or sorting programs) which allows for model checking of invariant (safety) and recurrence (liveness) properties by Satisfiability Modulo Theories (SMT) techniques. Unfortunately, the use of quantified first-order formulae to describe sets of states makes fix-point checking extremely expensive. In this paper, we show how invariant properties for a sub-class of array-based systems can be model-checked by a backward reachability algorithm where the length of quantifier prefixes is efficiently controlled by suitable heuristics. We also present various refinements of the reachability algorithm that allows it to be easily implemented in a client-server architecture, where a “light-weight” algorithm is the client generating proof obligations for safety and fix-point checks and an SMT solver plays the role of the server discharging the proof obligations. We also report on some encouraging preliminary experiments with a prototype implementation of our approach. [Copyright &y& Elsevier]

Abstract: An important missing link in the construction of secure systems is finding a practical way to establish a correspondence between a software specification and its implementation. We address this problem for the case of crypto-based Java implementations (such as crypto protocols) with an approach using automated theorem provers for first-order logic, by linking the implementation to a specification model. In this paper, we present details on an application of this approach to the open-source Java implementation Jessie of the SSL protocol. We also shortly comment on how these results can be transferred to the standard Java Secure Sockets Extension (JSSE) library that was recently open-sourced by Sun. [Copyright &y& Elsevier]

Abstract: Several symbolic notions of bisimilarity have been defined for the spi calculus and the applied pi calculus. In this paper, we treat a spi calculus with a general constructor-destructor message algebra, and define a symbolic bisimilarity that is both sound and complete with respect to its concrete counterpart. [Copyright &y& Elsevier]

Abstract: The JFLAP package is a free, interactive visualization, and teaching tool for formal languages. JFLAP is based on the principle that a picture of a concept can be easier to understand than a textual representation. With the help of this package, we implement Dana Angluin''s algorithm which is able to learn Deterministic Finite Automata. The use of JFLAP allows users to visualize each step in the process of learning. The protocol used by the algorithm is called exact learning from membership and equivalence queries. This protocol was also introduced by Dana Angluin, who showed that her learning algorithm discovers the unique minimum automaton coherent with the queries in an efficient running time. [Copyright &y& Elsevier]

Abstract: Latency Insensitive Protocols (LIP) and Elastic Circuits (EC) solve the same problem of rendering a design tolerant to additional latencies caused by wires or computational elements. They are performance-limited by a firing semantics that enforces coherency through a lazy evaluation rule: Computation is enabled if all inputs to a block are simultaneously available. Adaptive LIP''s (ALIP) and EC with early evaluation (ECEE) increase the performance by relaxing the evaluation rule: Computation is enabled as soon as the subset of inputs needed at a given time is available. Their difference in terms of implementation and behavior in selected cases justifies the need for the comparative analysis reported in this paper. Results have been obtained through simple examples, a single representative case-study already used in the context of both LIP''s and EC and through extensive simulations over a suite of benchmarks. [Copyright &y& Elsevier]

Abstract: As Globally Asynchronous and Locally Synchronous (GALS) based System-on-chip (SoC) are gaining importance, a special case of GALS when the global clocking is preserved, but the interconnect delays of multiple clock cycles are to be tolerated has also been proposed, and used. In some cases, such designs, known as Latency-Insensitive Protocol (LIP) based SoC integration are also general enough to work when the global clocking is not present. In either case, the protocols are complex, and many optimized implementations of such protocols need verification that indeed they work correctly with respect to the specification of the system. Usually the specification of the system is fully globally clocked with negligible interconnect delays, so that the specification can be first implemented as synchronous design with traditional tools. GALS or LIP refinements are then applied to tolerate the multi-cycle interconnect delays, or fully asynchronous interconnect communication, as the case may be. Verifying that such refinements are correctness preserving, researchers have used model checking in the past. In this paper, we present static analysis based framework for such verification. Our framework makes use of the Polychrony framework and associated semantic analysis techniques, in the form of endo-isochrony. We show a number of LIP protocols to preserve the correctness with respect to their fully synchronous specifications using our framework. We believe, designers can verify LIP implementations with clever optimizations using our framework much more readily than when using model checking. [Copyright &y& Elsevier]

Abstract: In the context of Dolev-Yao style analysis of security protocols, we investigate the security claims of a recently proposed RFID authentication protocol. We exhibit a flaw which has gone unnoticed in RFID protocol literature and present the resulting attacks on authentication, untraceability, and desynchronization resistance. We analyze and discuss the authors'' proofs of security. References to other vulnerable protocols are given. [Copyright &y& Elsevier]

Abstract: We propose a Petri net model of handshake protocols. These are asynchronous communication protocols which enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. We introduce the notion of handshake Petri net, a Petri net with a specific external interface. We show that the set of observable quiescent traces generated by such a net captures the properties defining a handshake protocol. Conversely we show that for any handshake protocol we can construct a corresponding net. We also study different subclasses of the model. Many examples are provided. [Copyright &y& Elsevier]

Abstract: We introduce a novel process calculus called DBSPI (distributed broadcast SPI-calculus) which models mobile ad hoc networks (MANET). The calculus is a cryptographic broadcast calculus with locations and migration. Communication and migration are limited to neighborhoods. Neighborhood definitions are explicitly part of the syntax allowing dynamic extension using bound identifiers. In this semantic setting we study authentication of agents in MANET protocols. A safety property dealing with authentication correspondence assertions is defined. Later a dependent type and effect system is given and it is shown to be sound, i.e. protocols which are typeable are also safe. This result is lifted to open systems which involves Dolev-Yao attackers. Our Dolev-Yao attacker may use public keys for encryption and can attack any neighborhood it wishes. Our technique is applied to the Mobile IP registration protocol – a type check shows it is safe. To our knowledge this is the first type system for a MANET calculus doing that. [Copyright &y& Elsevier]

Abstract: It is difficult to construct correct models for distributed large-scale service-oriented applications. Typically, the behavior of such an application emerges from the interaction and collaboration of multiple components/services. On the other hand, each component, in general, takes part in multiple scenarios. Consequently, not only components, but also their interaction protocols are important in the development process for distributed systems. Coordination models and languages, like Reo, offer powerful “glue-code” that encode the interaction protocols. In this paper we propose a novel synthesis technique, which can be used to generate Reo circuits directly from scenario specifications. Inspired by the way UML2.0 sequence diagrams can be algebraically composed, we define an algebraic framework for merging connectors generated from partial specifications by exploiting the algebraic structure of UML sequence diagrams. [Copyright &y& Elsevier]

Abstract: Communication protocols are often investigated using simulation. This paper presents a performance study of the distributed coordination function of 802.11 networks. Firstly, our study illustrates the different classes of Petri Nets used for modeling network protocols and their robustness in modeling based on formal methods. Next we propose a detailed 802.11b model based on Object-oriented Petri Nets that precises backoff procedure and time synchronization. Then, performance analyses are evaluated by simulation for a dense wireless network and compared with other measurements approaches. Our main goal is to propose a modular model that will enable to evaluate the impact of network performances on the performances of distributed discrete event systems. [Copyright &y& Elsevier]

Abstract: Formal modeling techniques can be used for analysis of wireless sensor networks (WSNs). Coloured Petri nets (CPNs) that is an extension of Petri nets is a powerful modeling technique. In this paper, we present a CPN model for modeling and performance evaluation of a medium access control protocol in WSNs named sensor-medium access control protocol (S-MAC). S-MAC is an energy-aware MAC protocol with nodes scheduling. The proposed model for this protocol uses the hierarchical modeling capability of CPNs. By using CPNs in this case study and the proposed method for modeling packet broadcast, we have demonstrated the possibility of modeling and evaluation of any other MAC protocol in WSNs or mobile ad-hoc networks (MANET). [Copyright &y& Elsevier]

Abstract: The strand space model is one of the most successful and widely used formalisms for analysing security protocols. This might seem surprising given that the model is not able to reflect choice points in a protocol execution: the key concept in the strand space model is that of a bundle, which models exactly one possible execution of a security protocol. Inspired by the branching processes of Petri nets, we show that branching can be introduced into the strand space model in a very natural way: bundles can be generalized to branching bundles, which are able to capture several conflicting protocol executions. Our investigations of the theory of branching bundles will motivate the concept of symbolic branching bundles, and culminate in the result that every protocol has a strand space semantics in terms of a largest symbolic branching bundle. We hope our results provide a strong theoretical basis for comparing models and providing process calculi semantics in security protocol analysis. Altogether our work is related but different to a series of works by Crazzolara and Winskel. Throughout we will profit from a close relationship of the strand space model to event structures, which has already been pointed out by these authors. [Copyright &y& Elsevier]

Abstract: We introduce weak binders, a lightweight construct to deal with fresh names in nominal calculi. Weak binders do not define the scope of names as precisely as the standard ν-binders, yet they enjoy strong semantic properties. We provide them with a denotational semantics, an equational theory, and a trace inclusion preorder. Furthermore, we present a trace-preserving mapping between weak binders and ν-binders. [Copyright &y& Elsevier]

Abstract: Choreography has recently emerged as a pragmatic and concise way of describing communication-based systems such as web services and financial protocols. Recent studies have investigated the transition from the design stage of a system to its implementation providing an automatic way of mapping a choreograhy into executable code. In this work, we focus on an extension of choreography with a communication-based (interactional) exception mechanism by giving its formal semantics. In particular, we discuss through some examples how interactional exceptions at choreography level can be implemented into end-point code. [Copyright &y& Elsevier]

Abstract: We describe the formal specification and verification of a new fault-tolerant real-time communication protocol, called DoRiS, which is designed for supporting distributed real-time systems that use a shared high-bandwidth medium. Since such a kind of protocol is reasonably complex and requires high levels of confidence on both timing and safety properties, formal methods are useful. Indeed, the design of DoRiS was strongly based on formal methods, where the TLA+ language and its associated model-checker TLC were the supporting design tool. The protocol conception was improved by using information provided by its formal specification and verification. In the end, a precise and highly reliable protocol description is provided. [Copyright &y& Elsevier]

Abstract: The verification of final termination for counter systems is undecidable. For non flattable counter systems, the verification of this type of property is generally based on the exhibition of a ranking function. Proving the existence of a ranking function for general counter systems is also undecidable. We provide a framework in which the verification whether a given function is a ranking function is decidable. This framework is applicable to convex counter systems which admit a Presburger or a LPDS ranking function. This extends the results of [A. Bradley, Z. Manna, and B. Sipma. Termination analysis of integer linear loops. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, volume 3653 of Lecture Notes in Computer Science, pages 488–502. Springer, 2005]. From this framework, we derive a model-checking algorithm to verify whether a final termination property is satisfied or not. This approach has been successfully applied to the verification of a parametric version of the ZCSP protocol. [Copyright &y& Elsevier]

Abstract: This paper extends a rewriting approximations-based theoretical framework in which the security problem – secrecy preservation against an active intruder – may be semi-decided through a reachability analysis. In a recent paper, we have shown how to semi-decide whether a security protocol using algebraic properties of cryptographic primitives is safe. In this paper, we investigate the dual - insecurity - problem: we explain how to semi-decide whether a protocol using cryptographic primitive algebraic properties is unsafe. This improvement offers us to draw automatically a complete diagnostic of a security protocol with an unbounded number of sessions. Furthermore, our approach is supported by the tool TA4SP successfully applied for analysing the NSPK-xor protocol and the Diffie-Hellman protocol. [Copyright &y& Elsevier]

Abstract: An on-the-fly symmetry reduction technique that exploits the lexicographic order on metarepresentations of Maude terms, and a technique that uses auxiliary data to verify strong properties that are not directly expressible in propositional temporal logic are presented. Both are implemented by simple transformations of rewrite theories. They are applied in the verification of a strong-consistency property of a client-server protocol, a simplification of the Chain-Replication protocol. [Copyright &y& Elsevier]

Abstract: Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union with B a set of axioms for which a finitary unification algorithm exists, and Δ a set of confluent, terminating, and B-coherent rewrite rules. However, when , effective narrowing strategies such as basic narrowing easily fail to be complete and cannot be used. This poses two challenges to narrowing-based equational unification: (i) finding effective narrowing strategies that are complete modulo B under mild assumptions on B, and (ii) finding sufficient conditions under which such narrowing strategies yield finitary E-unification algorithms. Inspired by Comon and Delaune''s notion of E-variant for a term, we propose a new narrowing strategy called variant narrowing that has a search space potentially much smaller than full narrowing, is complete, and yields a finitary E-unification algorithm when E has the finite variant property. We also discuss applications to symbolic reachability analysis of concurrent systems specified as rewrite theories, and in particular to the formal analysis of cryptographic protocols modulo the algebraic properties of the underlying cryptographic functions. [Copyright &y& Elsevier]

Abstract: The constraint solver is a symbolic cryptographic protocol security analysis tool that is based on a unique term rewriting approach. Several of the design characteristics of this tool, and the reasons for them, are discussed and placed in perspective with other approaches. The constraint solver uses a free message algebra and a bounded-process network model with a Dolev-Yao attacker. These choices yield simplicity and decidability. [Copyright &y& Elsevier]

Abstract: Protocol composition logic, PCL, is a formal approach for proving security properties of a class of network protocols. PCL involves reasoning directly about properties achieved by protocols steps, in a setting that does not require explicit reasoning about attacker actions. The method relies on protocol invariants to combine properties of different roles of a protocol. While some protocol invariants can be complex to identify and prove, many useful PCL invariants are relatively straightforward consequences of the programs (roles) executed by the agents involved in the protocol. We present a logic program based approach for automating proofs of invariants that appears effective for invariants that are required for several standardized, widely deployed protocols. We use the well-known Transport Layer Security Protocol (TLS/SSL) to illustrate the approach. [Copyright &y& Elsevier]

Abstract: The Adaptive Selective Verification (ASV) protocol was recently proposed as an effective and efficient DoS countermeasure within the shared channel model, in which clients and attackers probabilistically share communication bandwidth with the server. ASV has been manually shown to satisfy some desirable availability and bandwidth consumption properties. Due to the probabilistic nature of the protocol and its underlying attacker model, it is intrinsically difficult to build a faithful model of the protocol with which one may automatically verify its properties. This paper fills the gap between manual analysis and simulation-based experimental analysis of ASV, through automated formal analysis. We describe a formal model of ASV using probabilistic rewrite theories, implemented in a probabilistic extension of Maude, and show how it can be used to formally verify various characteristics of ASV through automated statistical quantitative model checking analysis techniques. In particular, we formally verify ASV''s connection confidence theorem and a slightly more general bandwidth consumption theorem of ASV. This is followed by a statistical comparison of ASV with non-adaptive selective verification protocols. We conclude with remarks on possible further development and future work. [Copyright &y& Elsevier]

Abstract: The PGIP protocol is a standard, abstract interface protocol to connect theorem provers with user interfaces. Interaction in PGIP is based on ASCII-text input and a single focus point-of-control, which indicates a linear position in the input that has been checked thus far. This fits many interactive theorem provers whose interaction model stems from command-line interpreters. PlatΩ, on the other hand, is a system with a new protocol tailored to transparently integrate theorem provers into text editors like ▪ that support semi-structured XML input files and multiple foci of attention. In this paper we extend the PGIP protocol and middleware broker to support the functionalities provided by PlatΩ and beyond. More specifically, we extend PGIP (i) to support multiple foci in provers; (ii) to display semi-structured documents; (iii) to combine prover updates with user edits; (iv) to support context-sensitive service menus, and (v) to allow multiple displays. As well as supporting ▪, the extended PGIP protocol in principle can support other editors such as OpenOffice, Word 2007 and graph viewers; we hope it will also provide guidance for extending provers to handle multiple foci. [Copyright &y& Elsevier]

Abstract: We describe a parallel algorithm for solving parity games, with applications in, e.g., modal μ-calculus model checking with arbitrary alternations, and (branching) bisimulation checking. The algorithm is based on Jurdzinski''s Small Progress Measures. Actually, this is a class of algorithms, depending on a selection heuristics. Our algorithm operates lock-free, and mostly wait-free (except for infrequent termination detection), and thus allows maximum parallelism. Additionally, we conserve memory by avoiding storage of predecessor edges for the parity graph through strictly forward-looking heuristics. We evaluate our multi-core implementation''s behaviour on parity games obtained from μ-calculus model checking problems for a set of communication protocols, randomly generated problem instances, and parametric problem instances from the literature. [Copyright &y& Elsevier]

Abstract: Fault-based conformance testing is a conformance testing strategy that relies on specific fault models. Previously, this mutation testing technique has been applied to protocol specifications. Although a practical case study of web-server testing has been conducted, we observed several issues when applying this method in a large industrial project. In this paper, we discuss the foundations, techniques and tools to overcome these shortcomings. More specifically, we show a solution to the problem of state-space explosion in generating mutation tests for industrial scale applications. Furthermore, the previous approach used the counterexamples of a bisimulation check (between the original and the mutant) as test purposes. With respect to input-output conformance (ioco), this is an over-approximation resulting in more tests than are necessary. Hence, we propose to use an ioco-checker in order to generate less test cases. An industrial case study demonstrates these improvements. [Copyright &y& Elsevier]

Abstract: System-on-chip verification is an active research area. Of particular interest is protocol conversion, where two components with different protocols are controlled to communicate accurately. We present an approach to protocol conversion using model checking. The temporal logic ACTL is used to describe desired behaviour and finite state machines are used for protocol description. We use tableau-based converter construction and prove that a converter exists only when a successful tableau can be constructed. Liveness is incorporated so that converters satisfy additional constraints on protocol communication. A NuSMV-based implementation has been created and we present results on various problems including a large NuSMV example. [Copyright &y& Elsevier]

Abstract: Efficient authenticated group key establishment is the pre-requirement for having group-wide encrypted communications in wireless ad hoc networks. Clustering has brought scalability to ad hoc networks in many ways, now we look at its benefits to group key agreement. In this paper, several solutions for authenticated key establishment in clustered ad hoc networks are surveyed and a new efficient solution for clustered group key establishment is presented. It is based on the AT-GDH and the Burmester-Desmedt broadcast group key protocols. [Copyright &y& Elsevier]

Abstract: To provide formal foundations to current (web) services technologies, we put forward using COWS, a process calculus for specifying, combining and analysing services, as a uniform formalism for modelling all the relevant phases of the life cycle of service-oriented applications, such as publication, discovery, negotiation, deployment and execution. In this paper, we show that constraints and operations on them can be smoothly incorporated in COWS, and propose a disciplined way to model multisets of constraints and to manipulate them through appropriate interaction protocols. Therefore, we demonstrate that also QoS requirement specifications and SLA achievements, and the phases of dynamic service discovery and negotiation can be comfortably modelled in COWS. We illustrate our approach through a scenario for a service-based web hosting provider. [Copyright &y& Elsevier]

Abstract: Control flow is often key problem in current web applications. For example, using the back button gives a POSTDATA error, using multiple windows books the wrong hotel, and sending a link to a friend does not work. Previous solutions used continuations as a model for user interaction. However continuations are insufficient as a model of all web interactions. We believe the protocol and browsers themselves are insufficiently powerful to represent the control flow desired in a web application. Our solution is to extend the protocol and browser sufficiently that these problems can be avoided. We seek to be agnostic about how web applications are written and instead recognise that many of the problems stem from underlying weaknesses in the protocol. As an example, the application ought to be able to inform the browser that pressing back on a payment confirmation page is not allowed. Instead, the cached page can be displayed in a read-only, archive fashion to the user, or a new page can be shown instead which is consistent with the global state. We discuss how some of these ideas may be implemented within the existing HTTP/1.1 protocol; and what modest extensions to the protocol would enable full implementation. We also discuss the interaction with Web 2.0 and the security and privacy implications of our extensions. [Copyright &y& Elsevier]

Abstract: Client-to-client password authenticated key exchange (C2C-PAKE) protocol enables two clients who only share their passwords with their own servers to establish a shared key for their secure communications. Recently, Byun et al. and Yin-Li respectively proposed first provably secure C2C-PAKE protocols. However, both protocols are found to be vulnerable to undetectable online dictionary attacks and other attacks. In this paper, we present an efficient generic construction for cross-realm C2C-PAKE protocols and prove its security in the Random-or-Real model due to Abdalla et al., without making use of the Random Oracle model. [Copyright &y& Elsevier]