To know or not to know: Epistemic approaches to security protocol verification
The authors survey the epistemic approaches to security protocol verification with the questions: are security protocols essentially about knowledge (what is there to know), what kind of knowledge can we distinguish (how to know), and does an epistemic approach bring benefits (why to know)? First they distinguish between different types of knowledge relevant in the security setting, and then give an overview of commonly used techniques in the epistemic approaches. In particular, they compare various equivalence relations defined in the literature (simple deduction equivalence, pattern matching equivalence, static equivalence, permutation equivalence) that correspond to the semantics of propositional knowledge. They also compare two major epistemic logical approaches proposed to model interaction in multi-agent systems. It turns out that, in the security protocol verification setting, ETL (epistemic temporal logic) approaches are more suitable to model message passing over time, based on which appropriate equivalence relation can be generated. On the other hand, the DEL (dynamic epistemic logic) approach offers all freedom to model higher-order information and uncertainties in term of agents' knowledge about each other. The model checker results of ETL also confirm that it is better to focus on a single agent case: in security setting, this would be the intruder. Finally, they collect clues for the comparison of expressivity of ETL and TL (temporal logic), in order to see when an epistemic approach is inevitable. They show under the assumption of synchronicity, that ETL can define more (security) properties of the temporal structures.
- Toward reasoning about security protocols: a semantic approach
- Temporal logics of knowledge and their applications in security
- Knowledge structure approach to verification of authentication protocols
- Symbolic model checking for temporal-epistemic logic
- Automatic verification of temporal-epistemic properties of cryptographic protocols
- A data symmetry reduction technique for temporal-epistemic logic
- A knowledge based semantics of messages
- A logic of authentication
- A semantics for a logic of authentication (extended abstract)
- A Theory of Communicating Sequential Processes
- An essay in modal logic
- Automata, Languages and Programming
- Automatic verification of temporal-epistemic properties of cryptographic protocols
- Bounds on secret key exchange using a random deal of cards
- Computer Aided Verification
- Computing Knowledge in Security Protocols under Convergent Equational Theories
- CONCUR 2005 – Concurrency Theory
- Dealing with logical omniscience: expressiveness and pragmatics
- Deductive Algorithmic Knowledge
- Dynamic epistemic logic with branching temporal structures
- Formalising Receipt-Freeness
- Foundations of Security Analysis and Design II
- scientific article; zbMATH DE number 3902018 (Why is no real title available?)
- scientific article; zbMATH DE number 88991 (Why is no real title available?)
- scientific article; zbMATH DE number 1962758 (Why is no real title available?)
- scientific article; zbMATH DE number 1487488 (Why is no real title available?)
- scientific article; zbMATH DE number 1500666 (Why is no real title available?)
- scientific article; zbMATH DE number 795590 (Why is no real title available?)
- scientific article; zbMATH DE number 2196583 (Why is no real title available?)
- Knowledge and common knowledge in a distributed environment
- Logic of information flow on communication channels
- Logics of communication and change
- Merging frameworks for interaction
- Mobile values, new names, and secure communication
- Model Checking Knowledge and Linear Time: PSPACE Cases
- Model Checking on Trees with Path Equivalences
- Model checking Russian cards
- Modeling adversaries in a logic for security protocol analysis
- Modelling knowledge and action in distributed systems
- Monadic second order definable relations on the binary tree
- On the security of public key protocols
- Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap
- Preserving Secrecy Under Refinement
- Probabilistic dynamic belief revision
- Programming Languages and Systems
- Reasoning about information change
- Reconciling two views of cryptography (The computational soundness of formal encryption)
- Refinement of Kripke Models for Dynamics
- Symbolic model checking for temporal-epistemic logic
- The dining cryptographers problem: Unconditional sender and recipient untraceability
- The logic of public announcements, common knowledge, and private suspicions
- The Russian cards problem
- Towards an awareness-based semantics for security protocol analysis
- Uniform inevitability is tree automaton ineffable
- Update semantics of security protocols
- Using encryption for authentication in large networks of computers
- VERICS 2007 -- a model checker for knowledgee and real-time
- Verifying privacy-type properties of electronic voting protocols: a taster
- An omniscience-free temporal logic of knowledge for verifying authentication protocols
- Endogenizing epistemic actions
- Towards an awareness-based semantics for security protocol analysis
- Toward reasoning about security protocols: a semantic approach
- Temporal logics of knowledge and their applications in security
- Deciding knowledge in security protocols under some e-voting theories
- An epistemic foundation for authentication logics (extended abstract)
- Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap
- Epistemic Cord logic: verifying anonymous routing protocols in Ad Hoc network
- Computing Knowledge in Security Protocols under Convergent Equational Theories
- Two Applications of Epistemic Logic in Computer Security
- Challenges for decidable epistemic logics from security protocols
- Automata, Languages and Programming
- Probability timed automata for investigating communication processes
- Knowledge structure approach to verification of authentication protocols
This page was built for publication: To know or not to know: Epistemic approaches to security protocol verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q625717)
