- should write down stuff about the other tools, look at the stuff that cites korg
- soundness before implementation
- design, proofs, implementation
- usage before case studies?
- talk about *why* we make the split between design stuff and like, others
- look at the spin trace! it did this and this and this!
- "supported attacker models" should be go before like, the custom attacker models
- usage and case studies? or usage goes in design?

The asynchronous channel automata