Formal Analysis of E-Cash Protocols

Jannik Dreier, Ali Kassem, Pascal Lafourcade

2015

Abstract

Electronic cash (e-cash) aims at achieving client privacy at payment, similar to real cash. Several security protocols have been proposed to ensure privacy in e-cash, as well as the necessary unforgery properties. In this paper, we propose a formal framework to define, analyze, and verify security properties of e-cash systems. To this end, we model e-cash systems in the applied p-calculus, and we define two client privacy properties and three properties to prevent forgery. Finally, we apply our definitions to an e-cash protocol from the literature proposed by Chaum et al., which has two variants and a real implementation based on it. Using ProVerif, we demonstrate that our framework is suitable for an automated analysis of this protocol.

Paper Citation

in Harvard Style

Dreier J., Kassem A. and Lafourcade P. (2015). Formal Analysis of E-Cash Protocols . In Proceedings of the 12th International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2015) ISBN 978-989-758-117-5, pages 65-75. DOI: 10.5220/0005544500650075

in Bibtex Style

@conference{secrypt15,
author={Jannik Dreier and Ali Kassem and Pascal Lafourcade},
title={Formal Analysis of E-Cash Protocols},
booktitle={Proceedings of the 12th International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2015)},
year={2015},
pages={65-75},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005544500650075},
isbn={978-989-758-117-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 12th International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2015)
TI - Formal Analysis of E-Cash Protocols
SN - 978-989-758-117-5
AU - Dreier J.
AU - Kassem A.
AU - Lafourcade P.
PY - 2015
SP - 65
EP - 75
DO - 10.5220/0005544500650075