Paper Info
Title
Modular Verification of Sequential Composition for Private Channels in Maude-NPA.
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.
Year
Venue
Field
2018
STM
Computer science,Computer security,Secrecy,Communication channel,Theoretical computer science,Key establishment protocol,Reachability,Parametric statistics,Cryptographic protocol analysis,Modular design
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
11
4
Name
Order
Citations
PageRank
Fan Yang191.15
Santiago Escobar245227.87
Catherine Meadows392889.05
José Meseguer49533805.39