Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Holtzman, D.H.: Privacy Lost. Jossey-Bass (2006)
WP 14.1: PRIME (Privacy and Identity Management for Europe) - Framework V3 (March 2008)
Team, T.A.: AVISPA v1.1 User Manual. Information Society Technologies Programme (June 2006), http://avispa-project.org/
Al-Azzoni, I., Down, D.G., Khedri, R.: Modeling and verification of cryptographic protocols using coloured petri nets and design/cpn. Nordic Journal of Computing 12(3), 201–228 (2005)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. J. Comput. Secur. 13(3), 347–390 (2005)
Koblitz, N., Menezes, A.: Another look at provable security. J. Cryptology 20(1), 3–37 (2007)
Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use, 2nd edn. Monographs in Theoretical Computer Science, vol. 1. Springer, Berlin (1997)
Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)
Gilmore, S.: Programming in standard ml 1997: A tutorial introduction. Technical report, The University of Edinburgh (1997)
Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. STTT 9(3-4), 213–254 (2007)
Suriadi, S., Foo, E., Smith, J.: Private information escrow bound to multiple conditions. Technical report, Information Security Institute - Queensland University of Technology (2008), http://eprints.qut.edu.au/17763/1/c17763.pdf
Suriadi, S., Foo, E., Josang, A.: A user-centric federated single sign-on system. Journal of Network and Computer Applications 32(2), 388–401 (2009)
Suriadi, S., Foo, E., Smith, J.: A user-centric protocol for conditional anonymity revocation. In: Furnell, S.M., Katsikas, S.K., Lioy, A. (eds.) TrustBus 2008. LNCS, vol. 5185, pp. 185–194. Springer, Heidelberg (2008)
Suriadi, S., Ouyang, C., Smith, J., Foo, E.: Modeling and verification of privacy enhancing security protocols. Technical report, ISI, Queensland University of Technology (April 2009) http://eprints.qut.edu.au/20088/ .
McCune, J.M., Parno, B., Perrig, A., Reiter, M.K., Isozaki, H.: Flicker: an execution infrastructure for TCB minimization. In: Sventek, J.S., Hand, S. (eds.) EuroSys, pp. 315–328. ACM, New York (2008)
Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
van der Aalst, W.: Pi calculus versus petri nets: Let us eat humble pie rather than further inflate the pi hype. In: BPTrends, pp. 1–11 (May 2005)
Christensen, S., Mortensen, K.H.: Design/CPN ASK-CTL Manual - Version 0.9. University of Aarhus, Aarhus C, Denmark (1996)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)
Meadows, C.: Open issues in formal methods for cryptographic protocol analysis. In: DISCEX 2000, pp. 237–250. IEEE Computer Society Press, Los Alamitos (2000)
Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Baeten, J.C.M.: A brief history of process algebra. Theor. Comput. Sci. 335(2-3), 131–146 (2005)
Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, Cambridge (1999)
Cremers, C.J.: The scyther tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, pp. 82–96 (June 2001)
Tatebayashi, M., Matsuzaki, N., Newman Jr., D.B.: Key distribution protocol for digital mobile communication systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324–334. Springer, Heidelberg (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Suriadi, S., Ouyang, C., Smith, J., Foo, E. (2009). Modeling and Verification of Privacy Enhancing Protocols. In: Breitman, K., Cavalcanti, A. (eds) Formal Methods and Software Engineering. ICFEM 2009. Lecture Notes in Computer Science, vol 5885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10373-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-10373-5_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10372-8
Online ISBN: 978-3-642-10373-5
eBook Packages: Computer ScienceComputer Science (R0)