3 ms·

Thanks for the feedback. As for #3, unfortunately we don't currently have plans to publish a formal proof (we're building a product). Some of our internal docu

• Taek 10y ago
  You will probably find it valuable to write that proof. Sometimes an edge case pops up or you end up proving that it doesn't work as expected. I've done this a few times in my work. Unless you already have it but don't plan to publish, which seems a little odd to me. I get that you want readable documentation, but at least you could link to it somewhere for people who go digging.
  • unboxed_type 10y ago
    Well personally I would rather suggest to write a model, not a rigorous proof. A formal proof of any real protocol is both long and tedious journey; production guys will hardly find it useful thing to do. On the other hand a logical model can be encoded in a rather short amount of time by someone who is doing it periodically. This hypothetical guy could benefit from this activity by co-authoring the paper. Original authors would benefit from it by reinforcing both the protocol and the paper.