Modeling and verification of privacy enhancing security protocols
Suriadi Suriadi, Chun Ouyang, Jason Smith, Ernest Foo · 2009
Privacy enhancing security protocols (PESPs) are a family of protocols that allow secure exchange of sensitive user information. They are important in preserving users privacy in today’s open environment. Like other security systems, proof of the correctness of PESPs is necessary before they can be deployed. However, the traditional provable security approach, though well established for verifying cryptographic primitives, is not applicable to PESPs. We apply the formal method of Coloured Petri Nets (CPNs) to construct an executable specification of a representative PESP, namely the Private Information Escrow Bound to Multiple Conditions Protocol (PIEMCP). Formal semantics of the CPN specification allows us to reason about various security properties of PIEMCP using state space techniques. This investigation has also led us to a number of approaches for modeling and verification of PESPs in general, demonstrating the benefit of applying CPN-based formal approach to proving the correctness of security protocols.