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~α 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.
展开▼
