Specification and verification of security properties of e-contracts

In this paper, we present new templates to specify the requirements of e-contracts, to securely check the well-execution of their clauses and to verify some security properties. To achieve this goal, we first analyze the contract of an illustrative e-commerce example. Then, through this example, we derive the most relevant security requirements of e-contracts. In particular, we characterize e-contract security rules / clauses by defining obligations, prohibitions, permissions, temporal constraints, responsibilities and disputes. We demonstrate how this kind of security requirements can be described using a timed automata formalism. Moreover, we show how verifying methods, such as model-checking, can be applied to this kind of models to check some security properties.