Folding Narrowing is a symbolic analysis technique used in various areas of computer science. Maude-NPA has already demonstrated the effectiveness and potential of this technique in protocol analysis, particularly in the cryptographic domain. However, a thorough investigation into how protocols should be specified to make folding narrowing effective has not yet been conducted. The key to enabling this technique lies in ensuring the finiteness of the search space, which requires the search graph to collapse onto itself. Achieving this demands a careful design of the sorts and rules of the specified system. In many cases, such a design even allows for proving properties without relying on lemmas that other techniques typically require. In this work, we show how to prove the mutex property for the Test-and-Set (TAS), Qlock, and Anderson protocols, providing a detailed explanation of the reasoning needed to ensure the folding of the search space—without the use of lemmas.

The BB84 protocol is the first quantum key distribution (QKD) protocol, allowing two parties (typically referred to as Alice and Bob) to securely share a cryptographic key by leveraging the principles of quantum mechanics.Given its importance in cryptography, simulating the protocol is essential for understanding its behavior, while formally verifying that it enjoys certain desired properties is equally crucial.This paper presents a formal specification of the BB84 protocol in Maude, a specification and programming language based on rewriting logic.The formal specification is executable in Maude with several formal analysis methods for simulation and analysis.We use the built-in Maude LTL model checker to analyze some qualitative properties of the protocol.Our analysis confirms that (1) if Alice and Bob choose the same basis and there is no eavesdropper, their bits will match; and (2) if Alice and Bob choose the same basis but do not share the same bit, the presence of an eavesdropper will be detected.

The Post-quantum OpenPGP (PQ OpenPGP) protocol extends OpenPGP with hybrid cryptography, combining classical and post-quantum algorithms.It aims to ensure longterm security against attacks by quantum-capable adversaries.This paper presents a formal specification and verification of the PQ OpenPGP protocol using the algebraic specification language CafeOBJ.Our specification captures key aspects of the protocol, including hybrid key encapsulation using post-quantum ML-KEM and classical ECDH-KEM, dual digital signatures from post-quantum ML-DSA and classical EdDSA, and a quantumcapable Dolev-Yao attacker model.We then focus on verifying the secrecy of the session key property under this attacker model.To facilitate the verification process, we employ the IPSG tool, which automatically generates formal proofs for desired properties based on a formal specification and auxiliary lemmas.

Digital signatures ensure the authenticity and integrity of digital assets , vital properties for any secure communication. The National Institute of Standards and Technologies launched the Post-Quantum Cryptography project to standardise new algorithms and protocols that are secure against quantum attackers. The post-quantum signature scheme FALCON was one of the finalists. We present a continuation of the first steps towards the formal specification and analysis, in the high-performance language Maude, of signature schemes. We have adapted and improved a previous framework, originally aimed to formally specify and analyse post-quantum key encapsulation mechanisms. As a use case of the new framework, we specify an executable symbolic model of FALCON. On the symbolic model, we verify termination and fairness using LTL formulas with Maude's model checker . Furthermore, authentication , integrity and non-repudiation are analysed through invariant analysis. Integrity and non-repudiation hold, meanwhile, authentication does not hold in our symbolic model.

Maude-NPA is a formal verification tool for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic primitives. It starts from an attack state to find counterexamples or conclude that the attack concerned cannot be conducted by performing a backward narrowing reachability analysis. Although Maude-NPA is a powerful analyzer, its running performance can be improved by taking advantage of parallel and/or distributed computing when dealing with complex protocols whose state space is huge. This paper describes a parallel version of Maude-NPA in which the backward narrowing and the transition subsumption at each layer in Maude-NPA are conducted in parallel. A tool supporting the parallel version has been implemented in Maude with a master-worker model using meta-interpreters. We report on some experiments of various kinds of protocols that demonstrate that the tool can increase the running performance of Maude-NPA by 52% on average for complex case studies in which the number of states located at each layer is considerably large.

While constructing practical quantum computers by big companies remains a challenge, the application of quantum communication and cryptography has made remarkable progress. Therefore, it is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. We have proposed Basic Dynamic Quantum Logic (BDQL) to formalize and verify sequential models of quantum protocols with a support tool developed in Maude. However, BDQL does not support concurrency in its formalization. This article introduces Concurrent Dynamic Quantum Logic (CDQL), an extension of BDQL, to formalize and verify concurrent models of quantum protocols. CDQL is more expressive than BDQL by considering concurrent behavior and communication among participants in quantum protocols. Since CDQL is a conservative extension of BDQL, we extend the syntax of BDQL to CDQL and make a transformation from CDQL to BDQL without interrupting the semantics of BDQL. We also extend the implementation of BDQL to support CDQL, making a new support tool in Maude. The new support tool is equipped with a lazy rewriting strategy to make the verification process significantly faster. Several quantum communication protocols are successfully formalized and verified in BDQL/CDQL, demonstrating the effectiveness of our automated approach and tool in verifying quantum protocols.

