A quantifier-free first-order knowledge logic of authentication

MaRDI QIDQ5486065zbMATH OpenFDO

Authors Mirosław Kurkowski, Marian Srebrny

Publication date 6 September 2006

zbMATH Keywords

authenticationformal methodsknowledgemodel checkingsecurityverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Authentication, digital signatures and secret sharing (94A62)

Recommendations

• scientific article; zbMATH DE number 2080723
• An omniscience-free temporal logic of knowledge for verifying authentication protocols
• An epistemic foundation for authentication logics (extended abstract)
• A logic of authentication
• Formal semantics for authentication logics

Cited in

(8)

• An omniscience-free temporal logic of knowledge for verifying authentication protocols
• An epistemic foundation for authentication logics (extended abstract)
• scientific article; zbMATH DE number 1330437 (Why is no real title available?)
• scientific article; zbMATH DE number 2080723 (Why is no real title available?)
• Formal semantics for authentication logics
• A (restricted) quantifier elimination for security protocols
• Knowledge structure approach to verification of authentication protocols
• Cryptographic protocol logic: satisfaction for (timed) Dolev-Yao cryptography

Describes a project that uses

Uses Software

• Casper
• Velev SAT Benchmarks

This page was built for publication: A quantifier-free first-order knowledge logic of authentication

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