A (restricted) quantifier elimination for security protocols

DOI10.1016/J.TCS.2006.08.037MaRDI QIDQ860909zbMATH OpenOpenAlexWikidataFDO

Authors N. E. Zubov

Publication date 9 January 2007

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

Full work available at URL https://doi.org/10.1016/j.tcs.2006.08.037

zbMATH Keywords

verificationdecidabilitysecurity protocols

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Authentication, digital signatures and secret sharing (94A62) Quantifier elimination, model completeness, and related topics (03C10)

Recommendations

• Bounding messages for free in security protocols -- extension to various security properties
• Dynamic tags for security protocols
• A quantifier-free first-order knowledge logic of authentication
• From One Session to Many: Dynamic Tags for Security Protocols
• Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1956510 (Why is no real title available?)
• scientific article; zbMATH DE number 1962758 (Why is no real title available?)
• A new logic for electronic commerce protocols
• A semantics for a logic of authentication (extended abstract)
• Authentication and delegation with smart-cards
• Authentication tests and the structure of bundles.
• Computer science today. Recent trends and developments
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Information based reasoning about security protocols
• On the security of public key protocols
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Secure protocol composition
• Using encryption for authentication in large networks of computers

Cited in

(5)

• Distributed temporal logic for the analysis of security protocol models
• Bounding Messages for Free in Security Protocols
• From One Session to Many: Dynamic Tags for Security Protocols
• Dynamic tags for security protocols
• Bounding messages for free in security protocols -- extension to various security properties

This page was built for publication: A (restricted) quantifier elimination for security protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q860909)