An omniscience-free temporal logic of knowledge for verifying authentication protocols

DOI10.1007/S41980-018-0087-9zbMath1486.68101OpenAlexW2784270315MaRDI QIDQ1734134

Xianqiang Yang

Publication date: 22 March 2019

Published in: Bulletin of the Iranian Mathematical Society (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s41980-018-0087-9

zbMATH Keywords

formal verificationauthentication protocolslogical omnisciencetemporal epistemic logics

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Authentication, digital signatures and secret sharing (94A62)

Cites Work

• Unnamed Item
• Unnamed Item
• An analytic tableau calculus for a temporalised belief logic
• Dealing with logical omniscience: expressiveness and pragmatics
• To know or not to know: Epistemic approaches to security protocol verification
• Reconciling two views of cryptography (The computational soundness of formal encryption)
• Modeling Adversaries in a Logic for Security Protocol Analysis
• Reasoning about Protocol Change and Knowledge
• Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
• Automatic verification of temporal-epistemic properties of cryptographic protocols
• A semantics for a logic of authentication (extended abstract)

This page was built for publication: An omniscience-free temporal logic of knowledge for verifying authentication protocols