Rewriting logic is a logical framework for expressing both concurrent computation and logical deduction using equations and rewrite rules. Quantitative equational reasoning enriches equations with quantitative measures, expressing concepts such as similarity or proximity rather than mere equality of terms. In this article, we bring these two approaches together and propose a quantitative extension of rewriting logic as a flexible formalism for quantitative deduction and computation.

We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is combined with inductive theorem proving to discharge inductive verification conditions that ensure useful symbolic state space reductions. An obvious combination is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible combination. In this paper we focus instead on a new deductive model checking methodology to verify invariants —including inductive invariants— of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle . Inductive verification conditions not discharged automatically by the oracle are dealt with by commands that refine some constrained patterns by useful semantic equivalences, and by using an inductive theorem prover in interactive mode. This methodology is demonstrated by means of concurrent system examples using two Maude tools working in tandem: the DM-Check narrowing-based symbolic model checker, and the NuITP inductive theorem prover.

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.

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.

NuITP is an inductive equational theorem prover that combines advanced symbolic techniques such as narrowing, equality predicates, variant unification, variant satisfiability, order-sorted congruence closure, ordered rewriting, and strategy-based rewriting (all applied modulo axioms) to verify equational programs with expressive features such as sorts and subsorts, conditional equations and rewriting modulo axioms in Maude and in other equational languages. The present paper introduces the tool, explains its most commonly used inference rules, and illustrates their use in proving the card trick benchmark.

Maude is a high-performance logical framework based on rewriting logic and supporting formal specification, verification and declarative programming of concurrent systems. Since most concurrent open systems are made up of actor-like objects that communicate with each other through message passing, Maude provides special features to support their specification, verification and programming. Since open systems are heterogeneous, involving widely different kinds of objects such as sensors, actuators, devices, databases, graphical user interfaces, and so on, Maude supports declarative message-passing interaction between Maude objects and a wide variety of heterogeneous external objects. In this paper we explain and illustrate a methodology where an open system can first be designed and verified in Maude and then implemented as a distributed system of heterogeneous objects in a way that seamlessly bridges the gap between its formal specification and verification and its distributed implementation.

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.

Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal cryptographic protocol analysis, which is why narrowing and unification are used in tools such as Maude-NPA, Tamarin and Akiss. In this work we present the implementation of a canonical narrowing algorithm, which improves the standard narrowing algorithm, extended to be able to process rewrite theories with conditional rules. The conditions of the rules will contain SMT constraints, which will be carried throughout the execution of the algorithm to determine if the solutions have associated satisfiable or unsatisfiable constraints, and in the latter case, discard them.

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.

In this paper, we develop an automated optimization framework for rewrite theories that supports sorts, subsort overloading, equations and algebraic axioms with free/non-free constructors, and rewrite rules modeling concurrent system transitions whose state structure is defined by means of the equations. The main idea of the framework is to make the system computations more efficient by partially evaluating the equations to the specific calls that are required by the transition rules. This can be particularly useful for automatically optimizing rewrite theories that contain overly general equational theories which perform unnecessary and costly computations involving pattern matching and/or unification modulo equations and axioms. The transformation is based on a suitable unfolding operator parameter that relies on the symbolic operational engine of Maude's equational theories, called folding variant narrowing, together with a generic abstraction operator. Depending on the properties of the rewrite theory, the unfolding and abstraction operators must be fine-tuned to achieve the biggest optimization possible while ensuring termination and total correctness of the transformation. We formalize two instances of our scheme for the case when the rewrite theory either has an infinite number of most general variants or a finite number of most general variants. Finally, we discuss some experimental results which demonstrate that the proposed optimization technique pays off in practice.

Abstract This paper introduces $\tt{{Presto}}$ , a symbolic partial evaluator for Maude’s rewriting logic theories that can improve system analysis and verification. In $\tt{{Presto}}$ , the automated optimization of a conditional rewrite theory $\mathcal{R}$ (whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of $\mathcal{R}$ , an underlying, companion equational logic theory $\mathcal{E}$ that specifies the algebraic structure of the system states of $\mathcal{R}$ . This can be particularly useful for specializing an overly general equational theory $\mathcal{E}$ whose operators may obey complex combinations of associativity, commutativity, and/or identity axioms, when being plugged into a host rewrite theory $\mathcal{R}$ as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used. $\tt{{Presto}}$ implements different unfolding operators that are based onfolding variant narrowing(the symbolic engine of Maude’s equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of $\tt{{Presto}}$ in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by $\tt{{Presto}}$ may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations.

The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and verification. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equational axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of different, increasingly efficient formulations of the homeomorphic embedding relation modulo axioms that we implement in Maude. Our experimental results show that the most efficient version indeed pays off in practice.

Abstract Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude’s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.

We perform an automated analysis of two devices developed by Yubico: YubiKey, de- signed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol an- alyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known at- tacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Abstract This paper introducesGLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity. This novel equational unification relies on built-in generation of the set ofvariantsof a termt, i.e., the canonical form oftσ for a computed substitution σ. Variant generation relies on a novel narrowing strategy calledfolding variant narrowingthat opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies thefinite variant property, i.e., there is a finite number of most general variants for every term in the theory. However, variant narrowing computations can be extremely involved and are simply presented in text format by Maude, often being too heavy to be debugged or even understood. TheGLINTSsystem provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of nodeembeddingandclosednessmodulo axioms, and (iv) querying and inspecting selected parts of the variant trees.

Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool.

Recent advances in the automated analysis of cryptographic protocols have aroused new interest in the practical application of unification modulo theories, especially theories that describe the algebraic properties of cryptosystems. However, this application requires unification algorithms that can be easily implemented and easily extended to combinations of different theories of interest. In practice this has meant that most tools use a version of a technique known as variant unification. This requires, among other things, that the theory be decomposable into a set of axioms B and a set of rewrite rules R such that R has the finite variant property with respect to B. Most theories that arise in cryptographic protocols have decompositions suitable for variant unification, but there is one major exception: the theory that describes encryption that is homomorphic over an Abelian group.

A concurrent system can be naturally specified as a rewrite theory R = (Sigma, E, R) where states are elements of the initial algebra of terms modulo E and concurrent transitions are axiomatized by the rewrite rules R. Under simple conditions, narrowing with rules R modulo equations E can be used to symbolically represent the system's state space by means of terms with logical variables. We call this symbolic representation a "logical state space" and it can also be used for model checking verification of LTL properties. Since in general such a logical state space can be infinite, we propose several abstraction techniques for obtaining either an over-approximation or an under-approximation of the logical state space: (i) a folding abstraction that collapses patterns into more general ones, (ii) an easy-to-check method to define (bisimilar) equational abstractions, and (iii) an iterated bounded model checking method that can detect if a logical state space within a given bound is complete. We also show that folding abstractions can be faithful for safety LTL properties, so that they do not generate any spurious counterexamples. These abstraction methods can be used in combination and, as we illustrate with examples, can be effective in making the logical state space finite. We have implemented these techniques in the Maude system, providing the first narrowing-based LTL model checker we are aware of.

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variant-based unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.

The length of the microprocessor development cycle is largely determined by functional verification, where contemporary practice relies primarily on constraint-based random stimulus generation to drive a simulation-based methodology. However, formal methods are, in particular, gaining wider adoption and are seen as having potential to bridge large gaps left by current techniques. And many gaps still remain. In this paper we propose directed- logical testing: a new method of stimulus generation based on purely logical techniques (i.e. formal methods). As far as we know, our methodology represents the first end-to-end mathematical formalization of the stimulus generation problem. Therefore, a major contribution of this paper is the definition of a class of logical propositions that relate the actual microprocessor implementation, the assembly program stimulus, and a coverage goal. These propositions are given in rewriting logic, and use the idea of rewriting semantics to automatically formalize within a common logical framework the microprocessor implementation and assembly programs. To solve these propositions, we demonstrate how narrowing and user-defined narrowing strategies can be used as a scalable logical framework. In addition, we describe two classes of effective strategies that can be used for many microprocessors and common coverage goals. Finally, we describe a prototype tool implementation and present empirical data to demonstrate the feasibility of our methodology. Since narrowing and user-defined narrowing strategies within rewriting logic do not yet have tool support, our prototype tool uses standard rewriting and user-defined rewriting strategies to simulate narrowing.

Abstract The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change the result. In this work, we provide methods for the analysis and elimination of redundant arguments in term rewriting systems as a model for the programs that can be written in more sophisticated languages. On the basis of the uselessness of redundant arguments, we also propose an erasure procedure which may avoid wasteful computations while still preserving the semantics (under ascertained conditions). A prototype implementation of these methods has been undertaken, which demonstrates the practicality of our approach.

Outermost-needed rewriting/narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential constructor systems. Its parallel extension (known as weakly) deals with non-inductively sequential constructor systems. In this paper, we present natural rewriting, a suitable extension of (weakly) outermost-needed rewriting which is based on a refinement of the demandness notion associated to the latter, and we extend it to narrowing. Intuitively, natural rewriting (narrowing) always reduces (narrows) the most often demanded position in a term. We formalize the strategy for left-linear constructor systems though, for the class of inductively sequential constructor systems, natural rewriting (narrowing) behaves even better than outermost-needed rewriting (narrowing) in the avoidance of failing computations. With regard to inductively sequential constructor systems, we introduce a larger class of systems called inductively sequential preserving where natural rewriting and narrowing preserve optimality for sequential parts of the program. We also provide a prototype interpreter of natural rewriting and narrowing.