Abstract State Machine Graphical Animation (called SMGA) is a visualization tool that assists formal methods experts in conjecturing characteristics of a protocol/system. The characteristics guessed by using the tool can be used as lemma candidates to theorem prove that the protocol/system satisfies its desired properties. Because previous work has shown that interaction in SMGA is one promising factor to foster assistance, in this paper, we revise SMGA equipping it with various interactive features in order to help human users in conjecturing lemmas. Moreover, we integrate SMGA and Maude, a declarative language and high-performance tool, so that the revised version of SMGA (called r-SMGA) can use some powerful features of Maude, such as parsing associative-commutative binary operators as well as context-free grammars, reachability analysis, and model checking. We conduct a case study with the Suzuki-Kasami protocol to demonstrate the usefulness of these new features. In the case study, some characteristics are conjectured and confirmed with these features. Based on the guessed characteristics and assistance of r-SMGA, we successfully prove that the protocol enjoys the mutual exclusion property. Finally, we propose guidelines that can help users to conjecture characteristics using r-SMGA. Our result shows that the graphical animation approach is useful for lemma conjecture in theorem proving. The formal verification is a part of the case study.

This paper presents a symbolic approach to model checking quantum circuits by using a set of laws from quantum mechanics and basic matrix operations with Dirac notation.We use Maude, a high-level specification/programming language based on rewriting logic, to implement our symbolic approach.As a case study, we use the approach to formally specify and verify the correctness of the quantum teleportation protocol, which is an important quantum communication protocol in the early work of quantum communications.Moreover, our implementation can be used as a general framework to formally specify and verify quantum circuits in Maude in an effortless way, where only an initial quantum state and a sequence of actions describing how a quantum circuit works in a simple way are required.

Facing the potential threat raised by quantum computing, a great deal of research from many groups and industrial giants has gone into building public‐key post‐quantum cryptographic primitives that are resistant to the quantum attackers. Among them, there is a large number of post‐quantum key encapsulation mechanisms (KEMs), whose purpose is to provide a secure key exchange, which is a very crucial component in public‐key cryptography. This paper presents a formal security analysis of three lattice‐based KEMs including Kyber, Saber, and SK‐MLWR. We use Maude, a specification language supporting equational and rewriting logic and a high‐performance tool equipped with many advanced features, such as a reachability analyzer that can be used as a model checker for invariant properties, to model the three KEMs as state machines. Because they all belong to the class of lattice‐based KEMs, they share many common parts in their designs, such as polynomials, vectors, and message exchange patterns. We first model these common parts and combine them into a specification, called base specification. After that, for each of the three KEMs, by extending the base specification, we just need to model some additional parts and the mechanism execution. Once completing the three specifications, we conduct invariant model checkings with the Maude search command, pointing out a similar man‐in‐the‐middle attack. The occurrence of this attack is due to the fact that authentication is not part of the KEMs, and therefore an active attacker can modify all communication between two honest parties.

We devised the L +1-layer divide & conquer approach to leads-to model checking ( L +1-DCA2L2MC) and its parallel version, and developed sequential and parallel tools for L +1-DCA2L2MC. In a temporal logic called UNITY , designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to these properties. Counterexample generation is one of the main tasks in the L +1-DCA2L2MC technique that can be optimized to improve its running performance. This article proposes a technique to find all counterexamples at once in model checking with a new model checker. Furthermore, layer configuration selection is essential to make the best use of the L +1-DCA2L2MC technique. This work also proposes an approach to finding a good layer configuration for the technique with an analysis tool. Some experiments are conducted to demonstrate the power and usefulness of the two optimization techniques, respectively. Moreover, our sequential and parallel tools are compared with SPIN and LTSmin model checkers, showing a promising way to mitigate the state space explosion and improve the running performance of model checking when dealing with large state spaces.

