Search

Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.

Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.

Two “knowingly incomplete,” yet useful, variant-based satisfiability procedures for QF formulas in the instantiations of two, increasingly more expressive, parameterized data types of strings are proposed. The first has four selector functions decomposing a list concatenation into its parts. The second adds a list membership predicate. The meaning of “parametric” here is much more general than is the case for decision procedures for strings in current SMT solvers, which are parametric on a finite alphabet. The parameterized data types presented here are parametric on a (typically infinite) algebraic data type of string elements. The main result is that if an algebraic data type has a variant satisfiability algorithm, then the data type of strings over such elements has a “knowingly incomplete,” yet practical, variant satisfiability algorithm, with no need for a Nelson-Oppen combination algorithm relating satisfiability in strings and in the given data type.

This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the same-origin policy (SOP) in reachability logic. It shows how these properties can be deductively verified using our constructor-based reachability logic theorem prover. This paper also highlights the reasoning techniques used in the proof and three modularity principles that have been crucial to scale up and complete the verification effort.

We present an inductive inference system for proving validity of formulas in the initial algebra \(T_{\mathcal {E}}\) of an order-sorted equational theory \(\mathcal {E}\) with 17 inference rules, where only 6 of them require user interaction, while the remaining 11 can be automated as simplification rules and can be combined together as a limited, yet practical, automated inductive theorem prover. The 11 simplification rules are based on powerful equational reasoning techniques, including: equationally defined equality predicates, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting and recursive path orderings. For \(\mathcal {E} = (\varSigma , E \uplus B)\), these techniques work modulo B, with B a combination of associativity and/or commutativity and/or identity axioms.

Lecture Notes in Computer Science, 12229, ISSN:0302-9743, ISSN:1611-3349, NASA Formal Methods. 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings, ISBN:978-3-030-55753-9, ISBN:978-3-030-55754-6

So far, results about variants, the finite variant property (FVP), and variant unification have been developed for equational theories \(E \cup B\) where B is a set of axioms having a finitary unification algorithm, and the equations E, oriented as rewrite rules \(\vec {E}\), are convergent modulo B. The extension to the case when B has an infinitary unification algorithm, for example because of non-commutative symbols having associative axioms, seems undeveloped. This paper takes a first step in developing such an extension. In particular, the relationships between the FVP and the boundedness properties, the identification of conditions on \(E \cup B\) ensuring FVP, and the effective computation of variants and variant unifiers are explored in detail. The extension from the finitary to the infinitary case includes both surprises and opportunities.

This work proposes canonical constrained narrowing, a new symbolic reachability analysis technique applicable to topmost rewrite theories where the equational theory has the finite variant property. Our experiments suggest that canonical constrained narrowing is more efficient than both standard narrowing and the previously studied contextual narrowing. These results are relevant not only for Maude-NPA, but also for symbolically analyzing many other concurrent systems specified by means of rewrite theories.

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 increasingly efficient formulations of the homeomorphic embedding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

Reachability logic has been applied to \(\mathbb {K}\) rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Constructor-based semantic unification, matching, and satisfiability procedures greatly increase the range of decidable background theories that can be used in reachability logic proofs. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.

Terminating functional programs should be deterministic, i.e., should evaluate to a unique result, regardless of the evaluation order. For equational functional programs such determinism is exactly captured by the ground confluence property. For terminating equations this is equivalent to ground local confluence, which follows from local confluence. Checking local confluence by computing critical pairs is the standard way to check ground confluence. The problem is that some perfectly reasonable equational programs are not locally confluent and it can be very hard or even impossible to make them so by adding more equations. We propose a three-step strategy to prove that an equational program as is is ground confluent: First: apply the strategy proposed in [9] to use non-joinable critical pairs as completion hints to either achieve local confluence or reduce the number of critical pairs. Second: use the inductive inference system proposed in this paper to prove the remaining critical pairs ground joinable. Third: to show ground confluence of the original specification, prove also ground joinable the equations added. These methods apply to order-sorted and possibly conditional equational programs modulo axioms such as, e.g., Maude functional modules.

Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.

We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems \(u =^? v\) such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.

A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [3] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [8] for standard rewrite theories, including a generalized notion of coherence, are given. Finally, symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations.

