Describing and verifying dual digital signature using Petri net

Dual digital signature is one of the important techniques utilized in electronic payment transactions to ensure the security for cardholder, merchant and bank. Petri net provides an effective method to describe and verify the cryptographic protocol. By adopting a petri net model, the properties of the dual digital signature applied in electronic payment system were discussed from both static and dynamic perspectives. The static analysis established the dual digital signature petri net model for formal description. The dynamic simulation using reachability tree verified the reachability, the boundness, and the liveness of the cryptographic protocol. Furthermore, it was analyzed that the dual digital signature could resist attacks. The results show that dual digital signature can be applied in the electronic payment to enhance its security.