Many previous case studies on formal verification of invariant properties by writing proof scores have demonstrated that the approach is powerful and flexible. Writing proof scores by hand, however, is prone to human errors and time-consuming, especially with complicated systems or specifications. Therefore, we propose an approach and implement a tool (called Invariant Proof Sore Generator or IPSG) that can automatically generate proof scores for formal invariant property verification. We demonstrate the practicability of the tool with three mutual exclusion protocols and one authentication protocol. The experiments show that IPSG can completely generate proof scores to prove that those protocols enjoy some desired properties.

The paper describes a technique to mitigate the notorious state space explosion in model checking.The technique is called a divide & conquer approach to until and until stable model checking.As indicated by the name, the technique is dedicated to until and until stable properties that are expressed as φ1 U φ2 and φ1 U □φ2, respectively, where φ1, φ2 are state propositions.For real-time system analysis, some interesting systems requirements are expressed as until and until stable properties.For example, a clock is running and shows a correct time until a certain time has passed or until the clock stops due to an empty battery or other failures.Therefore, it is worth focusing on the properties.For each property, we prove a theorem that the proposed technique is correct and design an algorithm based on the theorem to support the technique.Index Terms-until properties,

The security of most public-key cryptosystems currently in use today is threatened by advances in quantum computing.That is the reason why recently many researchers and industrial companies have spent lots of effort on constructing post-quantum cryptosystems, which are resistant to quantum attackers.A large number of post-quantum key encapsulation mechanisms (KEMs) have been proposed to provide secure key establishment -one of the most important building blocks in asymmetric cryptography.This paper presents a formal security analysis of Saber lattice-based KEM.We first formally specify the mechanism in Maude, a rewriting logic-based specification/programming language equipped with many functionalities, such as a reachability analyzer (or the search command) that can be used as an invariant model checker, and then conduct invariant model checking with the Maude search command, finding an attack.

Abstract This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm.

Abstract The paper proposes a new technique to mitigate the state explosion in model checking. The technique is called a divide & conquer approach to leads-to model checking. As indicated by the name, the technique is dedicated to leads-to properties. It is known that many important systems requirements can be expressed as leads-to properties, thus it is worth focusing on leads-to properties. The technique divides an original leads-to model checking problem into multiple smaller model checking problems and tackles each smaller one. We prove a theorem that the multiple smaller model checking problems are equivalent to the original leads-to model checking problem. We conduct two case studies demonstrating the power of the proposed technique.

Our previous work has proposed an approach and a tool supporting it, called Invariant Proof Score Generator (IPSG), that can automatically generate formal proofs, called proof scores, for formal verification of invariant properties. In this work, we present some improvements of the tool that are helpful when conducting formal verification in practice. We demonstrate the practicability of the tool with the TLS 1.2 Handshake Protocol, which is one of the most important cryptographic protocols in use today, securing numerous internet communications. We formally verify that the protocol enjoys two properties including the secrecy property and the authentication property by employing IPSG to infer proof scores. TLS is much more complex than academic protocols, and hence, through the case study, the practicability of the tool is confirmed. Moreover, the correctness of the generated proof scores is once more verified with the use of two extensions of CafeInMaude - a CafeOBJ interpreter implemented in Maude, ensuring that there is not any subtle error in the proof scores generated by our tool. In addition to the case studies reported in our previous work as well as the TLS case study presented in this paper, we also report experimental results of the tool with several other protocols.

CafeOBJ is a language for specifying and verifying a wide variety of software and/or hardware systems. Traditionally, verification has been carried out via proof scores, which consist of reducing goal-related terms in user-defined modules. Although proof scores are semi-formal (the specifier is partially responsible for soundness), their flexibility makes them a useful approach to verification. For the last years, we have developed different formal tools around the CafeInMaude interpreter, a CafeOBJ interpreter implemented in Maude. Besides supporting proof scores, we implemented a theorem prover, a proof script generator from proof scores, and the first stages of a proof script generator and fixer-upper. In this paper, we present (i) an improved and detailed version of our proof script generator and fixer-upper and (ii) a reimplementation of the CafeInMaude interpreter, which supports, among others, parallel execution, an improved tool integration, and an interactive user interface. The benchmarks used to evaluate the tools confirm the usefulness of the approach.

