Exploiting Symmetries When Proving Equivalence Properties for Security Protocols
Vincent Cheval, Steve Kremer, Itsaka Rakotonirina · 2019
Verification of privacy-type properties for cryptographic protocols in an active adversarial environment, modelled as a behavioural equivalence in concurrent-process calculi, exhibits a high computational complexity. While undecidable in general, for some classes of common cryptographic primitives the problem is coNEXP-complete when the number of honest participants is bounded.