Thanks for leandy, it's a great work.
As I was going through the SimpleAuth.lean example, I noticed a problem in initiator_check.
While the responder sends (na, a), they are parsed in the initiator_check as (a, na).
Thus, in an honest execution, the done event will never be emitted.
Thanks for leandy, it's a great work.
As I was going through the
SimpleAuth.leanexample, I noticed a problem ininitiator_check.While the responder sends
(na, a), they are parsed in theinitiator_checkas(a, na).Thus, in an honest execution, the
doneevent will never be emitted.