Abstract The mutual exclusion protocol invented by Mellor-Crummey and Scott (called MCS protocol) is used to exemplify that state picture designs based on which the state machine graphical animation (SMGA) tool produces graphical animations should be better visualized. Variants of MCS protocol have been used in Java virtual machines and therefore the 2006 Edsger W. Dijkstra Prize in Distributed Computing went to their paper on MCS protocol. The new state picture design of a state machine formalizing MCS protocol is assessed based on Gestalt principles, more specifically proximity principle and similarity principle. We report on a core part of a formal verification case study in which the new state picture design and the SMGA tool largely contributed to the successful completion of the formal proof that MCS protocol enjoys the mutual exclusion property. The lessons learned acquired through our experiments are summarized as two groups of tips. The first group is some new tips on how to make state picture designs. The second one is some tips on how to conjecture state machine characteristics by using the SMGA tool. We also report on one more case study in which the state picture design has been made for the mutual exclusion protocol invented by Anderson (called Anderson protocol) and some characteristics of the protocol have been discovered based on the tips.

The paper describes a support tool for a technique that alleviates the notorious state space explosion problem in model checking. The technique is called the L + 1-layer divide & conquer approach to leads-to model checking. As indicated by the name, the technique is dedicated to leads- to properties. In a temporal logic called UNITY designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to the properties. The paper also reports on some experiments that demonstrate that the tool can alleviate the state space explosion problem to some extent.

The second and third authors of the present paper have formally verified that A-Anderson protocol, which is an abstract version of Anderson mutual exclusion protocol, enjoys the mutual exclusion property in their previous work.The reason why they did not conduct formal verification with the original version of Anderson but with A-Anderson instead is that Anderson uses a finite boolean array and the modulo (or remainder) operation of natural numbers, causing the challenge to conduct formal verification in a sense of theorem proving.Since then, we have successfully completed formal verification with Anderson to which an auxiliary variable is introduced.The protocol is specified in CafeOBJ, an algebraic specification language, and it is formally verified that the protocol enjoys the property with CafeOBJ.The auxiliary variable does not change the behavior of Anderson.We then conclude that Anderson enjoys the mutual exclusion property by proving that the property is an invariant of the specification.We also informally discuss why it is necessary to introduce auxiliary variables so that we can successfully complete formal verification with some protocols or systems.

Proof scores are programs written in an algebraic specification language, such as CafeOBJ, to conduct formal verification.Thus, the proof score approach to formal verification (PSA2FV) can be regarded as a kind of proving by programming and then flexible.PSA2FV, however, is subject to human errors.To address the issue, a proof assistant called CiMPA was developed for CafeInMaude, the world's second implementation of CafeOBJ.Furthermore, a proof generator called CiMPG was developed to benefit from the strong points of both PSA2FV and CiMPA.Although some case studies have been conducted with CiMPG, it is necessary to do some more.The present paper reports on case studies in which it is formally verified that two authentication protocols enjoy desired properties with CiMPG.

Hybrid systems combine both continuous and discrete behaviors.Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports.In this paper, we propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system in CafeOBJ algebraic specification language and verify it by the proof score method based on equational reasoning implemented in CafeOBJ interpreter.

MCS is widely known as one of the most efficient and influential spinning lock mutual exclusion protocols.The protocol, however, only works under the assumption that processes do not crash while acquiring/releasing the lock or being in the critical section.Furthermore, the exit segment pseudo-code of MCS's algorithm is not wait-free since a process releasing the lock needs to wait for the next process in the virtual queue to perform some steps.A new version of MCS has been proposed by S. Dhoked and N. Mittal such that the new version is wait-free and recoverable (i.e., if some processes crash, the protocol can recover and work normally).In this paper, we formally specify the recoverable wait-free version of MCS and conduct model checking to check whether the protocol enjoys the mutual exclusion property.Our experiments say that: (1) the property is not satisfied if crashes are allowed to occur without any restriction, (2) the protocol enjoys the property if crashes never happen at all, or (3) if crashes have not occurred recently.We also describe the challenge of how to formally specify dynamic memory allocation and present our solution to solve that problem.

Hybrid systems combine both continuous and discrete behaviors, which occur frequently in safety-critical applications in various domains including Internet-of-Things (IoT) and Cyber-Physical Systems (CPS) applications such as health care, transportation, and robotics. For safe and reliable information society with IoT and CPS technologies, it is important to establish a way to specify and verify hybrid systems formally. Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports. We propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system (OTS) in CafeOBJ algebraic specification language. OTSs are models where systems behaviors are described through observations. CafeOBJ supports specification execution based on a rewrite theory. We verify that OTS/CafeOBJ specifications of hybrid systems satisfy desired property by the proof score method based on equational reasoning implemented in CafeOBJ interpreter. In this paper, we specify a signal control system with an arbitrary number of vehicles by our proposed method, and verify the system satisfies a safety property by the proof score method.

Java Pathfinder (JPF) is one of the most mature software model checker developed by NASA for detecting errors lurking in concurrent Java programs. However, the use of JPF often leads to the state space explosion due to the non-determinism of thread interleavings. Parallelization is one mainstream technique to deal with the problem by utilizing the advantage of multi-core processors. Hence, making JPF parallelized to improve the performance in verifying programs is highly desired. In this paper, we present a divide & conquer approach to splitting the entire state space into multiple layers, in which each layer consists of many sub-state spaces so that JPF can independently verify such sub-state spaces in parallel. Some experiments demonstrate that the proposed technique mitigates the state space explosion that prevents the use of only one JPF instance from conducting model checking.

Lemma conjecture is one of the most challenging tasks in theorem proving. The paper focuses on invariant properties (or invariants) of state machines. Thus, lemmas are also invariants. To prove that a state predicate p is an invariant of a state machine M, in general, we need to find an inductive invariant q of M such that q(s) implies p(s) for all states s of M. q is often in the form p∧p', and p'is often in the form q1∧...∧qn. q1, ..., qn are the lemmas of the proof that p is an invariant of M. The paper proposes a technique called Lemma Weakening (LW). LW replaces qi with q'i such that qi(s) implies qi'(s) for all states s of M, which can make the proof reasonably tractable that may become otherwise unreasonably hard. MCS mutual exclusion protocol is used as an example to demonstrate the power of LW.

The paper describes how to formally specify three path finding algorithms in Maude, a rewriting logic-based programming/specification language, and how to model check if they enjoy desired properties with the Maude LTL model checker. The three algorithms are Dijkstra Shortest Path Finding Algorithm (DA), A* Algorithm and LPA* Algorithm. One desired property is that the algorithms always find the shortest path. To this end, we use a path finding algorithm (BFS) based on breadth-first search. BFS finds all paths from a start node to a goal node and the set of all shortest paths is extracted. We check if the path found by each algorithm is included in the set of all shortest paths for the property. A* is an extension of DA in that for each node [Formula: see text] an estimation [Formula: see text] of the distance to the goal node from [Formula: see text] is used and LPA* is an incremental version of A*. It is known that if [Formula: see text] is admissible, A* always finds the shortest path. We have found a possible relaxed sufficient condition. The relaxed condition is that there exists the shortest path such that for each node [Formula: see text] except for the start node on the path [Formula: see text] plus the cost to [Formula: see text] from the start node is less than the cost of any non-shortest path to the goal from the start. We informally justify the relaxed condition. For LPA*, if the relaxed condition holds in each updated version of a graph concerned including the initial graph, the shortest path is constructed. Based on the three case studies for DA, A* and LPA*, we summarize the formal specification and model checking techniques used as a generic approach to formal specification and model checking of path finding algorithms.

The authentication protocol for HTTP proposed in RFC 8120 has been model checked under different assumptions. Four security properties have been taken into account: (1) Key Secrecy Property (K-SEC), (2) Key Sharing Property (K-SHR), (3) Correspondence Property from a client point of view (C-CORR), and (4) Correspondence Property from a server point of view (S-CORR). In each assumption, we suppose that there exists an intruder that eavesdrops on the network and forges messages based on any pieces of information available. Under the assumption (a) that the cryptosystem used is perfect, the formal analysis concludes that the protocol is likely to enjoy K-SEC and K-SHR, but reveals that it enjoys neither C-CORR nor S-CORR. Under the assumption (b) that pseudo-random numbers generated by clients are leaked to the intruder, the results are the same. Under the assumption (c) that pseudo-random numbers generated by servers are leaked to the intruder, however, the protocol enjoys neither K-SEC nor K-SHR. To discover a realistic counterexample for K-SHR, a model checking experiment has been divided into multiple smaller ones. We then propose a revised version, which is likely to enjoy all four properties even under the assumption (c).

Dynamic Software Updating (DSU) is a useful technique for updating running software without incurring any downtime. Its correctness must be guaranteed because updating a running software is a complicated and safety-critical process. In this paper, we present a formal tool called KupC for modeling and verifying dynamic updating of C programs. The tool is built on $$\mathbb {K}$$ –a formal semantic framework for programming languages. We formalize a patch-based dynamic updating mechanism in $$\mathbb {K}$$ based on the formal executable operational semantics of C. The formalization automatically yields an interpreter and several verification tools, which can be used to formally analyze the correctness of dynamic updating for C programs. To our knowledge, KupC is the first formal tool for code-level verification of dynamic software updating.

