Sciweavers

Share
AAI
2004

Model Checking A Knowledge Exchange Scenario

9 years 11 months ago
Model Checking A Knowledge Exchange Scenario
We are interested in applying model checking techniques to the verification of communication protocols which 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 secure 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 -- in our case, SPIN.
Sieuwert van Otterloo, Wiebe Der, Michael Wooldrid
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2004
Where AAI
Authors Sieuwert van Otterloo, Wiebe Der, Michael Wooldridge
Comments (0)
books