Analysis of Yahalom-Paulson protocol and its improvement

A detailed analysis of the original Yahalom-Paulson protocol and its simplified version given by Backes and Pfitzmann was presented. It was found that there exists a type flaw attack on the original one and the simplified one can not guarantee the agreement on new session keys between legitimate parties due to replay attacks. The protocol was adapted and the new version was proved correct based on strand space theory.