We have conducted a case study in which an autonomous vehicle intersection control protocol is formally specified in Maude and model checked with Maude model checking facilities.We found that a function used in the protocol should be revised while formally specifying it and a logical clock such that times are total order should be used to avoid deadlock states during model checking experiments.

We propose a concurrent program testing technique that is a specification-based one and uses simulation relations from concurrent programs to formal specifications.For a formal specification S, a concurrent program P and a simulation relation r from P to S, the proposed technique is outlined as follows: (1) state sequences s0, s1, . . ., sn are generated from P , (2) state sequences s 0 , s 1 , . . ., s m for S are obtained by converting s0, s1, . . ., sn with r and (3) it is checked that S can accept s 0 , s 1 , . . ., s m .(1) is very crucial, but we first tackle (2) and (3) and then the present paper focuses on (2) and (3).

A* algorithm is formally specified in Maude and model checked with the Maude LTL model checker.We take into account a graph such that it is a DAG, a goal node is reachable from a start node and each edge is given a nonnegative weight.If h is admissible, namely that h(n) never overestimates the cost to the goal from n for all nodes n, then A* finds a shortest path.The condition, however, can be relaxed.Our model checking experiments make us conjecture that if there exists a shortest path such that for each node n in the path h(n) plus the cost to n from the start node is less than the cost of any non-shortest path to the goal from the start, A* finds a shortest path.

We formally specify a mobile ad hoc network mutual exclusion protocol designed by Walter, Welch and Vaidya in Maude, a specification/programming language based on rewriting logic, and model check that the protocol enjoys the lockout freedom property. Matching equations that can be used as part of the condition of a conditional rewrite rule make it possible to concisely specify complex state transitions. The protocol needs to take into account link failures and/or recoveries, leading to a huge number of states even when there are a small number of nodes. We propose a technique to alleviate the situation, which is called a divide & conquer approach to leads-to model checking. We are interested in the lockout freedom property as one desired property for the protocol in this paper. The property can be expressed with the LTL leads-to connective.

CafeOBJ is a language for writing formal specifications for a wide variety of software and hardware systems and for verifying their properties. CafeOBJ makes it possible to verify properties by using either proof scores, which consists of reducing goal-related terms in user-defined modules, or by using theorem proving. While the former is more flexible, it lacks the formal support to ensure that a property has been really proven. On the other hand, theorem proving might be too strict, since only a predefined set of commands can be applied to the current goal; hence, it hardens the verification of properties. In order to take advantage of the benefits of both techniques, we have extended CafeInMaude, a CafeOBJ interpreter implemented in Maude, with the CafeInMaude Proof Assistant (CiMPA) and the CafeInMaude Proof Generator (CiMPG). CiMPA is a proof assistant for proving inductive properties on CafeOBJ specifications that uses Maude metalevel features to allow programmers to create and manipulate CiMPA proofs. On the other hand, CiMPG provides a minimal set of annotations for identifying proof scores and generating CiMPA scripts for these proof scores. In this article, we present the CiMPA and CiMPG, detailing the behavior of the CiMPA and the algorithm underlying the CiMPG and illustrating the power of the approach by using the QLOCK protocol. Finally, we present some benchmarks that give us confidence in the matureness and usefulness of these tools.

CafeOBJ is an advanced algebraic specification language that can be used for writing formal specifications of various software systems and verifying properties of them. It implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and conduct proofs by executing the proof scores. Despite its usefulness, up to present, the application of CafeOBJ specifications to software development is very limited. Therefore, we would like to propose methods or techniques to make an observation transition system (OTS) in CafeOBJ more usable in both software development and testing. We focus on concurrent systems and how to write concurrent programs in Java based on OTSs. Java has been chosen as the implementation language because concurrency is strongly supported in this language and there are also many powerful testing frameworks in Java that can help us further verify properties of the programs.

The paper proposes a new approach to model checking Chandy-Lamport Distributed Snapshot Algorithm (CLDSA). The essential of the approach is that CLDSA is specified as a meta-program in Maude such that the meta-program takes a specification of an underlying distributed system (UDS) and generates the specification of the UDS on which CLDSA is superimposed (UDS-CLDSA). To model check that a UDS-CLDSA enjoys a desired property, it suffices that human users specify the UDS for the proposed approach, while human users need to specify the UDS-CLDSA for the existing approach for each UDS. Since the proposed approach conducts model checking at meta-level, it produces a counterexample if a UDS-CLDSA does not enjoy the property, while the existing approach does not. Our method specifying CLDSA as a meta-program can be applied to formal specification of the class of distributed algorithms that are superimposed on UDSs.

Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.

