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-Verlag Berlin Heidelberg
Pages20-36
Number of pages17
ISBN (Print)9783030011406
DOIs
StatePublished - Jan 1 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
CountrySpain
CityBarcelona
Period9/6/189/7/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

    Yang, F., Escobar, S., Meadows, C., & Meseguer, J. (2018). Modular Verification of Sequential Composition for Private Channels in Maude-NPA. In C. Alcaraz, S. K. Katsikas, & S. K. Katsikas (Eds.), Security and Trust Management - 14th International Workshop, STM 2018, Proceedings (pp. 20-36). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11091 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-030-01141-3_2