Manual
The manual is available: mck.pdf.gz
Examples
The following are some examples that we have studied using the system. The distribution contains a number of variants of these examples.
A Robot with a Noisy Position Sensor
This is an example of verifying the implementation of a knowledge based program, in the sense of Fagin,
Halpern, Moses and Vardi, Reasoning about Knowledge, MIT Press, 1995. The example is drawn from this
book,
and is a discretized version of an example of Brafman et al, JACM 97.
(MCK input file for the Robot)
(Download)
One time Pad
This tests the security of the One Time Pad cipher on a single bit.
(MCK input file for the one time pad)
(Download)
Increasing Mutual Knowledge in a Message Passing System
An example from R. van der Meyden, Common Knowledge and Update in Finite Environments, Information and
Computation, 1998 that shows that in a message passing system with bounded but uncertain delivery times,
the
level of mutual knowledge about message delivery increases with time.
(MCK input file for the message passing system)
(Download)
The Dining Cryptographers
The dining cryptographers protocol is a protocol for anonymous broadcast. For details see: D. Chaum The
dining cryptographers problem: unconditional sender and recipient untraceability, Journal of
Cryptology(1),
1988.
MCK input file for the protocol:
dc_agent_protocol
(Download)
An environment description setting up the protocol for 3 cryptographers sitting around a table:
dc_environment3
(Download)
A probabilistic version, with various probabilistic formulations of anonymity:
prob_dc3
(Download)
A variant of the above probabilistic version, showing the effect of biased coins:
prob_dc3_variant
(Download)
Rivest's Oblivious Transfer Protocol
A protocol for oblivious transfer, with a trusted third party who does not need to be online at the time
of
the transfer. From Ronald L. Rivest. Unconditionally secure commitment and oblivious transfer schemes
using
private channels and a trusted initializer. (Unpublished report, available
here).
(MCK input file for Rivests protocol)
(Download)
(A probabilistic version)
(Download)
Two Phase Commit
Two phase commit is a solution to the atomic commitment problem tpc3.
(MCK input file for the Two Phase Commit)
(Download)
MCK MoChArt 2010 Examples
This package contains python scripts used to generate MCK scripts for the experiments whose results have
been reported in the paper:
Improved bounded model checking for a fair branching-time
temporal epistemic logic.
(Download)