Post-Compromise Security (PCS) is a property of secure-channel establishment schemes which limits the security breach of an
adversary that has compromised one of the endpoints to a certain number of messages, after which the channel heals. An attractive
property, especially in view of Snowden's revelation of mass-surveillance, PCS features in prominent messaging protocols
such as Signal.

In this thesis, we first present two variants of Signal which improve the PCS property. Moreover, by viewing PCS as a spectrum, rather than
a binary property which schemes might or might not have, in the second part of the thesis we introduce a framework for quantifying and
comparing PCS security, with respect to a broad taxonomy of adversaries. The generality and flexibility of our approach allows us
to model the healing speed of a broad class of protocols, including Signal and our variant SAMURAI, but also an identity-based messaging
protocol named SAID, and even a composition of 5G handover protocols. We also apply the results obtained for this last example in
order to provide a quick fix, which massively improves its post-compromise security.

The last part of this thesis is dedicated to the question of deep attestation in virtualized infrastructures.  Deep attestation is a
particular case of remote attestation, i.e., verifying the integrity of a platform in the presence of a remote server. We focus on the
remote attestation of hypervisors and their hosted virtual machines (VM), for which two solutions are currently supported by ETSI
(European Telecommunications Standards Institute). The first is single-channel attestation, requiring for each VM an attestation of
that VM and the underlying hypervisor through the physical TPM. The second, multi-channel attestation, allows to attest VMs via virtual
TPMs and separately from the hypervisor -- this is faster and requires less overall attestations, but the server cannot verify the link
between VM and hypervisor attestations, which is naturally available for single-channel attestation.
    
We design a new approach which provides linked remote attestation which achieves the best of both worlds: we benefit from the efficiency
of multi-channel attestation while simultaneously allowing attestations to be linked. Moreover, we formalize a security model for
deep attestation and prove the security of our approach.  Our contribution is agnostic of the precise underlying secure component
(which could be instantiated as a TPM or something equivalent) and can be of independent interest.

Jury:

• Pascal LAFOURCADE, LIMOS Université Clermont Auvergne (directeur de thèse);
• Cristina ONETE, XLIM Université de Limoges (directrice de thèse);
• Benjamin NGUYEN, LIFO INSA Centre Val de Loire (Rapporteur);
• Melek ÖNEN, EURECOM Sophia-Antipolis (Rapporteure);
• Karthikeyan BHARGAVAN, INRIA de Paris (Examinateur);
• Jean-Guillaume DUMAS, LJK Université Grenoble Alpes (Examinateur);
• David POINTCHEVAL, INRIA, PSL, ENS Paris (Examinateur);
• Olivier SANDERS, Orange Labs Cesson-Sevigne (Examinateur);

Up-to-date information about the defence can be found at my personal website:https://perso.limos.fr/~leorober/