Search

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.To achieve this goal, we develop and give formal semantics to a process algebra for cryptographic protocols that supports a rich taxonomy of choice primitives for composing strand spaces. In our taxonomy, deterministic and non-deterministic choices are broken down further. Non-deterministic choice can be either explicit, i.e., one of two paths is chosen, or implicit, i.e. the value of a variable is chosen non-deterministically. Likewise, deterministic choice can be either an (explicit) if-then-else choice, i.e. one path is chosen if a predicate is satisfied, while the other is chosen if it is not, or implicit deterministic choice, i.e. execution continues only if a certain pattern is matched. We have identified a class of choices which includes finite branching and some cases of infinite branching, which we address in this paper.Our main theoretical results are two bisimulation results: one proving that the formal semantics of our process algebra is bisimilar to the forwards execution semantics of its associated strands, and another showing that it is also bisimilar with respect to the symbolic backwards semantics of the strands such as that supported by Maude-NPA. At the practical level, we present a prototype implementation of our process algebra in Maude-NPA, illustrate its expressive power and naturalness with various examples, and show how it can be effectively used in formal analysis.

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.

El proposito de este articulo es identificar elementos y caracteristicas de la innovacion empresarialque se tienen en cuenta en la politica de transformacion productiva en el pais. Laestrategia metodologica empleada para lograr este proposito fue la revision, sistematizaciony analisis de articulos de acuerdo con las categorias innovacion y transformacion productiva.Como principal resultado este analisis se encontro que la innovacion es un eje fundamentalde la transformacion productiva, porque orienta el fortalecimiento industrial con apoyo aldesarrollo de las empresas; sin embargo, su insercion ha sido debil. A traves de ella se visibilizanlos cambios y se constituyen dinamicas que enlazan actividades e integran la diversidadde culturas, a traves de las cuales se acumula conocimiento y se garantizan competenciasindividuales y colectivas que se transforman en potencialidades sociales para las empresas

Basic narrowing is a restricted form of narrowing which constrains narrowing steps to a set of unblocked (or basic) positions. In this work, we study the modularity of termination of basic narrowing in hierarchical combinations of TRSs, which provides new algorithmic criteria to prove termination of basic narrowing. Basic narrowing has a number of important applications including equational unification in canonical theories. Another application is analyzing termination of narrowing by checking the termination of basic narrowing, as done in pioneering work by Hullot. As a particularly interesting application, we consider solving equations modulo a theory that is given by a TRS, and then distill a number of modularity results for the decidability of equational unification via the modularity of basic narrowing (completeness and) termination.

In previous work, an abstract certification technique for Java source code was proposed based on rewriting logic, which is a semantic framework that has been efficiently implemented in the rule–based programming language Maude. Starting from a specification of a (generic) Java abstract semantics written in Maude, we develop an abstract verification technique that essentially consists of a reachability analysis using the Java abstract semantics. We provide facilities to associate abstract domains to the variables of the considered Java program so that the resulting state–space is finite. As a by–product of the abstract verification, a safety certificate is delivered that contains a set of (abstract) rewriting proofs that can be checked by the code consumer using a standard rewriting logic engine. The main advantage is that the amount of code that must be explicitly trusted is very small. This paper presents a Web tool that implements the abstract certification technique by providing appropriate abstract domains for different safety properties while hiding the technical details of the method from the user. The tool has been devised to be easily extendable to other properties and domains. It currently supports the certification of two kinds of safety properties that are not handled by standard Java compilers: secure integer arithmetic rules and non–interference policies.

Generalization, also called anti-unification, is the dual of unification. Given terms t and t′, a generalization is a term t″ of which t and t′ are substitution instances. The dual of a most general unifier (mgu) is that of least general generalization (lgg). In this work, we extend the known untyped generalization algorithm to an order-sorted typed setting with sorts, subsorts, and subtype polymorphism. Unlike the untyped case, there is in general no single lgg. Instead, there is a finite, minimal set of lggs, so that any other generalization has at least one of them as an instance. Our generalization algorithm is expressed by means of an inference system for which we give a proof of correctness. This opens up new applications to partial evaluation, program synthesis, and theorem proving for typed reasoning systems and typed rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude.

