A new logic for electronic commerce protocols

DOI10.1016/S0304-3975(02)00364-XzbMath1008.68047MaRDI QIDQ1853749

Mourad Debbabi, Kamel Adi, Mohamed Me Jri

Publication date: 22 January 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

denotational semantics; logic; authentication; secrecy; tableau-based proof system; e-commerce protocols; eryptographic protocols; good atomicity; money atomicity

Mathematics Subject Classification ID

68P25: Data encryption (aspects in computer science)

Related Items

An analytic tableau calculus for a temporalised belief logic, A game-theoretic framework for specification and verification of cryptographic protocols, Injective synchronisation: An extension of the authentication hierarchy, A (restricted) quantifier elimination for security protocols, Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography

Uses Software

• NRL
• Murphi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An attack on the Needham-Schroeder public-key authentication protocol
• Applying a formal analysis technique to the CCITT X.509 strong two-way authentication protocol
• Tableau-based model checking in the propositional mu-calculus
• A calculus of mobile processes. II
• A calculus for cryptographic protocols: The spi calculus
• Three systems for cryptographic protocol analysis
• Proof theory and automated deduction
• A formal language for cryptographic protocol requirements
• A lattice-theoretical fixpoint theorem and its applications
• The NRL Protocol Analyzer: An Overview
• On the security of public key protocols
• A logic of authentication
• A semantics for a logic of authentication (extended abstract)
• A formal framework for authentication