An approach to prove confidentiality of cryptographic protocols with non-atomic keys

We propose an approach to prove confidentiality of non-atomic key cryptographic protocols based on Dolev-Yao model in this paper. We use graph to make the analysis more intuitional. Moreover, our approach gives a clear distinction to different data types, and is compatible with Strand Space Model completely. It shows expansibility by added the description of Diffie-Hellman exchange.