The NRL Protocol Analyzer (NPA) is a tool for the formal specification and analysis of cryptographic protocols that has been used with great effect on a number of complex real-life protocols. One of the most interesting of its features is that it can be used to reason about security in face of attempted attacks on low-level algebraic properties of the functions used in a protocol. Recently, we have given for the first time a precise formal specification of the main features of the NPA inference system: its grammar-based techniques for (co-)invariant generation and its backwards narrowing reachability analysis method; both implemented in Maude as the Maude-NPA tool. This formal specification is given within the well-known rewriting framework so that the inference system is specified as a set of rewrite rules modulo an equational theory describing the behavior of the cryptographic symbols involved. This paper gives a high-level overview of the Maude-NPA tool and illustrates how it supports equational reasoning about properties of the underlying cryptographic infrastructure by means of a simple, yet nontrivial, example of an attack whose discovery essentially requires equational reasoning. It also shows how rule-based programming languages such as Maude and complex narrowing strategies are useful to model, analyze, and verify protocols.

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., Accepted for publication in Theory and Practice of Logic Programming

‘Ciudadelas en los conflictos” es una tesis de Maestría quequiere mostrar cómo el proceso conceptual de la fotografía vade la realidad a la representación por modelos, pero tambiéncómo las representaciones de estos modelos adquieren unnuevo significado, la realidad de virtualismo y la ilusión. Usarinstalaciones o interactuar con modelos es inventar imaginarios, ollamar memorias, que podrían ser puestos sobre una base tangiblepara fotografiarlas después.Quiero reflexionar sobre ciudades imaginarias y la utopía de laguerra y el desplazamiento, imaginando cada foto como unaciudadela. Los modelos construidos que acompañan este textose entienden como fortalezas, ya que incluyen, a veces al azar,todas las variables sociales, culturales y físicas que las ciudadestienen, como “imitación de la vida”. Una metáfora de las variadase irónicas miradas de un desplazado, se podrían obtener al llegara las ciudades o a los lugares urbanos. Por lo tanto, el ciudadanoinesperado vive dentro de una ciudadela en el conflicto. Elfenómeno de la guerra y el desplazamiento forzado son lacartografía de las nuevas ciudades en Colombia, que se registranen esta obra de una manera triste y satirizada. Abstract This dissertation Citadels in Conflict wants to show howthe conceptual process of photography goes from realityto representation by models, but also how representationsof these models acquire a new significance, the reality ofvirtualism and illusion. To use installations or interact withmodels is to invent imaginaries –or to call memories– thatcould be placed on a tangible base… and later photographed.I want to reflect on imaginary cities and the utopia of war anddisplacement, picturing each photo as a citadel. The constructedmodels accompanying this text are understood as citadels, forthey include –sometimes randomly– all social, cultural andphysical variables that cities have, or as “imitations of life”. Ametaphor of the varied and ironic glances a desplazado couldget when arriving in cities or any other urban places. Therefore,the unexpected citizen dwells inside a citadel in conflict. Thephenomena of war and forced displacement are mapping newcities in Colombia in sad and iconic ways as satirized in thesesixteen images.

The access to ophthalmological care in Chile has been historically a problem. Only at the end of the twentieth century concrete solutions were promoted. In 1960, Primary Care Ophthalmologic Units were created to ease the access to ophthalmology, due to the efforts of Professor Juan Arentsen. Their functioning was organized and standardized subsequently using a model proposed by the Chilean Ophthalmologic Society, leading to a better patient flow and reducing waiting lists. These units became an innovative initiative to reduce the gaps in Chilean public health, optimizing the professional and infrastructural assets of the public health care system and achieving a new organization for the ophthalmological health care net.

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.

