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

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.