Verifying the SET Purchase Protocols