This paper is a tribute to Jose Meseguer, from the rest of us in the Maude team, reviewing the past, the present, and the future of the language and system with which we have been working for around two decades under his leadership. After reviewing the origins and the language’s main features, we present the latest additions to the language and some features currently under development. This paper is not an introduction to Maude, and some familiarity with it and with rewriting logic are indeed assumed.

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.

Strategy annotations provide a simple mechanism for introducing some laziness in the evaluation of expressions. As an eager programming language, Maude can take advantage of them and, in fact, they are part of the language. Maude strategy annotations are lists of non-negative integers associated to function symbols which specify the ordering in which the arguments are (eventually) evaluated in function calls. A positive index enables the evaluation of an argument whereas 'zero' means that the function call has to be attempted. The use of negative indices has been proposed to express evaluation on-demand, where the demand is an attempt to match an argument term with the left-hand side of a rewrite rule. In this paper we show how to furnish Maude with the ability of dealing with on-demand strategy annotations.

Strategy annotations are used in several rewriting-based programming languages to introduce replacement restrictions aimed at improving efficiency and/or reducing the risk of nontermination. Unfortunately, rewriting restrictions can have a negative impact on the ability to compute normal forms. In this paper, we first ascertain/clarify the conditions ensuring correctness and completeness (regarding normalization) of computing with strategy annotations. Then, we define a program transformation methodology for (correct and) complete evaluations which applies to OBJ-like languages.

Strategy annotations are used in eager programming languages (e.g., OBJ2 , OBJ3 , CafeOBJ , and Maude ) for improving efficiency and/or reducing the risk of nontermination. Syntactically, they are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index forces the evaluation of an argument whereas a negative index means “evaluation on-demand”. Recently, we have introduced a formal description of the operational meaning of such on-demand strategy annotations which improves previous formalizations that were lacking satisfactory computational properties. In this paper, we introduce an automatic, semantics-preserving program transformation which produces a program (without negative annotations) which can be then correctly executed by typical OBJ interpreters. Moreover, to demonstrate the practicality of our ideas, the program transformation has been implemented (in Haskell ) and we compare the evaluation of transformed programs with the original ones on a set of representative benchmarks.

Strategy annotations are used in rule-based programming languages such as OBJ2 , OBJ3 , CafeOBJ , and Maude to improve efficiency and/or reduce the risk of nontermination. Syntactically, they are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index forces the evaluation of an argument whereas a negative index means "evaluate on-demand". In this paper, we present OnDemandOBJ , an implementation of strategy-guided on-demand evaluation, which improves previous mechanizations that were lacking satisfactory computational properties.

We demonstrate that the problem of identifying redundant arguments of function symbols, i.e. parameters which can be replaced by any expression without changing the associated semantics, boils down to proving the validity of a particular class of inductive theorems in the equational theory of confluent, sufficiently complete term rewriting systems (TRSs). Hence, existing results for proving inductive theorems can be exploited to solve the problem in many interesting cases where previously developed methods fail to recognize and remove redundancies. In particular, this novel formulation directly yields a new decidability result for the redundancy problem which is based on the so-called standard theories . As an additional result which stems from the inductive encoding of the redundancy problem, we finally propose two different techniques for the analysis of redundant arguments, which are respectively based on inductionless induction and abstract rewriting (a technique for approximating normal forms in sufficiently complete, left linear, canonical TRSs).

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.In this paper we address this problem by studying various approximations of homomorphic encryption over an Abelian group. We construct a hierarchy of increasingly richer theories, taking advantage of new results that allow us to automatically verify that their decompositions have the finite variant property. This new verification procedure also allows us to construct a rough metric of the complexity of a theory with respect to variant unification, or variant complexity. We specify different versions of protocols using the different theories, and analyze them in the Maude-NPA cryptographic protocol analysis tool to assess their behavior. This gives us greater understanding of how the theories behave in actual application, and suggests possible techniques for improving performance.

