Models in this folder:
- `olm-fs-violation.vp`: demonstrating an explicit attack trace for Olm pre-key message secrecy violation in the case pre-keys remain unsigned by the responder
- `olm-fs`: demonstrating Olm with pre-key signing retains secrecy, authentication, and perfect forward secrecy
- `signal.vp`: A reference model from the original [Verifpal paper](https://eprint.iacr.org/2019/971.pdf). Attribution is at the header of the model.