Guided Specification and Analysis of a Loyalty Card System

Laurent Cuennet, Marc Pouly (Lead / Corresponding author), Saša Radomirović

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 publicationGraphical Models for Security
Subtitle of host publicationSecond International Workshop, GraMSec 2015 Verona, Italy, July 13, 2015 Revised Selected Papers
EditorsSjouke Mauw, Barbara Kordy, Sushil Jajodia
PublisherSpringer International Publishing
Number of pages16
ISBN (Electronic)9783319299686
ISBN (Print)9783319299679
Publication statusPublished - 2016
EventSecond International Workshop on Graphical Models for Security - University of Verona, Department of Computer Science, Verona, Italy
Duration: 13 Jul 201513 Jul 2015 (Link to Conference website)

Publication series

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


WorkshopSecond International Workshop on Graphical Models for Security
Abbreviated titleGraMSec 2015
Internet address

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