The access to ophthalmological care in Chile has been historically a problem. Only at the end of the twentieth century concrete solutions were promoted. In 1960, Primary Care Ophthalmologic Units were created to ease the access to ophthalmology, due to the efforts of Professor Juan Arentsen. Their functioning was organized and standardized subsequently using a model proposed by the Chilean Ophthalmologic Society, leading to a better patient flow and reducing waiting lists. These units became an innovative initiative to reduce the gaps in Chilean public health, optimizing the professional and infrastructural assets of the public health care system and achieving a new organization for the ophthalmological health care net.

The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It tries to find secrecy or authentication attacks by searching backwards from an insecure attack state pattern that may contain logical variables, in such a way that logical variables become properly instantiated in order to find an initial state. The execution mechanism for this logical reachability is narrowing modulo an equational theory. Although Maude-NPA also possesses a forwards semantics naturally derivable from the backwards semantics, it is not suitable for state space exploration or protocol simulation.In this paper we define an executable forwards semantics for Maude-NPA, instead of its usual backwards one, and restrict it to the case of concrete states, that is, to terms without logical variables. This case corresponds to standard rewriting modulo an equational theory. We prove soundness and completeness of the backwards narrowing-based semantics with respect to the rewriting-based forwards semantics. We show its effectiveness as an analysis method that complements the backwards analysis with new prototyping, simulation, and explicit-state model checking features by providing some experimental results.

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.

Natural Language (NL) processing tools, such as tokenizers, part-of speech taggers or syntactic processors obtain knowledge from a set of documents (e.g., tokens, syntactic patterns, etc.) and produce the different elements that will take part on the discourse universe in a NL text (e.g., noun phrases, verbs, sentences, etc.). In this paper, we present how NL software systems development can be performed incrementally by using a high-performance specification language like Maude. A generic algebraic specification for NL is defined, including sorts and sub-sorts apart from equational properties, such as associativity and commutativity for built-in lists and sets. Then, the full discourse universe, available for NL processing, is described in terms of the algebraic specification by providing a non-deterministic but terminating set of transformation rules. Finally, and as a proof of concept, a set of documents for NL processing is given to Maude as an input term and successfully transformed into a proper document, exploring all the non-deterministic possibilities, as well as resolving the ambiguity in language. The main advantages of implementing NL in this manner are: generality, transparency, extensibility, reusability, and maintainability. To the best of our knowledge, this is the first attempt to represent and develop complex NL software systems with this formal notation, and based on the analysis conducted, this implementation constitute the basis for the design and development of more specific NL processing applications, such as text summarization.

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.

We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems s=?ts=?t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification., S. Escobar and S. Santiago were partially supported by EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors were partially supported by NSF: S. Escobar, J. Meseguer, and R. Sasse under CNS 09-04749 and CCF 09- 05584; D. Kapur under CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under CNS 09-05378, and P. Narendran and S. Erbatur under CNS 09-05286. Part of the S. Erbatur’s work was supported while with the Department of Computer Science, University at Albany, and part of R. Sasse’s work was supported while with the Department of Computer Science, University of Illinois at Urbana-Champaign.

We address a problem that arises in cryptographic protocol analysis when the equational properties of the cryptosystem are taken into account: in many situations it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the equational theory. We give a tool-independent methodology for state exploration, based on unification and narrowing, that generates states that obey these irreducibility constraints, called contextual symbolic reachability analysis, prove its soundness and completeness, and describe its implementation in the Maude-NPA protocol analysis tool. Contextual symbolic reachability analysis also introduces a new type of unification mechanism, which we call asymmetric unification, in which any solution must leave the right side of the solution irreducible. We also present experiments showing the effectiveness of our methodology., S. Escobar and S. Santiago have been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors have been partially supported by NSF: S. Escobar, J. Meseguer and R. Sasse under grants CCF 09- 05584, CNS 09-04749, and CNS 09-05584; D. Kapur under grant CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under grant CNS 09-05378, and P. Narendran and S. Erbatur under grant CNS 09-05286.

