Abstract:
Electronic transaction protocols have been found with subtle
flaws. Recently, model checking has been used to verify electronic
transaction protocols for the limitations of low efficiencyand error prone
in the traditional approaches. This paper proposes an extendable verification
model to especially validate electromc transaction protocols. In
particular, the verification model is able to deal with the inconsistency in
transmitted messages. Thus, we can measure the incoherence in secure
messages coming from different sources and at different moments and ensure
the validity of verification result. We analyze two instances by using
this model. The analyses uncover some subtle flaws in the protocols.
