Currently no known bugs.
Better error messages.
Provide a syntax for opponents (this is just a matter of allowing opponents to hijack sessions).
Allow networks to be executed, to produce message-passing diagrams.
Add a LaTeX / HTML pretty printer.
Extend the checker to distinguish between short- and long-term keys and deal with key compromise (as described in our CONCUR'05 papers).
Find a way to allow a single nonce to be used multiple times within the same protocol, if confusion is ruled out by the message context. This would allow us to obtain a one-to-one correspondence for the acknowledgment in Carlsen.
Add proper Javadoc comments.
Update remaining examples from Cryptyc 1.1 to Cryptyc 1.2 and protocol-independent key types.
Look at examples with key compromise.
Document the Cryptyc surface syntax properly.
Cryptyc implementation Copyright © 2001-2004, Alan Jeffrey and Christian Haack