A MODEL FOR SECURE PROTOCOLS AND THEIR COMPOSITIONS

This paper develops a foundation for reasoning about protocol security . We adopt a model-based approach for defining protocol security prope rties. This allows us to describe security properties in greater detai l and precision than previous frameworks. Our model allows us to reaso n about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition theorem which allows us to state sufficient conditions on two secure protocols A and B suc h that they may be combined to form a new secure protocol C. Moreover, we give counter-examples to show that when the conditions are not met , the protocol C may not be secure.