Automatically generated tamper evident data structures, or Merkle things for free!

[Shaul]

If you found this interesting, you may also be interested in this post about formally proving Merkle data structures

Our new formal methods paper on Merkle trees & co

@Andreas_Lochbihler and myself have a new paper on formally modelling Merkle trees and similar so-called “authenticated data structures” in the theorem prover Isabelle. Such structures allow several systems to ensure that they’re talking about the same structure, even if everyone has only a part of the structure. Yes but why? The reason for the exercise are DAML transactions; there, you can have parties and participant nodes that only see a part of the transaction (their “projections”), but we …