I get that Verifpal is not perfect, doesn't do everything. I have considered switching. However, a significant part of proving the mechanism is having correct definitions for all of the needed primitives. If Verifpal tackles the right, correct definitions of the primitives, that is already a significant step, right? Considering the protocol is not complicated, or trying to be, one might try a less complex solution to start with.
I am not planning to "gloss over" and there is a bigger pictures. But, feel free to make any missed dimensions concrete. (Note, you might want to check some other comments, as I explain a bit more about the device.)
No comments yet.