Note: this project is not completely finished. The derivation results might be wrong, the output would first need to be made clearer to enable further developement/debugging. See my blog post (or here) for an explanation and a guide through the code structure.
The best way to see what is happening is to run the tests.
sbt lets you run some specific test file only, for example the one derivating the man-in-the-middle attack on the Needham Schroeder protocol.
sbt test
sbt 'testOnly *NeedhamSchroeder'
sbt 'testOnly *NeedhamSchroederLowe'