La crisis argentina es la primera de un pais latinoamericano en la sociedad globalizada. No tiene causas ni soluciones puramente internas o que dependan exclusivamente de los recursos nacionales de poder. Inmersos como estamos en un ciclo civilizatorio caracterizado por el descentramiento social de la politica, el relativismo cultural, la mundializacion de la economia y el cambio en los paradigmas de la seguridad, sus efectos resultan fundamentales para entender los posibles escenarios que enfrentara la region en un futuro cercano. Esa mezcla de crisis macroeconomica, desintegracion social, tension maxima del pacto federal y perdida total de legitimidad de la clase politica y de los mecanismos de representacion, en un contexto de violencia social difusa, esta deshaciendo insfitucionalmente al pais. La participacion en la situacion de organismos internacionales fuera de toda responsabilidad estatal, y el desarrollo de una crisis de seguridad humana sin que medie una clara solidaridad externa, son signos inquietantes de un nuevo orden internacional prescindente en lo politico y social, y que transfonna a paises enteros en zonas de indiferencia.

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.

There is a growing interest in formal methods and tools to analyze cryptographic protocols modulo algebraic properties of their underlying cryptographic functions. It is well-known that an intruder who uses algebraic equivalences of such functions can mount attacks that would be impossible if the cryptographic functions did not satisfy such equivalences. In practice, however, protocols use a collection of well-known functions, whose algebraic properties can naturally be grouped together as a union of theories E 1... ¿ n. Reasoning symbolically modulo the algebraic properties E 1... ¿ n requires performing (E 1... ¿ n)-unification. However, even if a unification algorithm for each individual E i is available, this requires combining the existing algorithms by methods that are highly non-deterministic and have high computational cost. In this work we present an alternative method to obtain unification algorithms for combined theories based on variant narrowing. Although variant narrowing is less efficient at the level of a single theory E i, it does not use any costly combination method. Furthermore, it does not require that each E i has a dedicated unification algorithm in a tool implementation. We illustrate the use of this method in the Maude-NPA tool by means of a well-known protocol requiring the combination of three distinct equational theories. © 2011 Springer-Verlag., R. Sasse and J. Meseguer have been partially supported by NSF Grants CNS0716638, CNS-0831064 and CNS-0904749. S. Escobar has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2007-68093- C02-02. C. Meadows has been partially supported by NSF Grant CNS-0904749, National Science Foundation, EEUU

Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows to occur from high to low security levels. Erasure is a way of strengthening confidentiality by upgrading data confidentiality levels, up to the extreme of demanding the removal of secret data from the system. In this paper, we propose a certification technique for confidentiality of complete Java classes that includes non-interference and erasure policies. This technique is based on rewriting logic, which is a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. In order to achieve a finite state transition system, we develop an abstract Java semantics which correctly approximates non-interference and erasure. The analysis produces certificates that are independently checkable, and are small enough to be used in practice. We have implemented our methodology and developed some experiments that demonstrate the feasibility of our approach.

In this tutorial, we give an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the analysis of cryptographic protocols using functions that obey different equational theories. We show the reader how to use Maude-NPA, and how it works, and also give some of the theoretical background behind the tool.

This paper presents a modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work provides a missing connection between least general generalization and computing modulo equational theories, and opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as partial evaluators, test case generators, and machine learning techniques, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.

In this paper we propose a certification technique for non-interference of Java programs based on rewriting logic, a very general logical and semantic framework efficiently implemented in the high-level programming language Maude. Non---interference is a semantic program property that prevents illicit information flow to happen. Starting from a basic specification of the semantics of Java written in Maude, we develop an information---flow extension of this operational Java semantics which allows us to observe non-interference of Java programs. Then we develop in Maude an abstract, finite-state version of the information-flow operational semantics which supports finite program verification. As a by---product of the verification, a certificate of non-interference is delivered which consists of a set of (abstract) rewriting proofs that can be easily checked by the code consumer using a standard rewriting logic engine.

Basic narrowing is a restricted form of narrowing which constrains narrowing steps to a set of non-blocked (or basic) positions. Basic narrowing has a number of important applications including equational unification in canonical theories. Another application is analyzing termination of narrowing by checking the termination of basic narrowing, as done in pioneering work by Hullot. In this work, we study the modularity of termination of basic narrowing in hierarchical combinations of TRSs, including a generalization of proper extensions with shared subsystem. This provides new algorithmic criteria to prove termination of basic narrowing.

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.

In this paper we propose an abstract certification techniquefor Java which is based on rewriting logic, a very general logical and semanticframework efficiently implemented in the functional programminglanguage Maude. Starting from a specification of the Java semantics writtenin Maude, we develop an abstract, finite-state operational semanticsalso written in Maude which is appropriate for program verification. Asa by-product of the abstract verification, a dependable safety certificateis delivered which consists of a set of (abstract) rewriting proofs thatcan be easily checked by the code consumer using a standard rewritinglogic engine. Our certification methodology extends to other programminglanguages by simply replacing the concrete semantics of Java by asemantics for the programming language at hand. The abstract proofcarryingcode technique has been implemented and successfully testedon several examples, which demonstrate the feasibility of our approach.

The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties that includes many crypto-systems of interest such as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks for attacks by searching backwards from an insecure attack state, and assumes an unbounded number of sessions. Because of the unbounded number of sessions and the support for different equational theories, it is necessary to develop ways of reducing the search space and avoiding infinite search paths. As a result, we have developed a number of state space reduction techniques. In order for the techniques to prove useful, they need not only to speed up the search, but should not violate soundness so that failure to find attacks still guarantees security. In this paper we describe the state space reduction techniques we use. We also provide soundness proofs, and experimental evaluations of their effect on the performance of Maude-NPA.

In this work, we extend the dependency pair approach for automated proofs of termination in order to prove the termination of narrowing. Our extension of the dependency pair approach generalizes the standard notion of dependency pairs by taking specifically into account the dependencies between the left-hand side of a rewrite rule and its own argument subterms. We demonstrate that the new narrowing dependency pairs exactly capture the narrowing termination behavior and provide an effective termination criterion which we prove to be sound and complete. Finally, we discuss how the problem of analyzing narrowing chains can be recast as a standard analysis problem for traditional (rewriting) chains, so that the proposed technique can be effectively mechanized by reusing the standard DP infrastructure.

Rewriting is a general and expressive way of specifying concurrent systems, where concurrent transitions are axiomatized by rewrite rules. Narrowing is a complete symbolic method for model checking reachability properties. We show that this method can be reinterpreted as a lifting simulation relating the original system and the symbolic system associated to the narrowing transitions. Since the narrowing graph can be infinite, this lifting simulation only gives us a semi-decision procedure for the failure of invariants. However, we propose new methods for folding the narrowing tree that can in practice result in finite systems that symbolically simulate the original system and can be used to algorithmically verify its properties. We also show how both narrowing and folding can be used to symbolically model check systems which, in addition, have state predicates, and therefore correspond to Kripke structures on which ACTL* and LTL formulas can be algorithmically verified using such finite symbolic abstractions.

The NRL Protocol Analyzer (NPA) is a tool for the formal specification and analysis of cryptographic protocols that has been used with great effect on a number of complex real-life protocols. It probably outranks any of the existing tools in the sheer range of the types of attacks it is able to model and discover. However, the techniques in NPA lack an independent formal specification and model, and instead are closely intertwined with other NPA features. The main contribution of this paper is to rectify this problem by giving for the first time a precise formal specification of one of the main features of the NPA inference system: its grammar-based techniques for invariant generation, as well as a backwards reachability analysis method that captures some of the key features of the NPA. This formal specification is given within the well-known rewriting framework so that the inference system is specified as a set of rewrite rules modulo an equational theory describing the behavior of the cryptographic algorithms involved.