ProVerif Scripts

reach.pv: Example of Reachability Assertions

corr.pv: Example of Correspondence Assertions

obsv_neq.pv: Example of Observational Equivalence Failing

obsv_eq.pv: Example of Observational Equivalence Passing

handshake.pv: Naive Server-Client Authentication

handshake_fix.pv: Fixed Server-Client Authentication

JCJ_t.pv: pv implementation of soundness model, ZK proof model is not included

JCJ_soundness.pi: pi implementation of soundness model, ZK proof model included

JCJ_soundness_noPET.pi: tallier does not perform Plain-text Equivalence test (targets Inalterability and Non-reusability properties)

JCJ_coercion2.pi: pi implementation of coercion model for verifying 2nd Condition of Strong-Coercion Resistance