JCJC SIMI 2 - JCJC - SIMI 2 - Science informatique et applications

Verification of Indistinguishability Properties – VIP

Verification of Indistinguishability Properties

1. Modelling protocols and their privacy properties.<br />2. Algorithms for verifying equivalence-based properties.<br />3. Modularity issues.<br />

Analysis of privacy-type properties

The Internet is a large common space, and it is essential to obtain as much confidence as possible in the correctness of the applications that we use to secure our data and our transactions. Because security protocols are notoriously difficult to design and analyse, formal verification techniques are extremely important. However, nearly all the studies do not allow one to analyse privacy-type properties that play an important role in many modern applications.

The novel part of this project is to formally analyse modern applications in
which privacy plays an important role. Many applications having an important
societal impact are concerned by privacy, e.g. electronic voting, safety
critical applications in vehicular ad hoc networks, routing protocols in
mobile ad hoc networks, or RFID tags that are now embedded in many devices.

Some recent studies have revealed the existence of a flaw in the French implementation of the BAC protocol, which means that anyone carrying a French e-passport can be physically
traced.

We plan to develop new techniques to analyze security protocols used in smartphones.

The scientific publications are available on the web site of the project.


The Internet is a large common space, accessible to everyone around
the world. As in any public space, people should
take appropriate precautions to protect themselves against fraudulent people and processes.
It is therefore essential to obtain as much confidence as possible in
the correctness of the applications that we use.

Because security protocols are notoriously difficult to design and analyse, formal verification techniques
are extremely important.
Formal verification of security protocols has known significant
success during the two last decades.
The techniques
have become mature and several tools for protocol verification are
nowadays available.
However, nearly all studies focus on trace-based security properties (secrecy, authentication, ...),
and thus do not allow one to
analyse privacy-type properties that play an important role in many modern applications.


Modelling protocols and their privacy properties.
---------------------------------------------------------------------------

We came to the study of privacy-type properties a few years ago through the electronic voting
application. Even for
this particular application the concept of privacy represents formally
several security properties.
Actually, privacy is a general requirement that has also been recently
studied in the context of RFID protocols
leading again to several definitions (different from those obtained in
electronic voting).
For many applications such as routing
protocols or location-based services for
vehicular ad hoc networks (e.g. e-toll collection,
``pay-as-you-go'' insurance, ...),
formal definitions of privacy are still missing.


Algorithms for verifying equivalence-based properties.
------------------------------------------------------------------------------------
While algorithms and efficient tools already exist for trace-based security
properties, there are still few results to analyse privacy-type
properties. The existing procedures are actually quite
limited. Moreover, our target applications have some specificities
that can not be expressed in current models.
Lastly, we may want to consider a different intruder model or
express our privacy definitions relying on different notions of
equivalence (e.g. trace equivalence, observational equivalence).

To the best of our knowledge,
the only verification tool that is able to check equivalence
is the ProVerif tool. However, we have already
observed that the approximations used in ProVerif are not suited for
the privacy properties we wish to verify.
Moreover, ProVerif is not well-suited to analyse trace equivalence that
seems however to be the right notion in some applications.

Other techniques to decide equivalence-based properties have been
proposed, but either they are not effective
or the implementation does not scale up well to deal with even rather small
processes. Moreover, in order to deal with our target applications,
it seems necessary to enlarge the scope
of the method to a larger class of processes.


Modularity issues.
---------------------------
One of the task of the project is focused at proposing modular
techniques in two main directions. First, we would like to combine
the decision procedures that we will obtain for various cryptographic
primitives.
Secondly, regarding protocol composition,
it is well-known that composition works when the protocols do not share
secrets. However, there is no result allowing us to derive some
interesting results when the processes rely on some shared secrets
such as long term keys.
This kind of composition results will be very useful. For instance, this
could allow us to establish privacy in presence of two honest voters or
untraceability in presence of two different tags, and to
obtain guarantee in a setting that involves an
arbitrary number of voters or tags.


Project coordination

Stéphanie DELAUNE (CNRS - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR EST) – delaune@lsv.ens-cachan.fr

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

LSV CNRS - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR EST

Help of the ANR 200,408 euros
Beginning and duration of the scientific project: - 48 Months

Useful links

Explorez notre base de projets financés

 

 

ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter