An Efficient Canonical Narrowing Implementation for Protocol Analysis

Raúl López-Rueda, Santiago Escobar, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This work improves the canonical narrowing previously implemented using Maude 2.7.1 by taking advantage of the new functionalities that Maude 3.2 offers. In order to perform more faithful comparisons between algorithms, we have reimplemented Maude’s built-in narrowing using Maude’s metalevel. We compare these two metalevel implementations with Maude’s built-in narrowing, implemented at the C++ level, through a function that collects all the solutions, since the original command only returns one at a time. The results of these experiments are relevant for narrowing-based protocol analysis tools, as well as for improving the analysis of many other narrowing-based applications such as logical model checking, theorem proving or partial evaluation.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
EditorsKyungmin Bae
PublisherSpringer
Pages151-170
Number of pages20
ISBN (Print)9783031124402
DOIs
StatePublished - 2022
Event14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Germany
Duration: Apr 2 2022Apr 3 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13252 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Country/TerritoryGermany
CityMunich
Period4/2/224/3/22

Keywords

  • Canonical narrowing
  • Maude
  • Narrowing modulo
  • Reachability analysis
  • Security protocols

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'An Efficient Canonical Narrowing Implementation for Protocol Analysis'. Together they form a unique fingerprint.

Cite this