[ivan-gavran]

This is a simple fix to the problem described in Issue #1 . It includes:

• an honest run in SimpleAuthDemo that witnesses whether or not the done event happened
• a fix, which itself consists of two parts: 1) change of the order; 2) change of how sa was parsed. It was previously treated as String, but the responder sends it as symbolic bytes.

[ivan-gavran]

Ideally, I would like to include a theorem (not only a debug run) that would have the claim that the check would be successful. As it seems now (I have just started exploring, so I may be wrong), the main theorem says that
if therre is a successful done event, there must have been a prior start event.
What would be a best practice theorem that would establish that there indeed has to be a done event? Could you guide me on how to approach this?