I would like to learn how to proof the trustworthiness of a protocol based on blockchain, so I'm looking for a simple example. Specifically, I would like to know which formal system is adecuate for the job and how to apply it for the properties of the blockchain.

Taken from Wikipedia's article on BAN logic:

In some cases a protocol was reasoned as secure by the BAN analysis but where in fact insecure. This has led to the abandonment of BAN-family logics in favor of proof methods based on standard invariance reasoning.

Does anybody knows which "proof methods based on standard invariance reasoning" is the author writing about?

  • 3
    That part was recently added by an anonymous user. It doesn't have any source for the claim of the second sentence and the reference added to the first sentence is the result of a workshop which was held over 20 years ago. You might want to reconsider taking that seriously. Edit: I decided that that needs at least one more "citation needed" tag and added it.
    – UTF-8
    Commented Jan 1, 2017 at 9:29
  • Did you find any answer for this? Do they really abandon BAN-family logics ? Commented Mar 23, 2020 at 15:56


Browse other questions tagged or ask your own question.