Abstract We present in this paper an interpreter implemented in Maude for non-behavioral CafeOBJ specifications. This alternative implementation poses a number of advantages: (1) it allows Maude tools to be used with CafeOBJ specifications, (2) it improves the performance of some CafeOBJ commands, such as search, (3) it enriches CafeOBJ syntax with Maude syntax, and (4) it makes CafeOBJ easily extensible, since new commands and tools can be included and tested and, once they are sufficiently mature, can be considered for inclusion in the Lisp implementation of CafeOBJ. The current tool presents a number of improvements over the tool presented in previous papers: it supports principal sorts, all kinds of CafeOBJ views, and all the search predicates recently implemented in the system. These improvements have allowed us to run the most recent CafeOBJ specifications, hence proving the robustness of the tool. Moreover, we present case studies illustrating the power of the tool, focusing on the falsification and verification of the NSPK and QLOCK protocols, respectively.

Even though software systems in some domains are expected to provide continuous services, most of them must undergo some form of changes. It leads to the emergence of dynamic software updating, a technique for updating a running software system without incurring any downtime. One of the challenges of designing a correct dynamic update is to identify a set of update points where the update can be safely applied to a running system. In this paper, we present a formal approach to modeling dynamic software updates and use the formal model to identify safe update points. In our approach, we formalize dynamic updates as state machines, and verify by model checking a set of desired properties which the running system is expected to satisfy after being updated. If counterexamples are found, we exclude those states that cause the counterexamples, and do model checking again. The process is iterated until all desired properties are successfully verified. We then finally obtain a set of safe update points. A case study is also presented to demonstrate the feasibility of the proposed approach.

This work evaluates Maude, an expressive and executable algebraic specification language, as a potential test sequence generation engine in the context of constraint-based test sequence generation for automotive operating systems. Our approach defines requirement specifications for automotive operating systems compliant with the OSEK/VDX international standard, and specifies constraint patterns in Maude. The correctness of the Maude specification is verified using LTL model checking and the test sequences from each classified environment are generated using reach ability computation provided by the Maude rewriting engine. Experimental evaluation shows that constraint-based test generation using Maude can be as effective as that of using NuS MV, a state machine based specification language specialized for model checking and specification-based testing, but more expressive and flexible.

Model checking liveness properties needs anti-fairness as well as fairness assumptions. As a formula expressing fairness assumptions becomes too long to make liveness model checking feasible, so does one expressing anti-fairness ones. ABP is used as an example to demonstrate that a divide & conquer approach can make liveness model checking under those assumptions feasible.

An approach to making liveness model checking problems under fairness feasible is described. The proposed method divides such a problem into multiple smaller ones that can be conquered such that the former is derived from the latter. Since the proposed method does not need any specialized algorithms, it can use existing LTL model checkers such as Spin, SAL and Maude LTL model checker. The proposed method also lets (or helps) humans get better understanding of the reason why they need to use fairness assumptions.

A state machine can be specified as either an equational theory or a rewrite theory in algebraic approaches. The former is used for theorem proving, and the latter for model checking. We have proposed an approach to transform a class of equational theories into rewrite theories in order to use them in the combination of the two verification techniques. This paper shows the correctness of the transformation with respect to its preservation of invariant properties. Invariant-preservation guarantees that a counterexample found by model checking a generated rewrite theory is also a counterexample of the same invariant in the original equational theory, which provides the theoretical support to the utilization of the transformation in combination of theorem proving and model checking.

Dynamic Software Updating (DSU) is a promising software maintenance technique, which aims at updating running software systems on the fly without incurring any downtime. The systems that require dynamic updating usually require high reliability assurance. Incorrect updating may cause them to behave erratically and/or even crash, and hence results in dreadful loss. However, there are few approaches to the study of the correctness of dynamic updating. In this paper, we systematically discuss the correctness of dynamic updating from a formal perspective, and present a first algebraic approach to formal analysis of it. The basic idea is to formalize dynamic updating systems as rewrite systems, with which we can analyze dynamic updates e.g. verifying their desired properties, or detecting incorrect update points, etc. The formal analysis helps us understand the behaviors of updated systems before we apply updates to the running systems, and hence improves the reliability of the systems after being updated.

Proof scores are documents of comprehensible plans to prove theorems. The proof score approach to systems analysis is a method in which proof scores are used to verify that systems enjoy properties (or analyze systems). In this paper, we describe a way to analyze electronic commerce protocols with the proof score approach, which has been developed and refined through several case studies conducted.

Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method — the OTS/CafeOBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method.

We describe a method of automating invariant verification of behavioral specifications, which are algebraic specifications of abstract machines. The proposed method is based on fixed-point computation, which is one of the standard techniques for automatic (invariant) verification. The proposed method has some notable features. Among them are as follow: (1) the method finds and uses as lemmas state predicates whose invariant proofs may (even mutually) depend on other state predicates whose invariant proofs may not be completed, and (2) the method finds a counterexample showing that an abstract machine does not satisfy an invariant property if any, which does not need to make the (reachable) state space of the abstract machine finite. Crème is a tool based on the proposed method. We also report on two case studies in which (1) Crème proves fully automatically that the NSLPK authentication protocol satisfies the secrecy property and (2) Crème finds a counterexample showing that the NSPK authentication protocol does not satisfy the secrecy property.

Theorem proving and model checking are known as two formal verification techniques that have complementary features. In this paper, we describe a lightweight integration of the two techniques by a translation from theorem proving formalism to model checking formalism, and then treating model checking as part of the decision procedure. In the translation, system and property specifications defined for a theorem prover can be automatically translated to specifications feedable to a model checker after a simple data abstraction. The main aim of this integration is to provide the theorem prover with automatic counter-example generating capability, thus to be able to find "bugs" in the early stage of theorem proving and ease the hard-work of doing theorem proving. A case study is used to demonstrate how this translation works and what the verification flow is when using this integration to do system verification.

We report on a case study in which the Maude model checker has been used to analyze the Suzuki-Kasami distributed mutual exclusion algorithm with respect to the mutual exclusion property and the lockout freedom property. Maude is a specification and programming language/system based on membership equational logic and rewriting logic, equipped with model checking facilities. Maude allows users to use abstract data types, including inductively defined ones, in specifications to be model checked, which is one of the advantages of the Maude model checker. Hence, queues, which are used in the case study, do not have to be encoded in more basic data types. In the case study, the Maude model checker has found a counterexample that the algorithm is lockout free, which has led to one possible modification that makes the algorithm lockout free.

TLS has been formally analyzed with the OTS/CafeOBJ method. In the method, distributed systems are modeled as transition systems, which are written in terms of equations, and it is verified that the models have properties by means of equational reasoning. TLS is the latest version, or the successor of SSL, which is probably the most widely deployed security protocol. Among the results of the analysis are that pre-master secrets cannot be leaked, when a client has negotiated a cipher suite and security parameters with a server, the server has really agreed on them, and client cannot be identified if they do not send their certificates to servers

Chocolat/SMV is a translator that takes a CafeOBJ specification of a transition system called an OTS and generates an SMV specification of a finite version of the OTS. The primary purpose of the translation is to find errors lurked in CafeOBJ specifications of OTSs with SMV.

CafeOBJ is a wide spectrum specification language based on multiple logical foundations. CafeOBJ can be used to specify dynamic as well as static aspects of systems including object-oriented and reactive systems and verify their properties with the help of the CafeOBJ system. In this paper, we show that CafeOBJ can be also used to de-scribe real-time systems and verify their properties. Con-cretely, we evolve UNITY computational models by intro-ducing so-called clock variables so as to model real-time systems, describe a specification of a railroad crossing sys-tem in CafeOBJ and verify that the system has a safety prop-erty based on the specification with the help of the CafeOBJ system. 1.

CafeOBJ is a wide spectrum formal specification language based on multiple logical foundations: mainly initial and hidden algebra. A wide range of systems can be specified in CafeOBJ thanks to its multiple logical foundations. However, distributed real-time systems happen to be excluded from targets of CafeOBJ. The authors propose a method of modeling and verifying such systems based on CafeOBJ, together with timed evolution of UNITY computational models.

HoME is a version of Smalltalk which can be efficiently executed on a multiprocessor and can be executed in parallel by combining a Smalltalk process with a Mach thread and executing the process on the thread. HoME is nearly the same as ordinary Smalltalk except that multiple processes may execute in parallel. Thus, almost all applications running on ordinary Smalltalk can be executed on HoME without changes in their code.