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 responderolm-fs: demonstrating Olm with pre-key signing retains secrecy, authentication, and perfect forward secrecysignal.vp: A reference model from the original Verifpal paper. Attribution is at the header of the model.