MODEL CHECKING A KNOWLEDGE EXCHANGE SCENARIO
We are interested in applying model checking techniques to the verification of communication protocols that require safe communication. Typically, in such scenarios, one desires to demonstrate that one party can reliably communicate information to another party without a third party being able to determine this information. Our approach involves using the modal logic of knowledge, which has only relatively recently been studied in the context of security protocols. We demonstrate our approach by means of a detailed case study: the Russian cards problem. This is an example of a security protocol with nontrivial requirements on the knowledge of the agents involved. Using the Russian cards problem as an example, it is shown how the satisfaction of properties involving knowledge can be verified in a standard model checker, which in our case is SPIN.
No Reference information available - sign in for access.
No Citation information available - sign in for access.
No Supplementary Data.
No Article Media
Document Type: Research Article
Affiliations: Department of Computer Science, University of Liverpool, Liverpool, United Kingdom
Publication date: 2004-10-01