Guided specification and analysis of a loyalty card system

Laurent Cuennet, Marc Pouly*, Saša Radomirović

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish
Title of host publicationGraMSec 2015: Graphical Models for Security
EditorsSjouke Mauw, Barbara Kordy, Sushil Jajodia
Number of pages16
ISBN (Electronic)978-3-319-29968-6
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Guided specification and analysis of a loyalty card system'. Together they form a unique fingerprint.

Cite this