Missions

The postdoc researcher will work on a research project in theoretical computer science in the SPICY team at IRISA (Rennes). This project is about theoretical, and possibly practical, developments on the Squirrel proof assistant for cryptographic protocols. The goal is to extend the underlying logic to better support its higher-order features.

Activités

CCSA (Computationally Complete Symbolic Attacker) logics are used to reason
about cryptographic messages and protocols.
They have emerged from seminal work by Bana and Comon [1] based on first-order
logic, which has gradually evolved towards a higher-order CCSA logic [2],
implemented in the proof assistant Squirrel [3]. A high-level introduction to
CCSA logics and Squirrel may be found in [4].

Cryptographic proofs consider arbitrary attackers within a computationally
limited class, and this limitation must be reflected in several places in our
logics. First, CCSA logics come with a methodology for encoding cryptographic
assumptions, i.e. pairs of indistinguishable cryptographic games, as axiom
schemes. These schemes require -- by various means which are not relevant here
-- that specific subterms are computable by an adversary in the corresponding
game. Since adversaries are probabilistic polynomial-time (PPTIME) Turing
machines, our axioms require verifying that terms are computable in that
sense. Second, the logic features a predicate expressing indistinguishability.
Reasoning about that predicate often involves simple reductions where the
distinguisher is left to compute part of a term, which thus has to be PPTIME
computable.

Squirrel currently relies on very simple criteria for ensuring that terms
are PPTIME-computable. This is sufficient for practical purposes, mainly
because current proofs of protocols rely only on simple, hard-coded recursive
definitions encoding observables during an interaction between an adversary
and a protocol. However, the logic allows complex recursive definitions,
possibly involving higher-order terms, which are starting to be used in more
complex or more experimental proofs. Proving complexity guarantees for such
terms will require more powerful techniques. Another issue is that the
indistinguishability predicate currently only deals with terms of order at
most 1. Extending it to higher-order terms would bring a more uniform and
flexible proof system, but this requires a cost model for higher-order
indistinguishability.

The goal of this postdoc will be to handle these issues at a theoretical
level, and explore new applications in cryptography involving the newly
enriched language. On the one hand, the postdoc will adapt techniques from
implicit complexity and higher-order computability to equip CCSA logics with
a suitable higher-order cost-model and techniques for certifying complexity
bounds. On the other hand, the postdoc will explore how these foundations
may be used to support new applications in Squirrel involving richer
higher-order terms.


Further details

Complexity certification in Squirrel may take various forms, drawing
inspiration from several earlier work, e.g. using sized types [5],
circular proofs [6], functional programming [7] or term orderings [8].
We expect that the more expressive implicit complexity methods will only
become useful for more complex recursive definitions than the ones that
arise in established Squirrel developments. We describe next how these
more complex definitions might arise in cryptographic applications.

When modelling cryptographic protocols, it is often natural to reason about
oracles, which an adversary can call to obtain certain information.
Typically, modelling a hash function may involve giving the adversary access to an
oracle that returns the hash of any message it is called on -- that oracle
can then be idealised into a random oracle that instead returns randomly sampled
outputs, if the hash function is assumed pseudo-random.
In existing Squirrel proofs, such oracles are modelled as sub-processes in the
protocol specification. This modelling style,
inherited from early versions of the logic without higher-order features,
forces oracle calls to explicitly occur in the execution trace
of the protocol, and allows to do basic reasoning in this way.
However, ongoing work involving more complex proofs suggests that it might
be more convenient to model oracles as first-order functions, i.e. lambdas,
that are directly given to the adversary.
This requires reasoning about higher-order constructions when using
cryptographic arguments in the logic, which is currently difficult.
Some experiments have been made in that direction, and we intend to explore
more in-depth how this modelling style can be used. This will require
several extensions to the logic. In particular, we will need to define a higher-order
execution and cost model: what does it mean to give an adversary access
to a higher-order function? to have the adversary return one? if an adversary
calls a higher-order oracle on a first-order function he computed, should
the runtime of that first-order function count towards the adversary's computation time?
Other questions include how to formalise reasoning, within the logic, on the
oracle calls made by the adversary: on paper, some proofs involve for instance
choosing at random one of these calls, which cannot currently be written in the logic.

More generally, it would be interesting to explore higher-order-based alternative
modelling styles for the protocols themselves. In principle, it should be
possible to model protocols as a collection of lambda-terms given to the adversary,
rather than as processes. Stateful protocols would then have to be encoded
using continuations, subject to a linear usage policy. Reasoning about
protocols would then follow an entirely different style, which needs to be
developed from scratch, though it is likely that inspiration can be taken
from more conventional areas of program verification.

## References

[1] Bana, Comon. "A computationally complete symbolic attacker
for equivalence properties." CCS 2014.
[2] Baelde, Koutsos, Lallemand. "A higher-order indistinguishability logic for
cryptographic reasoning." LICS 2023.
[3] Baelde et al. "An interactive prover for protocol verification in the
computational model." S&P 2021.
[4] Baelde et al. The Squirrel Prover and its Logic. SIGLOG newsletter 2024/04.
[5] Avanzini & Dal Lago. Automating Sized-Type Inference for Complexity
Analysis. ICFP'17.
[6] Curzi & Das. Cyclic Implicit Complexity. LICS'22.
[7] Hoffmann, Aehlif & Hofmann. Resource aware ML. CAV'12.
[8] Avanzin, Eguchi & Moser. A New Order-theoretic Characterisation of the
Polytime Computable Functions. APLAS'12.

Compétences

- PhD in Computer Science, ideally in an area related to logic, lambda calculus
- A strong expertise in higher-order languages and theoretical foundations of
computation is necessary.
- Prior knowledge in cryptography is however not
necessary, though it would be valuable.
- The postdoc may or may not use Squirrel to carry out significant proofs,
and they may or may not implement new features in Squirrel. However, the
project is at the intersection of theory and practice, and a candidate with
the ability to work on both aspects would be ideal.

Contexte de travail

This postdoc is part of the HOPR ANR project, and will take place at IRISA.

About the laboratory:
IRISA is currently one of the largest French research laboratories (more than 850 people) in the field of computer science and information technology. Structured into seven scientific departments, IRISA is a center of research excellence with scientific priorities in bioinformatics, system security, new software architectures, virtual reality, big data analysis, and artificial intelligence. Focused on the future of computing and necessarily oriented towards international collaboration, IRISA is at the heart of the digital transition of society and innovation serving cybersecurity, health, environment and ecology, transportation, robotics, energy, culture, and artificial intelligence.

Presentation of IRISA as the host laboratory: https://www.irisa.fr/umr-6074
Presentation of CNRS as the employer: https://www.cnrs.fr/fr/le-cnrs
Presentation of the host team: https://www-spicy.irisa.fr/

Contraintes et risques

Trips to the project partners (e.g. Lille, Paris, Sophia) are planned, for progress meetings.