Modular Verification of Sequential Composition for Private Channels in Maude-NPA

Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer

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

Abstract

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.

Original languageEnglish (US)
Title of host publicationSecurity and Trust Management - 14th International Workshop, STM 2018, Proceedings
EditorsCristina Alcaraz, Sokratis K. Katsikas, Sokratis K. Katsikas
PublisherSpringer
Pages20-36
Number of pages17
ISBN (Print)9783030011406
DOIs
StatePublished - 2018
Event14th International Workshop on Security and Trust Management, STM 2018 - Barcelona, Spain
Duration: Sep 6 2018Sep 7 2018

Publication series

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

Other

Other14th International Workshop on Security and Trust Management, STM 2018
Country/TerritorySpain
CityBarcelona
Period9/6/189/7/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Modular Verification of Sequential Composition for Private Channels in Maude-NPA'. Together they form a unique fingerprint.

Cite this