Verifying the Independence of Security Protocols

Abstract
Determining if two protocols can be securely run alongside each other requires analyzing the independence of the involved protocols. In this paper we construct a canonical model of security protocols that allows us to conduct a syntactical analysis on the independence of multiple security protocols. By integrating participant knowledge in the model, we are able to detect subtle multi-protocol attacks, where the types of certain message components can not be checked, also known as type-flaw attacks. Of special interest is the construction of messages in the proposed model, which is made by mapping each message component from the regular specification to a type. We provide a theorem for analyzing the independence of security protocols and illustrate its applicability by analyzing two protocols.

This publication has 9 references indexed in Scilit: