A New Logic for Electronic Commerce Protocols

The primary objective of this paper is to present the deÿnition of a new dynamic, linear and modal logic for security protocols. The logic is compact, expressive and formal. It allows the speciÿcation of classical security properties (authentication, secrecy and integrity) and also electronic commerce properties (non-repudiation, anonymity, good atomicity, money atomicity, certiÿed delivery, etc.). The logic constructs are interpreted over a trace-based model. Traces re ect valid protocol executions in the presence of a malicious smart intruder. The logic is endowed with a tableau-based proof system that leads to a modular denotational semantics and local model checking. c 2002 Elsevier Science B.V. All rights reserved.

• Type: Conference
• Year: 2000
• Where: AMAST
• Authors: Kamel Adi, Mourad Debbabi, Mohamed Mejri
• Keywords: AMAST 2000, Ect Valid Protocol, Logic, Modal Logic, Software Engineering