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?