Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
type: Item
instance of: scholarly article
title: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
zbMATH Open document ID: 1115.68079
author: Prasannaa Thati
author: José Meseguer
published in: Higher-Order and Symbolic Computation
publication date: 2007-05-21T00:00:00Z
Mathematics Subject Classification ID: 68P25
zbMATH DE Number: 5155274
zbMATH Keywords: Rewrite theories
zbMATH Keywords: Narrowing
zbMATH Keywords: Reachability
zbMATH Keywords: Security protocols
describes a project that uses: Isabelle
describes a project that uses: Maude
describes a project that uses: NRL
describes a project that uses: Timbuk
MaRDI profile type: Publication
full work available at URL: s10990-007-9000-6
OpenAlex ID: W2042987983
cites work: Q4536615
cites work: A needed narrowing strategy
cites work: Conditional narrowing modulo a set of equations
cites work: Q4251060
cites work: Verification on infinite structures.
cites work: FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
cites work: An NP decision procedure for protocol insecurity with XOR
cites work: Reflection in rewriting logic. Metalogical foundations and metaprogramming applications
cites work: Maude: specification and programming in rewriting logic
cites work: Q4447224
cites work: On the security of public key protocols
cites work: Q4936148
cites work: Functional and Logic Programming
cites work: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
cites work: Term Rewriting and Applications
cites work: Well-structured transition systems everywhere!
cites work: Q2723425
cites work: Reachability Analysis of Term Rewriting Systems with Timbuk
cites work: The integration of functions into logic programming: From theory to practice
cites work: Q3883561
cites work: Q2767013
cites work: Q3664457
cites work: Q4447232
cites work: Control and data abstraction: The cornerstones of practical formal verification
cites work: Property preserving abstractions for the verification of concurrent systems
cites work: The NRL Protocol Analyzer: An Overview
cites work: Q3046721
cites work: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
cites work: Conditional rewriting logic as a unified model of concurrency
cites work: Q3839051
cites work: Q4447253
cites work: Isabelle. A generic theorem prover
cites work: Fast narrowing-driven partial evaluation for inductively sequential programs
cites work: Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
cites work: An attack on a recursive authentication protocol. A cautionary tale
cites work: Q4818812
cites work: Programming in equational logic: Beyond strong sequentiality
cites work: Q4421726
cites work: Algebra and Coalgebra in Computer Science
cites work: Rewriting Techniques and Applications
DOI: 10.1007/S10990-007-9000-6
description: scientific article; zbMATH DE number 5155274