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.
Document Type: Research Article
Affiliations: Department of Computer Science, University of Liverpool, Liverpool, United Kingdom
Publication date: 01 October 2004
- Information for Authors
- Subscribe to this Title
- Ingenta Connect is not responsible for the content or availability of external websites
- Access Key
- Free content
- Partial Free content
- New content
- Open access content
- Partial Open access content
- Subscribed content
- Partial Subscribed content
- Free trial content