Walter is a distributed partially replicated data store providing Parallel Snapshot Isolation (PSI), an important consistency property that offers attractive performance while ensuring adequate guarantees for certain kinds of applications. In this work we formally model Walter’s design in Maude and formally specify and verify PSI by model checking. To also analyze Walter’s performance we extend the Maude specification of Walter to a probabilistic rewrite theory and perform statistical model checking analysis to evaluate Walter’s throughput for a wide range of workloads. Our performance results are consistent with a previous experimental evaluation and throw new light on Walter’s performance for different workloads not evaluated before.

This paper gives a modular verification methodology in which, given parametric specifications of a key establishment protocol P and a protocol Q providing private channel communication, security and authenticity properties of their sequential composition \(P\; ;\; Q\) can be reduced to: (i) verification of corresponding properties for P, and (ii) verification of corresponding properties for an abstract version \(Q^\alpha \) of Q in which keys have been suitably abstracted. Our results improve upon previous work in this area in several ways. First of all, we both support a large class of equational theories and provide tool support via the Maude-NPA cryptographic protocol analysis tool. Secondly as long as certain conditions on P and Q guaranteeing the secrecy of keys inherited by Q from P are satisfied, our results apply to the composition of any two reachability properties of the two protocols.

Partial evaluation (PE) is a powerful and general program optimization technique with many successful applications. However, it has never been investigated in the context of expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts and overloading; and equational rewriting modulo axioms such as commutativity, associativity–commutativity, and associativity–commutativity–identity. In this paper, we illustrate the key concepts by showing how they apply to partial evaluation of expressive rule-based programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on equational least general generalization for ensuring global termination. We demonstrate the use of the resulting partial evaluator for program optimization on several examples where it shows significant speed-ups.

Arriving at a mature distributed system design through implementation and experimental validation is a labor-intensive task. This limits the number of design alternatives that can be explored in practice. In this work we use formal modeling with probabilistic rewrite rules and statistical model checking to explore and extend the design space of the RAMP (Read Atomic Multi-Partition) transaction system for large-scale partitioned data stores. Specifically, we formally model in Maude eight RAMP designs, only two of which were previously implemented and evaluated by the RAMP developers; and we analyze their key consistency and performance properties by statistical model checking. Our results: (i) are consistent with the experimental evaluations of the two implemented designs; (ii) are also consistent with conjectures made by the RAMP developers for other unimplemented designs; and (iii) uncover some promising new designs that seem attractive for some applications.

This paper introduces some novel features of Maude 2.7. We have added support for: i built-in order-sorted unification modulo associativity, commutativity, and identity, ii built-in variant generation, iii built-in order-sorted unification modulo a finite variant theory, and iv symbolic reachability modulo a finite variant theory.

Non-Functional Properties (NFPs) are crucial in the design of software. Specification of systems is used in the very first phases of the software development process for the stakeholders to make decisions on which architecture or platform to use. These specifications may be analyzed using different formalisms and techniques, simulation being one of them. During a simulation, the relevant data involved in the analysis of the NFPs of interest can be measured using monitors. In this work, we show how monitors can be parametrically specified so that the instrumentation of specifications to be monitored can be automatically performed. We prove that the original specification and the automatically obtained specification with monitors are bisimilar by construction. This means that the changes made on the original system by adding monitors do not affect its behavior. This approach allows us to have a library of possible monitors that can be safely added to analyze different properties, possibly on different objects of our systems, at will.

Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra \(T_{\varSigma /E}\) when the theory \((\varSigma ,E)\) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation in Maude 2.7 of variant satisfiability using these sub-algorithms.

Although different satisfiability decision procedures can be combined by algorithms such as those of Nelson-Oppen or Shostak, current tools typically can only support a finite number of theories to use in such combinations. To make SMT solving more widely applicable, generic satisfiability algorithms that can allow a potentially infinite number of decidable theories to be user-definable, instead of needing to be built in by the implementers, are highly desirable. This work studies how folding variant narrowing, a generic unification algorithm that offers good extensibility in unification theory, can be extended to a generic variant-based satisfiability algorithm for the initial algebras of its user-specified input theories when such theories satisfy Comon-Delaune’s finite variant property (FVP) and some extra conditions. Several, increasingly larger infinite classes of theories whose initial algebras enjoy decidable variant-based satisfiability are identified and illustrated with examples.

