Modeling and Verification of Privacy Enhancing Protocols
Contribuinte(s) |
Breitman, Karin Cavalcanti, Ana |
---|---|
Data(s) |
09/12/2009
|
Resumo |
Privacy enhancing protocols (PEPs) are a family of protocols that allow secure exchange and management of sensitive user information. They are important in preserving users’ privacy in today’s open environment. Proof of the correctness of PEPs is necessary before they can be deployed. However, the traditional provable security approach, though well established for verifying cryptographic primitives, is not applicable to PEPs. We apply the formal method of Coloured Petri Nets (CPNs) to construct an executable specification of a representative PEP, namely the Private Information Escrow Bound to Multiple Conditions Protocol (PIEMCP). Formal semantics of the CPN specification allow us to reason about various security properties of PIEMCP using state space analysis techniques. This investigation provides us with preliminary insights for modeling and verification of PEPs in general, demonstrating the benefit of applying the CPN-based formal approach to proving the correctness of PEPs. |
Formato |
application/pdf |
Identificador | |
Publicador |
Springer Berlin / Heidelberg |
Relação |
http://eprints.qut.edu.au/29833/1/c29833.pdf DOI:10.1007/978-3-642-10373-5_7 Suriadi, Suriadi, Ouyang, Chun, Smith, Jason, & Foo, Ernest (2009) Modeling and Verification of Privacy Enhancing Protocols. In Breitman, Karin & Cavalcanti, Ana (Eds.) Modeling and Verification of Privacy Enhancing Protocols, Springer Berlin / Heidelberg, Rio de Janeiro, Brazil, pp. 127-146. |
Direitos |
Copyright 2009 Springer-Verlag Berlin Heidelberg |
Fonte |
Faculty of Science and Technology; School of Information Technology; Information Security Institute; School of Information Systems |
Palavras-Chave | #080203 Computational Logic and Formal Languages #080202 Applied Discrete Mathematics #coloured petri nets #state space analysis #privacy protocols #anonymous credential system #security |
Tipo |
Conference Paper |