Researchers　have　proposed　several　security　protocols　to　protect　the　electronic　commerce　security　in　these　years;　however,　not　all　of　them　are　secure　enough.　This　article　extends　model　checking　method　with　Casper/FDR2　to　model　and　analyze　a　new　electronic　protocol.　Attacks　are　found　in　the　protocol　and　their　mechanisms　are　discussed.　A　variety　of　solutions　are　given　to　different　security　flaws.　The　improved　protocol　is　proven　to　be　robust　and　secure.　©　2012　Wuhan　University　and　Springer-Verlag　Berlin　Heidelberg.