I wrote down a rough outline of a security game definition, and a clearer description of the algorithms with pseudocode.
https://docs.google.com/document/d/12xl5eRtoE0uISUX188jnmGSb-bwG4yXByRBbdr2r97A

I also wrote out an implementation in OCaml of the key operations (using the Lambda-auth language/compiler I made especially for this sort of thing), for building the hash-value highway and creating/verifying the compact SPV proofs. It compiles but I haven't tested it, I plan to use it to create some illustrative graphs.
https://gist.github.com/amiller/9635632

Any of the above could be totally broken, but hopefully this gets the conversation moving along more concretely!