The HSMs are converted to Firebase security rules.
The theorem proover is used to verify somewhat arbitrary higher level properties
So for item trade* I was specifying the that no new items could be introduced (dupe bugs) or removed from the system, and that a player could never get stuck in a state they could never leave (deadlock). The HSM abstraction is just a useful notation for developing such protocols, though the formal verification actually operated on the Firebase security rule level.
So for item trade* I was specifying the that no new items could be introduced (dupe bugs) or removed from the system, and that a player could never get stuck in a state they could never leave (deadlock). The HSM abstraction is just a useful notation for developing such protocols, though the formal verification actually operated on the Firebase security rule level.
* https://github.com/tomlarkworthy/firesafe/wiki/Send-Item
EDIT: reply to oggy's child question as I can't reply underneath.
The actual spec prooving bit is secret sauce territory until I work out what the future holds for this project.