Abstract:
In common sense, electronic transactions through
secure transaction protocols are secure. However, not all
so-called secure transaction protocols are secure. To
verify the protocols this paper proposes the NDL (nonmonotonic
dvnamic logic. A novel idea of fail-negate,
namely non-monotonic, is proposed in NDL. Thus some
security properties are believed to be true,if we based on
current conditions, cannot prove they are false. On the
other hand, the dynamic property in NDL converts the
transaction into an action sequences. To evaluate the
logic, two instances are illustrated. From the evaluation,
it is convinced that the NDL is effective and promising.
