Electronic Commerce and Internet in wireless networks are profoundly changing the way of payment, but there is still little confidence among users concerning the security of their data. The application of formal techniques to the modelling and design of electronic commerce protocols should help to improve their reliability and so enhance the choices of these new technologies. In this paper, we show how the Casper, a special-purpose formal methods tool designed for the verification of the security protocols, was used in the analysis of the BCY(Beller, Chang, Yacobi), the Carlsen BCY and the Mu-Varadharajan BCY protocols. We describe the results of our analysis, which uncovered several vulnerabilities in the specification that would have made possible attacks such as man-in-the-middle attack and replay attack. Finally, we propose a new protocol resistant to these attacks and formally verify its correctness.