Recently, a new dependency pair framework for proving operational termination of Conditional Term Rewriting Systems (CTRSs) has been introduced. We call it 2D Dependency Pair (DP) Framework for CTRSs because it makes explicit and exploits the bidimensional nature of the termination behavior of conditional rewriting, where rewriting steps \(s\rightarrow t\) and rewritings \(s\rightarrow ^*t\) (in zero or more steps) are defined for specific terms \(s\) and \(t\) by using an inference system where appropriate proof trees should be exhibited for such particular goals. In this setting, the horizontal component of the termination behavior concerns the existence of infinite sequences of rewriting steps, and the vertical component captures infinitely many climbs during the development of a proof tree for a single rewriting step. In this paper we extend the 2D DP Framework for CTRSs with several powerful processors for proving and disproving operational termination that specifically exploit the structure of conditional rules. We provide the first implementation of the 2D DP Framework as part of the termination tool mu-term. Our benchmarks suggest that, with our new processors, the 2D DP Framework is currently the most powerful technique for proving operational termination of CTRSs.

A patternt, i.e., a term possibly with variables, denotes the set language $$\llbracket t \rrbracket $$ of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. But for the more expressive patterns needed in declarative languages supporting rich type disciplines such as subtype polymorphism untyped pattern operations and algorithms break down. We show how they can be properly defined by means of a signature transformation $$\varSigma \mapsto \varSigma ^{\#}$$ that enriches the types of $$\varSigma $$. We also show that this transformation allows a systematic reduction of the first-order logic properties of an initial order-sorted algebra supporting subtype-polymorphic functions to equivalent properties of an initial many-sorted i.e., simply typed algebra. This yields a new, simple proof of the known decidability of the first-order theory of an initial order-sorted algebra.

The promise of high scalability and availability has prompted many companies to replace traditional relational database management systems RDBMS with NoSQL key-value stores. This comes at the cost of relaxed consistency guarantees: key-value stores only guarantee eventual consistency in principle. In practice, however, many key-value stores seem to offer stronger consistency. Quantifying how well consistency properties are met is a non-trivial problem. We address this problem by formally modeling key-value stores as probabilistic systems and quantitatively analyzing their consistency properties by statistical model checking. We present for the first time a formal probabilistic model of Apache Cassandra, a popular NoSQL key-value store, and quantify how much Cassandra achieves various consistency guarantees under various conditions. To validate our model, we evaluate multiple consistency properties using two methods and compare them against each other. The two methods are: 1 an implementation-based evaluation of the source code; and 2 a statistical model checking analysis of our probabilistic model.

Cryptographic Application Programmer Interfaces Crypto APIs are designed to allow a secure interoperation between applications and cryptographic devices such as smartcards and Hardware Security Modules HSMs. However, several Crypto APIs have been shown to be subject to attacks in which sensitive information is disclosed to an attacker, such as the RSA Laboratories Public Key Standards PKCS#11, an API widely adopted in industry. Recently, there has been a growing interest on applying automated crypto protocol analysis methods to formally analyze APIs. However, the PKCS#11 has been proven difficult to analyze using such methods since it involves non-monotonic mutable global state. In this paper we specify and analyze the PKCS#11 in Maude-NPA, a general purpose crypto protocol analysis tool.

The modeling and analysis of mobile ad hoc networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectionality can interact in unforeseen ways that are hard to model and analyze by automatic formal methods. In this work we use rewriting logic and Real-Time Maude to address this challenge. We propose a composable formal framework for MANET protocols and their mobility models that can take into account such complex interactions. We illustrate our framework by analyzing a well-studied leader election protocol for MANETs in the presence of both mobility and uni- and bidirectional links.

Termination can be thought of as the property of programs ensuring that every input is given an answer in finite time. There are, however, many different (combinations of) programming paradigms and languages for these paradigms. Is a common formal definition of termination of programs in any (or most) of these programming languages possible? The notion of operational termination provides a general definition of termination which relies on the logic-based description of (the operational semantics of) a programming language. The key point is capturing termination as the absence of infinite inference, that is: all proof attempts must either successfully terminate, or they must fail in finite time. This global notion is well-suited for most declarative languages, where programs are theories in a logic whose inference system is specialized to each theory to characterize its computations. Other programming languages (e.g., imperative languages) and applications (e.g., the evaluation of specific expressions and goals in functional and logic programs) require a more specialized treatment which pays attention not just to theories, but to specific formulas to be proved within the given theory. For instance, the execution of an imperative program can be viewed as a proof of an specific formula (representing the program) within the computational logic describing the operational semantics of the programming language. In such cases, an appropriate definition of termination should focus on proving the absence of infinite proofs for computations localized to specific goals. In this paper we generalize the global notion of operational termination to this new setting and adapt the recently introduced OT-framework for mechanizing proofs of operational termination to support proofs of localized operational termination.

Research in the formal analysis of cryptographic protocols has produced much good work in the solving of equality constraints, developing new methods for unification, matching, and deducibility. However, considerably less attention has been paid to disequality constraints. These also arise quite naturally in cryptographic protocol analysis, in particular for analysis of indistinguishability properties. Thus methods for deciding whether or not they are satisfiable could potentially be quite useful in reducing the size of the search space by protocol analysis tools. In this paper we develop a framework for reasoning about disequality constraints centered around the paradigm of the most discriminating Dolev-Yao attacker, who is able to detect a disequality if it is satisfied in some implementation of the crypto-algebra satisfying given equality properties. We develop several strategies for handling disequalities, prove their soundness and completeness, and demonstrate the result of experimental analyses using the various strategies. Finally, we discuss how disequality checking algorithms could be incorporated within symbolic reachability protocol analysis methods.

Many cyber-physical systems are hierarchical distributed control systems whose components operate with different rates, and that should behave in a virtually synchronous way. Designing such systems is hard due to asynchrony, skews of the local clocks, and network delays; furthermore, their model checking is typically unfeasible due to state space explosion. Multirate PALS reduces the problem of designing and verifying virtually synchronous multirate systems to the much simpler tasks of specifying and verifying their underlying synchronous design. To make the Multirate PALS design and verification methodology available within an industrial modeling environment, we define in this paper the modeling language Multirate Synchronous AADL, which can be used to specify multirate synchronous designs using the AADL modeling standard. We then define the formal semantics of Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification into the OSATE tool environment for AADL. Finally, we show how an algorithm for smoothly turning an airplane can be modeled and analyzed using Multirate Synchronous AADL.

Fault tolerance has been a major concern in the design of computing platforms. However, currently, fault tolerance has been done mostly with just heuristics, high level probabilistic analysis and extensive testing. In this work, we explore how we can use formal patterns to achieve fault-tolerance designs and methods. In particular, we look at faults that occur in mechanical button interfaces such as button bounce, button stuck, and phantom button faults. Our primary goal is the safety of such interfaces for medical devices [7], but the methods are more widely applicable. We formally describe corresponding patterns to address these faults including button debouncing, button stuck detection, and phantom press filtering. We prove stuttering-bisimulation results for some patterns showing their fault-masking capabilities. Furthermore, for patterns where fault-masking is not possible, we prove fault-detection properties. We also instantiate these patterns to a simple instance of a button-press counter and perform execution and model checking as further validation.

Intuitively, two protocols \({\mathcal P}_1\) and \({\mathcal P}_2\) are indistinguishable if an attacker cannot tell the difference between interactions with \({\mathcal P}_1\) and with \({\mathcal P}_2\). In this paper we: (i) propose an intuitive notion of indistinguishability in Maude-NPA; (ii) formalize such a notion in terms of state unreachability conditions on their synchronous product; (iii) prove theorems showing how —assuming the protocol’s algebraic theory has a finite variant (FV) decomposition– these conditions can be checked by the Maude-NPA tool; and (iv) illustrate our approach with concrete examples. This provides for the first time a framework for automatic analysis of indistinguishability modulo as wide a class of algebraic properties as FV, which includes many associative-commutative theories of interest to cryptographic protocol analysis.

The linear temporal logic of rewriting (LTLR) is a simple extension of LTL that adds spatial action patterns to the logic, expressing that a specific instance of an action described by a rewrite rule has been performed. Although the theory and algorithms of LTLR for finite-state model checking are well-developed [2], no theoretical foundations have yet been developed for infinite-state LTLR model checking. The main goal of this paper is to develop such foundations for narrowing-based logical model checking of LTLR properties. A key theme in this paper is the systematic relationship, in the form of a simulation with remarkably good properties, between the concrete state space and the symbolic state space. A related theme is the use of additional state space reduction methods, such as folding and equational abstractions, that can in some cases yield a finite symbolic state space.

Distributed key-value stores are quickly becoming a key component of cloud computing systems. In order to improve read/write latency, distributed key-value stores offer weak notions of consistency to clients by using many complex design decisions. However, it is challenging to formally analyze consistency behaviors of such systems, both because there are few formal models, and because different consistency level combinations render understanding hard, particularly under communication latency. This paper presents for the first time a formal executable model in Maude of Cassandra, a popular key-value store. We formally models Cassandra’s main components and design strategies. We formally specify various consistency properties and model check them against our model under various communication latency and consistency combinations.

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze infinite-state open systems, i.e., systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism, which is proper to the system, and external non-determinism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. The proposed technique is illustrated with the formal analysis of a real-time system that is beyond the scope of timed-automata methods.

For an infinite-state concurrent system \(\mathcal{S}\) with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s → s′ are witnessed by concrete transitions between states in \(\mathcal{S}\) satisfying the respective sets of predicates s and s′. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems \(\mathcal{S}\) described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method—based on rewriting, semantic unification, and variant narrowing—to automatically generate a predicate abstraction when the formal specification of \(\mathcal{S}\) is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.

Standards for cryptographic protocols have long been attractive candidates for formal verification. It is important that such standards be correct, and cryptographic protocols are tricky to design and subject to non-intuitive attacks even when the underlying cryptosystems are secure. Thus a number of general-purpose cryptographic protocol analysis tools have been developed and applied to protocol standards. However, there is one class of standards, security application programming interfaces (security APIs), to which few of these tools have been applied. Instead, most work has concentrated on developing special-purpose tools and algorithms for specific classes of security APIs. However, there can be much advantage gained from having general-purpose tools that could be applied to a wide class of problems, including security APIs. One particular class of APIs that has proven difficult to analyze using general-purpose tools is that involving exclusive-or. In this paper we analyze the IBM 4758 Common Cryptographic Architecture (CCA) protocol using an advanced automated protocol verification tool with full exclusive-or capabilities, the Maude-NPA tool. This is the first time that API protocols have been satisfactorily specified and analyzed in the Maude-NPA, and the first time XOR-based APIs have been specified and analyzed using a general-purpose unbounded session cryptographic protocol verification tool that provides direct support for AC theories. We describe our results and indicate what further research needs to be done to make such protocol analysis generally effective., Antonio González-Burgueño, Sonia Santiago and Santiago Escobar have been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana PROMETEO2011/052. José Meseguer has been partially supported by NSF Grant CNS 13-10109.

Mobile ad hoc networks (MANETs) are increasingly popular and deployed in a wide range of environments. However, it is challenging to formally analyze a MANET, both because there are few reasonably accurate formal models of mobility, and because the large state space caused by the movements of the nodes renders straightforward model checking hard. In particular, the combination of wireless communication and node movement is subtle and does not seem to have been adequately addressed in previous formal methods work. This paper presents a formal executable and parameterized modeling framework for MANETs in Real-Time Maude that integrates several mobility models and wireless communication. We illustrate the use of our modeling framework with the Ad hoc On-Demand Distance Vector (AODV) routing protocol, which allows us to analyze this protocol under different mobility models.

\(\textsf {DY}^\star \) is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the \(\textsf {F}^\star \) programming language. Unlike automated symbolic provers, \(\textsf {DY}^\star \) accounts for advanced protocol features like unbounded loops and mutable recursive data structures as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Protocols modeled in \(\textsf {DY}^\star \) can be executed, and hence, tested, and they can even interoperate with real-world counterparts. \(\textsf {DY}^\star \) extends a long line of research on using dependent type systems but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. With this, one can uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security.