Can epistemic logic be useful for secure payments and secure communication? The following article answers this question positively, using BAN logic:

N. Agray, W. van der Hoek, and E.P. de Vink, On BAN logics for industrial security protocols, From Theory to Practice in Multi-Agent Systems, B. Dunin-Kęplicz and E. Nawarecki (eds.), LNAI 2296, 2002, pp. 29-38.

However, Wouter Teepe has shown that BAN logic is problematic: it can prove things that are highly debatable. He prefers to use GNY logic, see Reconciling Information Exchange and Confidentiality.

For a project, you could for example simulate an authentication protocol. As an example, you could make a GNY analysis of OpenSSH or GnuPG. This can be use as a first step towards a simulation in which the relations between the agents, the relations between the agents and the keys, and the relations among the keys are clearly represented.

As several people have noted, the Logics Workbench can hardly be called user-friendly. Also, a module for S5n is missing. It would be worthwhile to have a good, user-friendly theorem prover for S5n, not necessarily based on the same proof method (sequent calculus) as the LWB. For this project, a good knowledge of tableau proofs, as used in the course on Advanced Logic, would be useful. You may ask Rineke Verbrugge for relevant literature.

One can model well-known knowledge games such as bridge, liar's dice/blufpoker, or Cluedo (see Hans van Ditmarsch' Ph.D. thesis). Warning: even for small versions of these games, an epistemic analysis is often extremely difficult.

In the past, students have adapted Masterminds and Zeeslag in such a way that players also have to answer the questions (or "guesses") they ask the other player, with respect to their own position. Thus, they need to devise questions that give as little as possible information away about their own position, while attaining as much as possible information about the other's position. One can do such an adaptation for other asymmetric guessing games such as 'galgje' or 'hangman'. It would be interesting to make an implementation of your game, along with an analysis of good strategies.

This project is based on the following variant of Freudenthal's Sum and Product puzzle:

A says to S and P: "I have chosen two integers x, y such that 1 < x < y and 30 < x * y < 60. In a moment, I will inform S only of x + y, and P only of x * y. These announcements remain private. You are required to determine the pair (x, y). The two of you, S and P, are perfect both at epistemic logic and at arithmetic".

He acts as said. The following conversation now takes place:

P says: "I do not know it."

S says: "I already knew you didn't."

P says: "I still have two possible pairs left."

S says: "I now know the pair."

Determine the pair (x, y).

It would be interesting to build a program that gives, for every step in the puzzle story, the individual knowledge and common knowledge of S and P. For example, one could model the puzzle in DEMO. For example see De Sam & Pro Website and SAM & Pro - Common Knowledge for projects on Freudenthal's "Sam & Pro" puzzle, as given on the page Projectuitwerkingen.

You may also have a look at: H.P. van Ditmarsch, J. Ruan, L.C. Verbrugge, Sum and Product in Dynamic Epistemic Logic. Journal of Logic and Computation 18(4): 563-588, 2007.