Abstract
We apply a graphical model to develop a digital loyalty program protocol specifically tailored to small shops with no professional or third-party-provided infrastructure. The graphical model allows us to capture assumptions on the environment the protocol is running in, such as capabilities of agents, available channels and their security properties. Moreover, the model serves as a manual tool to quickly rule out insecure protocol designs and to focus on improving promising designs. We illustrate this by a step-wise improvement of a crude but commercially used protocol to finally derive a light-weight and scalable security protocol with proved security properties and many appealing features for practical use.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6–15 (1996)
ECB (European Central Bank). Virtual currency schemes, October 2012
Basin, D., Radomirović, S., Schläpfer, M.: A complete characterization of secure human-server communication. In: 28th IEEE Computer Security Foundations Symposium (CSF 2015), pp. 199–213. IEEE Computer Society (2015). http://www.infsec.ethz.ch/research/projects/hisp.html
Blanco-Justicia, A., Domingo-Ferrer, J.: Privacy-preserving loyalty programs (2014). CoRR, abs/1411.3961
Canard, S., Gouget, A., Hufschmitt, E.: A handy multi-coupon system. In: Zhou, J., Yung, M., Bao, F. (eds.) ACNS 2006. LNCS, vol. 3989, pp. 66–81. Springer, Heidelberg (2006)
Chaum, D.: Blind signatures for untraceable payments. In: Chaum, D., Rivest, R.L., Sherman, A.T. (eds.) Advances in Cryptology, pp. 199–203. Springer, New York (1983)
Chen, L., Enzmann, M., Sadeghi, A.-R., Schneider, M., Steiner, M.: A privacy-protecting coupon system. In: S. Patrick, A., Yung, M. (eds.) FC 2005. LNCS, vol. 3570, pp. 93–108. Springer, Heidelberg (2005)
Cuennet, L.: Security protocols for loyalty card systems on mobile devices. Master’s thesis, University Of Fribourg (2014)
Cumby, C., Fano, A., Ghani, R., Krema, M.: Predicting customer shopping lists from point-of-sale purchase data. In: Proceedings of the Tenth ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pp. 402–409. ACM (2004)
Dominikus, S., Aignerc, M.: mCoupons: an application for near field communication (NFC). In: 2007 21st International Conference on Advanced Information Networking and Applications Workshops, AINAW 2007, vol. 2, pp. 421–428. IEEE (2007)
Enzmann, M., Fischlin, M., Schneider, M.: A privacy-friendly loyalty system based on discrete logarithms over elliptic curves. In: Juels, A. (ed.) FC 2004. LNCS, vol. 3110, pp. 24–38. Springer, Heidelberg (2004)
Maurer, U.M., Schmid, P.E.: A calculus for secure channel establishment in open networks. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 173–192. Springer, Heidelberg (1994)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013)
Pfitzmann, B., Waidner, M.: Properties of payment systems: general definiton sketch and classification (1996)
Quaresma, J.: On building secure communication systems. Ph.D. thesis, DTU Compute, Technical University of Denmark (2013)
Quaresma, J., Probst, C.W., Nielson, F.: The guided system development framework: modeling and verifying communication systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 509–523. Springer, Heidelberg (2014)
Radomirović, S.: Tamarin specification files for two loyalty points protocols (2015). http://www.infsec.ethz.ch/research/projects/hisp.html
Sadeghi, A.-R., Schneider, M.: Electronic payment systems. In: Becker, E., Buhse, W., Günnewig, D., Rump, N. (eds.) Digital Rights Management. LNCS, vol. 2770, pp. 113–137. Springer, Heidelberg (2003)
Schoenmakers, B.: Basic security of the ecash payment system. In: Preneel, B., Rijmen, V. (eds.) Computer Security and Industrial Cryptography: State of the Art and Evolution, pp. 342–356. Springer Verlag, New York (1998)
Song, D., Perrig, A., Phan, D.: AGVI - automatic generation, verification, and implementation of security protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 241–245. Springer, Heidelberg (2001)
Sprankel, S: Technical basis of digital currencies (2013)
Sprenger, C., Basin, D.: Developing security protocols by refinement. In: 7th ACM Conference on Computer and Communications Security (CCS 2010), 4–8 October 2010, Chicago, USA, pp. 361–374. ACM (2010)
von Solms, S., Naccache, D.: On blind signatures and perfect crimes. Comput. Secur. 11, 581–583 (1992)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Cuennet, L., Pouly, M., Radomirović, S. (2016). Guided Specification and Analysis of a Loyalty Card System. In: Mauw, S., Kordy, B., Jajodia, S. (eds) Graphical Models for Security. GraMSec 2015. Lecture Notes in Computer Science(), vol 9390. Springer, Cham. https://doi.org/10.1007/978-3-319-29968-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-29968-6_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29967-9
Online ISBN: 978-3-319-29968-6
eBook Packages: Computer ScienceComputer Science (R0)