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

Ensuring the safety of autonomous driving systems (ADSs) through rigorous verification in simulated environments is crucial before real-world deployment. However, using simulation environments for ADS testing and verification poses several challenges, including specifying various behaviors of traffic participants and collecting comprehensive real-time data to verify the ADS. To address these challenges, we propose a framework for runtime verification of ADSs, focusing on Autoware, a leading ADS. This framework integrates AWSIM-Script, a scripting language for defining traffic scenarios; Runtime Monitor, a tool to record real-time data during the simulation; and AW-Checker, a Linear Temporal Logic-based property checker for verifying safety requirements. Unlike prior research that primarily focuses on generating critical scenarios, we leverage a well-established ADS safety standard from the Japan Automobile Manufacturers Association and adopt its systematic methodology for safety assessment. We conducted a series of experiments focused on nonintersection road geometry to evaluate Autoware's capability in handling different traffic disturbances such as cut-in, cut-out, and deceleration scenarios. The results revealed that, compared to the competent and careful driver model, which represents the minimum safety requirements for ADSs, Autoware failed to prevent collisions in some cases, particularly during high-speed scenarios and fast lateral movements by other vehicles.

This paper investigates the use of simulation-based testing for Autoware, an open-source autonomous driving system, for scenario-based safety analysis. We employed the AWSIM-Labs simulator to evaluate Autoware within specific scenarios derived from the safety analysis. The results show the feasibility of using simulation for safety evaluation based on these scenarios, while also revealing gaps between the scenario-based safety analysis and the simulation outcomes. We also identified key challenges in addressing these gaps for our future research.

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.

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.

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

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.

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.

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.

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.