Knowledge structure approach to verification of authentication protocols
The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of Kripke semantics called knowledge structure and, by this kind of Kripke semantics, analyzes communication protocols over hostile networks, especially on authentication protocols. Compared with BAN-like logics, the method is automatically implementable because it operates on the actual definitions of the protocols, not on some difficult-to-establish justifications of them. What is more, the corresponding tool called SPV (Security Protocol Verifier) has been developed. Another salient point of this approach is that it is justification-oriented instead of falsification-oriented, i.e. finding bugs in protocols.
This page was built for publication: Knowledge structure approach to verification of authentication protocols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q866176)
