Abstract :
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.
Keywords :
automata theory; electronic commerce; formal logic; formal specification; formal verification; security of data; dispute clause; e-commerce; e-contracts; model-checking method; obligation clause; permission clause; prohibition clause; responsibility clause; security clauses; security property specification; security property verification; security rules; temporal constraint clause; Automata; Computer aided software engineering; Contracts; Indium phosphide; Logic; Mechanical factors; Natural languages; Permission; Protocols; Security; e-contract security; model-checking; timed automata;
