Stéphanie Delaune. Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction, (FSCD'18), LIPIcs 108, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Oxford, UK, 2018.
Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. For example, passports are no more pure paper documents. Instead, they contain a chip that stores additional information such as pictures and fingerprints of their holder. In order to ensure privacy, these chips include a mechanism, i.e. a cryptographic protocol, that does not letthe passport disclose private information to external users except theintended terminal. This is just a single example but of course privacy appears in many other contexts such as RFIDs technologies or electronic voting.Formal methods have been successfully applied to automatically analyse traditional protocols and discover their flaws. Privacy-type securityproperties (e.g. anonymity, unlinkability, vote secrecy, łdots) are expressed relying on a notion of behaviouralequivalence, and are actually more difficult to analyse thanconfidentiality and authentication properties.We will discuss some recent advances that have been done to analyse automatically equivalence-based security properties, and we will review some issuesthat remain to be solved in this field.
@inproceedings{Delaune-fscd18,
abstract={Cryptographic protocols aim at securing communications over insecure
networks such as the Internet, where dishonest users may listen to
communications and interfere with them. For example, passports are no more
pure paper documents. Instead, they contain a chip that stores additional information
such as pictures and fingerprints of their holder. In order to ensure privacy, these chips
include a mechanism, i.e. a cryptographic protocol, that does not let
the passport disclose private information to external users except the
intended terminal.
This is just a single example but of course privacy appears in many other contexts
such as RFIDs technologies or electronic voting.
Formal methods have been successfully applied to automatically analyse
traditional protocols and discover their flaws. Privacy-type security
properties (e.g. anonymity, unlinkability, vote secrecy, \ldots) are expressed relying on a notion of behavioural
equivalence, and are actually more difficult to analyse than
confidentiality and authentication properties.
We will discuss some recent advances that have been done to analyse automatically
equivalence-based security properties, and we will review some issues
that remain to be solved in this field.},
author = {Delaune, St{\'e}phanie},
title = {Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)},
booktitle = {3rd International Conference on Formal Structures for Computation
and Deduction, ({FSCD}'18)},
address = {Oxford, {UK}},
year = {2018},
editor = {H{\'{e}}l{\`{e}}ne Kirchner},
series = {LIPIcs},
volume = {108},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
}