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.

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.

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.

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.

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,

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.

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.

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.

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).