1 Introduction

In recent messaging applications, protocols are secured with end-to-end encryption to enable secure communication services for their users. Besides security, there are many other characteristics of communication systems. The nature of two-party protocols is that it is asynchronous: the messages should be transmitted regardless of the counterpart being online; the protocols do not have any control over the time that participants send messages; and, the participants change their roles as a sender or a receiver arbitrarily.

Many deployed systems are built with some sort of security guarantees. However, they often struggle with security vulnerabilities due to the internal state compromises that occur through exposures of participants. In order to prevent the attacker from decrypting past communication after an exposure, a state update procedure is applied. Ideally, such updates are done through one-way functions which delete the old states and generate new ones. This guarantees forward secrecy. Additionally, to further prevent the attacker from decrypting future communication, ratcheting is used. This adds some source of randomness in every state update to obtain what is called future secrecy, or backward secrecy, or post-compromise security, or even self-healing.

Formal definitions of ratcheting security given have been recently studied, by Bellare et al. [2], followed by many others subsequent studies [1, 7,8,9,10]. Some of these schemes are key-exchange protocols while others are secure messaging. Since secure ratcheted messaging boils down to secure key exchange, we consider these works as equivalent.

Previous Work. Early ratcheting protocols were suggested in Off-the-Record (OTR) and then Signal [3, 11]. The security of Signal was studied by Cohn-Gordon et al. [5]. Unger et al. [12] surveyed many ratcheting techniques. Alwen et al. [1] formalized the concept of “double ratcheting” from Signal.

Cohn-Gordon et al. [6] proposed a ratcheted protocol at CSF 2016 but requiring synchronized roles. Bellare et al. [2] proposed another protocol at CRYPTO 2017, but unidirectional and without forward secrecy. Poettering and Rösler (PR) [10] designed a protocol with “optimal ” security (in the sense that we know no better security so far), but using a random oracle, and heavy algorithms such as hierarchical identity-based encryption (\(\mathsf {HIBE}\)). Yet, their protocol does not guarantee security against compromised random coins. Jaeger and Stepanovs (JS) [8] proposed a similar protocol with security against compromised random coins: with random coin leakage before usage. Their protocol also requires \(\mathsf {HIBE}\) and a random oracle.

Durak and Vaudenay (\(\mathsf {DV}\)) [7] proposed a protocol with slightly lower securityFootnote 1 but relying on neither \(\mathsf {HIBE}\) nor random oracles. They rely on a public-key cryptosystem, a digital signature scheme, a one-time symmetric encryption scheme, and a collision-resistant hash function. They further show that a unidirectional scheme with post-compromise security implies public-key cryptography, which obviates any hope of having a fully secure protocol solely based on symmetric cryptography. At EUROCRYPT 2019, Jost, Maurer, and Mularczyk (JMM) [9] proposed concurrently and independently a protocol with security between optimal security and the security of the \(\mathsf {DV}\) protocol.Footnote 2 They achieve it even with random coin leakage after usage. Contrarily to other protocols achieving security with corrupted random coins, in their protocol, random coin leakage does not necessarily imply revealing part of the state of the participant. In the same conference, Alwen, Coretti, and Dodis [1] proposed two other ratcheting protocols denoted as ACD and ACD-PK with security against adversarially chosen random coins and immediate decryption. Namely, messages can be decrypted even though some previous messages have not been received yet. The ACD-PK protocol offers a good level of security, although having immediate decryption may lower it a bit as it will be discussed shortly. On the other hand, during a phase when the direction of communication does not change, the ACD protocol is fully based on symmetric cryptography, hence has lower security (in particular, no post-compromise security in this period). However, it is much more efficient. Following the authors of \(\mathsf {ACD}\), we consider Signal and \(\mathsf {ACD}\) as equivalent.

We summarize these results in Table 1. The first four rows are based on \(\mathsf {DV}\) [7, Table 1]. The other rows of the table will be discussed shortly.

Recently, Yan and Vaudenay [13] proposed Encrypt-then-Hash (\(\mathsf {EtH}\)), a simple, natural, and extremely efficient ratchet protocol based on symmetric cryptography only, which provides forward secrecy but not post-compromise security. In short, it replaces the encryption key by its hash after every encryption or decryption, and needs one key for each direction of communication.

We are mostly interested in the \(\mathsf {DV}\) model [7]. It gives a simple description of the \(\mathsf {KIND}\) security and \(\mathsf {FORGE}\) security. The former deals with key indistinguishability where the generated keys are indistinguishable from random strings and the latter states that update messages for ratcheted key exchange are unforgeable. Additionally, they present the notion of \(\mathsf {RECOVER}\)-security which guarantees that participants can no longer accept messages from their counterpart after they receive a forged message. Even though \(\mathsf {FORGE}\) security avoids non-trivial forgeries, there are still (unavoidable) trivial forgeries. They occur when the state of a participant is exposed and the adversary decides to impersonate him. With \(\mathsf {RECOVER}\) security, when an adversary impersonates someone (say Bob), the impersonated participant is out and can no longer communicate with the counterpart (say Alice). It does not mean to bother participants but rather work for their benefit. Indeed, this security notion guarantees that the attack is eventually detected by Bob if he is still alive. If the protocol has a way to resume secure communication based on an explicit action from the users, this property is particularly appealing.

What makes the \(\mathsf {DV}\) model simple is that all technicalities are hidden in a cleanness notion which eliminates trivial attack strategies. The adversary can only win when the attack scenario trace is “clean”. This model makes it easy to consider several cleanness notions, specifically for hybrid protocols. The difficulty is perhaps to provide an exhaustive list of criteria for attacks to be clean.

Our Contributions. We start with formally and explicitly defining a notion of security awareness in which the users detect active attacks by realizing they can no longer communicate; users can be confident that nothing in the protocol can compromise the confidentiality of an acknowledged message if it did not leak before; and users can deduce from an incoming message which of the messages they sent have been delivered when the incoming message was formed.

More concretely, we elaborate on the \(\mathsf {RECOVER}\) security to offer optimal security awareness. We start by defining a new notion called \(\mathsf {s\text {-}RECOVER}\). We make sure that not only is a receiver of a forgery no longer able to receive genuine messages via \(\mathsf {r\text {-}RECOVER}\)-security but he can no longer send a message to his counterpart either via \(\mathsf {s\text {-}RECOVER}\)-security. The \(\mathsf {r\text {-}RECOVER}\) security is equal to \(\mathsf {RECOVER}\) security of the \(\mathsf {DV}\) protocol. Both \(\mathsf {r\text {-}RECOVER}\) and \(\mathsf {s\text {-}RECOVER}\) notions imply that reception of a genuine message offers a strong guarantee of having no forgery in the past: after an active attack ended, participants realize they can no longer communicate. Our security-awareness notion makes also explicit that the receiver of a message can deduce (in absence of a forgery) which of his messages have been seen by his counterpart (which we call an acknowledgment extractor). Hence, each sent message implicitly carries an acknowledgment for all received messages. Finally, what we want from the history of receive/send messages and exposures of a participant is the ability to deduce which message remains private (or “clean”). We call it a cleanness extractor.

Then, we give another generic construction to compose “any” two protocols with different security levels to allow a sender to select which security level to use. By composing a strongly secure protocol (such as \(\mathsf {PR}\), \(\mathsf {JS}\), \(\mathsf {JMM}\), \(\mathsf {DV}\)) with a lighter and weakly secure one (such as \(\mathsf {EtH}\) [13], which is solely based on symmetric cryptography), we obtain the notion of ratchet on-demand. When the ratcheting becomes infrequent, we obtain the excellent software performances of \(\mathsf {EtH}\) as we will show in our implementation results. Hybrid constructions already exist, like Signal/\(\mathsf {ACD}\). However, they offer no control on the choice of the protocol to be used. Instead, they ratchet if (and only if) the direction of communication alternates.

We find that there would be an advantage to offer more fine grained flexibility. The decision to ratchet or not could of course be made by the end user or rather be triggered by the application at an upper layer, based on a security policy. For instance, it could make sense to ratchet on a smartphone for every new message following bringing back the app to foreground, or to ratchet no more than once an hour.

Another interesting outcome of our hybrid system is that we can form our hybrid system with two identical protocols: an upper one and a lower one. The lower protocol is used to communicate the messages and the upper protocol is used to control the lower protocol: to setup or to reset it. With this hybrid structure with identical protocols, we can repair broken communication in the case of a message loss or active attacks. As far as we observe, the complexity of the hybrid system is the same as the complexity of the underlying protocol. Since our security-aware property breaks communication in the case of an active attack, this repairing construction is a nice additional tool.

Last but not least, we implemented the many existing protocols: \(\mathsf {PR}\), \(\mathsf {JS}\), \(\mathsf {DV}\), \(\mathsf {JMM}\), \(\mathsf {ACD}\), \(\mathsf {ACD}\text {-}\mathsf {PK}\), together with \(\mathsf {EtH}\). We observe that \(\mathsf {EtH}\) is the fastest one. This is not surprising for all protocols which heavily use public-key cryptography, but it is surprising for \(\mathsf {ACD}\). Our goal is to offer a high level of security with the performances of \(\mathsf {EtH}\). We reach it with on-demand ratcheting when the participant demands healing scarcely.

Finally, we conclude that security awareness can be added on top of an existing protocol (even a hybrid one) in a generic way to strengthen security. We propose this generic strengthening (called \(\mathsf {chain}\)) of protocol to obtain \(\mathsf {r\text {-}RECOVER}\) and \(\mathsf {s\text {-}RECOVER}\) security on the top of any protocol. As an example, we apply it on the ratchet-on-demand hybrid protocol composed with \(\mathsf {DV}\) and \(\mathsf {EtH}\) and obtain our final protocol.

We provide a comparison of all the protocols with \(\mathsf {r\text {-}RECOVER}\)-security, \(\mathsf {s\text {-}RECOVER}\)-security, acknowledgment extractor and cleanness extractor in Table 1. Note that this table is made to help both the authors and the readers to have a fair understanding of what specified properties each protocol has or not. We stress that “any” protocol could form a hybrid system to provide ratchet-on-demand and repairing a broken communication in the case of message loss or active attacks. The protocol which is shown in the last column is the case where we chose to use \(\mathsf {DV}\) and \(\mathsf {EtH}\) to construct our hybrid system.

Table 1. Comparison of Several Protocols with our protocol \(\mathsf {chain}(\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {DV},\mathsf {EtH}))\) from Corollary 29 in Sect. 3.3: security level; worst case complexity for exchanging n messages; types of coin-leakage security; plain model (i.e. no random oracle); PKC or less (i.e. no \(\mathsf {HIBE}\)). \(\mathsf {DV}\) and \(\mathsf {ARCAD}_\mathsf {DV}\) have identical characteristics. \(\mathsf {ARCAD}_\mathsf {DV}\) is based on \(\mathsf {DV}\) and described in Appendix B. The terms “optimal”, “near-optimal”, and “sub-optimal” from Durak-Vaudenay [7] are mentioned on p. 2. “Pragmatic” degrades a bit security to offer on-demand ratcheting. “id-optimal” is optimal among protocols with immediate decryption.

To summarize, our contributions are:

  • we formally define the notion of security awareness, construct a generic protocol strengthening called \(\mathsf {chain}\), and prove its security;

  • we define the notion of on-demand ratcheting, construct a generic hybrid protocol called \(\mathsf {hybrid}\), define and prove its security;

  • we implement \(\mathsf {PR}\), \(\mathsf {JS}\), \(\mathsf {DV}\), \(\mathsf {JMM}\), \(\mathsf {ACD}\), \(\mathsf {ACD}\text {-}\mathsf {PK}\), and \(\mathsf {EtH}\) protocols in order to clearly compare their performances.

Notation. We have two participants named Alice (A) and Bob (B). Whenever we talk about either one of the participants, we represent it as P, then \(\overline{P}\) refers to P’s counterpart. We have two roles \(\mathsf {send}\) and \(\mathsf {rec}\) for sender and receiver respectively. We define \(\overline{\mathsf {send}}=\mathsf {rec}\) and \(\overline{\mathsf {rec}}=\mathsf {send}\). When the communication is unidirectional, the participants are called the sender S and the receiver R.

Structure of the Paper. In Sect. 2, we revisit the preliminary notions from Durak-Vaudenay [7] and Alwen-Coretti-Dodis [1]. They all are essential to be able to follow our results. In Sect. 3, we define a new notion named security awareness and build a protocol with regard to the notion. In Sect. 4, we define a new protocol called on-demand ratcheting with better performance than state-of the-art. Finally, in Appendix A, we present our implementation results with the figures comparing various protocols. Appendix B presents \(\mathsf {ARCAD}_\mathsf {DV}\): the \(\mathsf {DV}\) protocol in a simplified form and in the frame of \(\mathsf {ARCAD}\).

2 Preliminaries

2.1 \(\mathsf {ARCAD}\) Definition and Security

In this section, we recall the \(\mathsf {DV}\) model [7] and we slightly adapt it to define asynchronous ratcheted communication with additional data denoted as \(\mathsf {ARCAD}\). That is, we consider message encryption instead of key agreement (\(\mathsf {BARK}\): bidirectional asynchronous ratcheted key agreement). The difference between \(\mathsf {BARK}\) and \(\mathsf {ARCAD}\) is the same as the difference between KEM and cryptosystems: \(\mathsf {pt}\) is input to \(\mathsf {Send}\) instead of output of \(\mathsf {Send}\). Additionally, we treat associated data \(\mathsf {ad}\) to authenticate. Like \(\mathsf {DV}\) [7]Footnote 3, we adopt asymptotic security rather than exact security, for more readability. Adversaries and algorithms are probabilistic polynomially bounded (PPT) in terms of a parameter \(\lambda \).

As we slightly change our direction from key exchange to encryption, we feel that it is essential to redefine the set of definitions from \(\mathsf {BARK}\) for \(\mathsf {ARCAD}\). In this section, some of the definitions are marked with the reference [7]. It means that these definitions are unchanged except for possible necessary notation changes. The other definitions are straightforward adaptations to fit \(\mathsf {ARCAD}\). We try not to overload this section by redefining already existing terminology, hence, we let less essential definitions in the full version [4].

Definition 1

(\(\mathsf {ARCAD}\)). An asynchronous ratcheted communication with additional data (\(\mathsf {ARCAD}\)) consists of the following PPT algorithms:

  • \(\mathsf {Setup}(1^{\lambda }) \xrightarrow {\$} \mathsf {pp}\): This defines the common public parameters \(\mathsf {pp}\).

  • \(\mathsf {Gen}(1^{\lambda },\mathsf {pp}) \xrightarrow {\$} (\mathsf {sk},\mathsf {pk})\): This generates the secret key \(\mathsf {sk}\) and the public key \(\mathsf {pk}\) of a participant.

  • \(\mathsf {Init}(1^{\lambda },\mathsf {pp},\mathsf {sk}_P,\mathsf {pk}_{\overline{P}},P) \rightarrow \mathsf {st}_P\): This sets up the initial state \(\mathsf {st}_P\) of P given his secret key, and the public key of his counterpart.

  • \(\mathsf {Send}(\mathsf {st}_P,\mathsf {ad},\mathsf {pt}) \xrightarrow {\$} (\mathsf {st}'_P, \mathsf {ct})\): it takes as input a plaintext \(\mathsf {pt}\) and some associated data \(\mathsf {ad}\) and produces a ciphertext \(\mathsf {ct}\) along with an updated state \(\mathsf {st}'_P\).

  • \(\mathsf {Receive}(\mathsf {st}_P,\mathsf {ad},\mathsf {ct}) \rightarrow (\mathsf {acc}, \mathsf {st}'_P, \mathsf {pt}) \): it takes as input a ciphertext \(\mathsf {ct}\) and some associated data \(\mathsf {ad}\) and produces a plaintext \(\mathsf {pt}\) with an updated state \(\mathsf {st}'_P\) together with a flag \(\mathsf {acc}\).Footnote 4

An additional \(\mathsf {Initall}(1^\lambda ,\mathsf {pp})\rightarrow (\mathsf {st}_A,\mathsf {st}_B,z)\) algorithm, which returns the initial states of A and B as well as public information z, is defined as follows:

figure a

\(\mathsf {Initall}\) is defined for convenience as an initialization procedure for all games. None of our security games actually cares about how \(\mathsf {Initall}\) is made from \(\mathsf {Gen}\) and \(\mathsf {Init}\). This is nice because there is little to change to define a notion of “symmetric-cryptography-based \(\mathsf {ARCAD}\)” with a slight abuse of definition: we only need to define \(\mathsf {Initall}\). This approach was already adopted for \(\mathsf {EtH}\) [13] which was proven as a “secure \(\mathsf {ARCAD}\)” in this way.

For all global variables v in the game such as \(\mathsf {received}_\mathsf {ct}^P\), \(\mathsf {st}_P\), or \(\mathsf {ct}_P\) (which appear in Fig. 1 and Fig. 2, for instance), we denote the value of v at time t by v(t). The notion of time is participant-specific. It refers to the number of elementary operations he has done. We assume neither synchronization nor central clock. Time for two different participants can only be compared when they are run non-concurrently by an adversary in a game.

Definition 2

(Correctness of \(\mathsf {ARCAD}\)). Consider the correctness game given on Fig. 1.Footnote 5 We say that an \(\mathsf {ARCAD}\) protocol is correct if for all sequence \(\mathsf {sched}\) of tuples of the form \((P,``\mathsf {send}",\mathsf {ad}, \mathsf {pt})\) or \((P,``\mathsf {rec}")\), the game never returns 1. Namely,

  • at each stage, for each P, \(\mathsf {received}_\mathsf {pt}^{P}\) is prefix of \(\mathsf {sent}_\mathsf {pt}^{\overline{P}}\)Footnote 6;

  • each \(\mathsf {RATCH}(P,``\mathsf {rec}")\) call returns \(\mathsf {acc}=\mathsf {true}\).

Fig. 1.
figure 1

The Correctness Game of \(\mathsf {ARCAD}\) Protocol.

We note that \(\mathsf {RATCH}(P,``\mathsf {rec}",\mathsf {ad},\mathsf {ct})\) ignores messages when decryption fails. For this reason, when we say that a participant P “receives” a message, we may implicitly mean that the message was accepted. More precisely, it means that decryption succeeded and \(\mathsf {RATCH}\) returned \(\mathsf {acc}=\mathsf {true}\).

In addition to the \(\mathsf {RATCH}\) oracle (in Fig. 1) which is used to ratchet (either to send or to receive), we define several other oracles (in Fig. 2): \(\mathsf {EXP_{st}}\) to obtain the state of a participant; \(\mathsf {EXP_{pt}}\) to obtain the last received message \(\mathsf {pt}\); \(\mathsf {CHALLENGE}\) to send either the plaintext or a random string. All those oracles are used without change throughout all security notions in this paper.

Definition 3

(Matching status [7]). We say that P is in a matching status at time t for P if

  1. 1.

    at any moment of the game before time t for P, \(\mathsf {received}_\mathsf {ct}^P\) is a prefix of \(\mathsf {sent}_\mathsf {ct}^{\overline{P}}\)—this defines the time \(\overline{t}\) for \(\overline{P}\) when \(\overline{P}\) sent the last message in \(\mathsf {received}_\mathsf {ct}^P(t)\);

  2. 2.

    at any moment of the game before time \(\overline{t}\) for \(\overline{P}\), \(\mathsf {received}_\mathsf {ct}^{\overline{P}}\) is a prefix of \(\mathsf {sent}_\mathsf {ct}^P\).

We further say that time t for P originates from time \(\overline{t}\) for \(\overline{P}\).

Intuitively, P is in a matching status at a given time if his state is not influenced by an active attack (i.e. message injection/modification/erasure/replay).

Definition 4

(Forgery). Given a participant P in a game, we say that \((\mathsf {ad},\mathsf {ct})\in \mathsf {received}_\mathsf {ct}^P\) is a forgery if at the moment of the game just before P received \((\mathsf {ad},\mathsf {ct})\), P was in a matching status, but no longer after receiving \((\mathsf {ad},\mathsf {ct})\).

Definition 5

(Trivial forgery). Let \((\mathsf {ad},\mathsf {ct})\) be a forgery received by P. At the time t just before the \(\mathsf {RATCH}(P,``\mathsf {rec}",\mathsf {ad},\mathsf {ct})\) call, P was in a matching status. We assume that time t for P originates from time \(\overline{t}\) for \(\overline{P}\). If there is an \(\mathsf {EXP_{st}}(\overline{P})\) call between time \(\overline{t}\) for \(\overline{P}\) and the next \(\mathsf {RATCH}(\overline{P},``\mathsf {send}",.,.)\) call (or just after time \(\overline{t}\) is there is no further \(\mathsf {RATCH}(\overline{P},``\mathsf {send}",.,.)\) call), we say that \((\mathsf {ad},\mathsf {ct})\) is a trivial forgery.

We give a brief description of the \(\mathsf {DV}\) security notions [7] as follows.

\(\mathsf {FORGE}\)-security: It makes sure that there is no forgery, except trivial ones.

\(\mathsf {r\text {-}RECOVER}\)-securityFootnote 7: If an adversary manages to forge (trivially or not) a message to one of the participants, then this participant can no longer accept genuine messages from his counterpart.

\(\mathsf {PREDICT}\)-security: The adversary cannot guess the value \(\mathsf {ct}\) which will be output from the \(\mathsf {Send}\) algorithm.

\(\mathsf {KIND}\)-security: We omit this security notion which is specific to key exchange. Instead, we consider \(\mathsf {IND\text {-}CCA}\)-security in a real-or-random style.

We define the ratcheting security with \(\mathsf {IND\text {-}CCA}\) notion. Before defining it, we like to introduce a predicate called \(C_\mathsf {clean}\) as \(\mathsf {IND\text {-}CCA}\) is relative to this predicate. The purpose of \(C_\mathsf {clean}\) is to discard trivial attacks. Somehow, the technicality of the security notion is hidden in this cleanness notion. An “optimal” cleanness predicate discards only trivial attacks but other predicates may discard more and allow to have more efficient protocols [7].

More precisely, for “clean” cases, a security property must be guaranteed. A “trivial” attack (i.e. an attack that no protocol can avoid) implies a non-clean case. If the cleanness notion is tight, this is an equivalence.

In the full version [4] we recall the most useful cleanness predicates. In short, \(C_\mathsf {leak}\wedge C^{A,B}_{\mathsf {trivial\ forge}}\) corresponds to the \(\mathsf {DV}\)-cleanness notion for post-compromise security (“sub-optimal”) and \(C_\mathsf {sym}\) is the weaker cleanness notion for forward secrecy only which is adapted to symmetric cryptographic schemes.

Fig. 2.
figure 2

\(\mathsf {IND\text {-}CCA}\) Game. (Oracle \(\mathsf {RATCH}\) is defined in Fig. 1)

Definition 6

(\(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\) security). Let \(C_\mathsf {clean}\) be a cleanness predicate. We consider the \(\mathsf {IND\text {-}CCA}_{b,C_\mathsf {clean}}^{\mathcal {A}}\) game of Fig. 2. We say that the \(\mathsf {ARCAD}\) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure if for any PPT adversary, the advantage

$$ \mathsf {Adv}(\mathcal {A})= \left| \Pr \left[ \mathsf {IND\text {-}CCA}_{0, C_\mathsf {clean}}^{\mathcal {A}}(1^\lambda ) \rightarrow 1 \right] - \Pr \left[ \mathsf {IND\text {-}CCA}_{1, C_\mathsf {clean}}^{\mathcal {A}}(1^\lambda ) \rightarrow 1 \right] \right| $$

of \(\mathcal {A}\) in \(\mathsf {IND\text {-}CCA}_{b,C_\mathsf {clean}}^{\mathcal {A}}\) security game is negligible.

Fig. 3.
figure 3

\(\mathsf {FORGE}\), \(\mathsf {r\text {-}RECOVER}\), and \(\mathsf {PREDICT}\) Games. (Oracles \(\mathsf {RATCH}\), \(\mathsf {EXP_{st}}\), \(\mathsf {EXP_{pt}}\) are defined in Fig. 1 and Fig. 2.)

Definition 7

(\(C_\mathsf {clean}\)-\(\mathsf {FORGE}\) security). Given a cleanness predicate \(C_\mathsf {clean}\), consider \(\mathsf {FORGE}^{\mathcal {A}}_{C_\mathsf {clean}}\) game in Fig. 3 associated to the adversary \(\mathcal {A}\). Let the advantage of \(\mathcal {A}\) be the probability that the game outputs 1. We say that \(\mathsf {ARCAD}\) is \(C_\mathsf {clean}\)-\(\mathsf {FORGE}\)-secure if, for any PPT adversary, the advantage is negligible.

In this definition, we added the notion of cleanness which determines if an attack is trivial or not. The original notion of \(\mathsf {FORGE}\) security [7] is equivalent to using the following \(C_\mathsf {trivial}\) predicate \(C_\mathsf {clean}\):

 

  • \(C_\mathsf {trivial}\): the last \((\mathsf {ad},\mathsf {ct})\) message is not a trivial forgery (following Definitions 5).

The purpose of this update in the definition is to allow us to easily define a weaker form of \(\mathsf {FORGE}\)-security for symmetric protocols and in Sect. 3.3.

Definition 8

(\(\mathsf {r\text {-}RECOVER}\) security [7]). Consider the \(\mathsf {r\text {-}RECOVER}^{\mathcal {A}}\) game in Fig. 3 associated to the adversary \(\mathcal {A}\). Let the advantage of \(\mathcal {A}\) in succeeding in the game be \(\Pr (\mathsf {win}=1)\). We say that the \(\mathsf {ARCAD}\) is \(\mathsf {r\text {-}RECOVER}\)-secure, if for any PPT adversary, the advantage is negligible.

Definition 9

(\(\mathsf {PREDICT}\) security [7]). Consider \(\mathsf {PREDICT}^{\mathcal {A}}(1^\lambda )\) game in Fig. 3 associated to the adversary \(\mathcal {A}\). Let the advantage of \(\mathcal {A}\) in succeeding in the game be the probability that 1 is returned. We say that the \(\mathsf {ARCAD}\) is \(\mathsf {PREDICT}\)-secure, if for any PPT adversary, the advantage is negligible.

\(\mathsf {PREDICT}\)-security is useful to reduce the notion of matching status to the two conditions that \(\mathsf {received}_\mathsf {ct}^P\) is a prefix of \(\mathsf {sent}_\mathsf {ct}^{\overline{P}}\) at time t for P and \(\mathsf {received}_\mathsf {ct}^{\overline{P}}\) is a prefix of \(\mathsf {sent}_\mathsf {ct}^P\) at time \(\overline{t}\) for \(\overline{P}\).

2.2 The Epoch Notion in Secure Communication

We define the epochs in an equivalent way to the work done by Alwen et al. [1].Footnote 8 Epochs are useful to designate the sequence of messages, as both participants may not see exactly the same. We will use epoch numbers in the design of our hybrid scheme for on-demand ratcheting in Sect. 4.1.

Epochs are a set of consecutive messages going in the same direction. An epoch is identified by an integer counter e. Each message is assigned one epoch counter \(\mathsf {e_{m}}\). Hence, the epochs are non-intersecting. For convenience, each participant P keeps the epoch value \(\mathsf {e_{send}^{P}}\) of the last sent message and the epoch value \(\mathsf {e_{rec}^{P}}\) of the last received message. They are used to assign an epoch to a message to be sent.

Definition 10

(Epoch). Epochs are non-intersecting sets of messages which are defined by an integer. During the game, we let \(\mathsf {e_{rec}^{P}}\) (resp. \(\mathsf {e_{send}^{P}}\)) be the epoch of the last received (resp. sent) message by P. At the very beginning of the protocol, we define \(\mathsf {e_{send}^{P}}\) and \(\mathsf {e_{rec}^{P}}\) specifically. For the participant A, \(\mathsf {e_{rec}^{A}}=-1\) and \(\mathsf {e_{send}^{A}}=0\). For the participant B, \(\mathsf {e_{send}^{B}}=-1\) and \(\mathsf {e_{rec}^{B}}=0\). The procedure to assign an epoch \(\mathsf {e_{m}}\) to a new sent message follows the rule described next:

If \(\mathsf {e_{rec}^{P}}< \mathsf {e_{send}^{P}}\), then the message is put in the epoch \(\mathsf {e_{m}}= \mathsf {e_{send}^{P}}\). Otherwise, it is put in epoch \(\mathsf {e_{m}}= \mathsf {e_{rec}^{P}}+1\).

Let \(\mathsf {e_{P}}= \max \{\mathsf {e_{rec}^{P}}, \mathsf {e_{send}^{P}}\}\). Let \(b_A=0\) and \(b_B=1\). We have

$$ \mathsf {e_{send}^{P}}= {\left\{ \begin{array}{ll} \mathsf {e_{P}}&{} \text{ if } \mathsf {e_{P}}\bmod 2 = b_P \\ \mathsf {e_{P}}-1 &{} \text{ otherwise } \end{array}\right. } \qquad \mathsf {e_{rec}^{P}}= {\left\{ \begin{array}{ll} \mathsf {e_{P}}&{} \text{ if } \mathsf {e_{P}}\bmod 2 \ne b_P \\ \mathsf {e_{P}}-1 &{} \text{ otherwise } \end{array}\right. } $$

Therefore, it is equivalent to maintain \((\mathsf {e_{rec}^{P}}, \mathsf {e_{send}^{P}})\) or \(\mathsf {e_{P}}\). The procedure to manage \(\mathsf {e_{P}}\) and \(\mathsf {e_{m}}\) is described by Alwen et al. [1].

We will use a counter c for each epoch e. We will use the order on (ec) pairs defined by

$$ (e,c)<(e',c') \Longleftrightarrow (e<e' \vee (e=e'\wedge c<c')) $$

3 Security Awareness

3.1 \(\mathsf {s\text {-}RECOVER}\) Security

We gave the \(\mathsf {DV}\) \(\mathsf {r\text {-}RECOVER}\) security definition [7] in Definition 8. It is an important notion to capture that P cannot accept a genuine \(\mathsf {ct}\) from \(\overline{P}\) after P receives a forgery. However, \(\mathsf {r\text {-}RECOVER}\)-security does not capture the fact that when it is \(\overline{P}\) who receives a forgery, P could still accept messages which come from \(\overline{P}\). We strengthen \(\mathsf {r\text {-}RECOVER}\) security with another definition called \(\mathsf {s\text {-}RECOVER}\).

Definition 11

(\(\mathsf {s\text {-}RECOVER}\) security). In the \(\mathsf {s\text {-}RECOVER}^{\mathcal {A}}\) game in Fig. 4 with the adversary \(\mathcal {A}\), we let the advantage of \(\mathcal {A}\) in succeeding in the game be \(\Pr (\mathsf {win}=1)\). We say that the \(\mathsf {ARCAD}\) is \(\mathsf {s\text {-}RECOVER}\)-secure, if for any PPT adversary, the advantage is negligible.

Fig. 4.
figure 4

\(\mathsf {s\text {-}RECOVER}\) Security Game. (\(\mathsf {RATCH}\) and \(\mathsf {EXP}\) oracles are defined in Fig. 1 and Fig. 2.)

Ideally, what we want from the protocol is that participants can detect forgeries by realizing that they are no longer able to communicate to each other. We cannot prevent impersonation to happen after a state exposure but we want to make sure that the normal exchange between the participants is cut. Hence, if a participant eventually receives a genuine message (e.g. because it was authenticated after meeting in person), he should feel safe that no forgeries happened. Contrarily, detecting a communication cut requires an action from the participants, such as restoring communication using a super \(\mathsf {hybrid}\) structure, as we will suggest in Sect. 4.1.

We directly obtain the following useful result:Footnote 9

Lemma 12

If an \(\mathsf {ARCAD}\) is \(\mathsf {r\text {-}RECOVER}\), \(\mathsf {s\text {-}RECOVER}\), and \(\mathsf {PREDICT}\) secure, whenever P receives a genuine message from \(\overline{P}\) (i.e., an \((\mathsf {ad},\mathsf {ct})\) pair sent by \(\overline{P}\) is accepted by P), P is in a matching status (following Definition 3), except with negligible probability.

Our notion of \(\mathsf {RECOVER}\)-security and forgery is quite strong in the sense that it focuses on the ciphertext. Some protocols such as \(\mathsf {JMM}\) [9] focus on the plaintext. In \(\mathsf {JMM}\), \(\mathsf {ct}\) includes some encrypted data and some signature but only the encrypted data is hashed. Hence, an adversary can replace the signature by another signature after exposure of the signing key. It can be seen as not so important because it must sign the same content. However, the signature has a key update and the adversary can make the receiver update to any verifying key to desynchronize, then re-synchronize at will. Consequently, the \(\mathsf {JMM}\) protocol does not offer \(\mathsf {RECOVER}\) security as we defined it. Contrarily, \(\mathsf {PR}\) [10] hashes \((\mathsf {ad},\mathsf {ct})\) but does not use it in the next \(\mathsf {ad}\) or to compute the next \(\mathsf {ct}\). Thus, \(\mathsf {PR}\) has no \(\mathsf {RECOVER}\) security either.Footnote 10 One may think that it is easy to fix this by hashing all messages but this is not as simple. We propose in Sect. 3.3 the \(\mathsf {chain}\) transformation which can fix any protocol, thanks to Lemma 18.

3.2 Security Awareness

To have a security-awareness notion, we want \(\mathsf {r\text {-}RECOVER}\), \(\mathsf {s\text {-}RECOVER}\), and \(\mathsf {PREDICT}\) securityFootnote 11, we want to have an acknowledgment extractor (to be aware of message delivery), and we want to have a cleanness extractor (to be aware of the cleanness of every message, if not subject to trivial exposure). The last two notions are defined below. This means that on the one hand, impersonations are eventually discovered, and on the other hand, by assuming that no impersonation occurs and assuming that exposures are known, a participant P knows exactly which messages are safe, at least after one round-trip occurred.

Definition 13

(Security-awareness). A protocol is \(C_\mathsf {clean}\)-security-aware if

  • it is \(\mathsf {r\text {-}RECOVER}\), \(\mathsf {s\text {-}RECOVER}\), and \(\mathsf {PREDICT}\)-secure;

  • there is an acknowledgment extractor (Definition 15);

  • there is a cleanness extractor for \(C_\mathsf {clean}\) (Definition 16).

To make participants aware of the security status of any (challenge) message, they need to know the history of exposures, they need to be able to reconstruct the history of \(\mathsf {RATCH}\) calls from their own view, and they need to be able to evaluate the \(C_\mathsf {clean}\) predicate. Thankfully, the \(C_\mathsf {clean}\) predicates that we consider only depend on these histories. We first formally define the notion of transcript.

Definition 14

(Transcript). In a game, for a participant P, we define the transcript of P as the chronological sequence \(T_P\) of all \((\mathsf {oracle},\mathsf {extra})\) pairs involving P where each pair represents an oracle call to \(\mathsf {oracle}\) with P as input (i.e. either \(\mathsf {RATCH}(P, ``\mathsf {rec}", ., .)\), \(\mathsf {RATCH}( P, ``\mathsf {send}", .,.)\), \(\mathsf {EXP}_\mathsf {pt}(P)\), \(\mathsf {EXP_{st}}(P)\), or \(\mathsf {CHALLENGE}(P)\)), except the unsuccessful \(\mathsf {RATCH}\) calls which are omitted. For each pair with a \(\mathsf {RATCH}\) or \(\mathsf {CHALLENGE}\) oracle, \(\mathsf {extra}\) specifies the role (\(``\mathsf {send}"\) or \(``\mathsf {rec}"\)) and the message \((\mathsf {ad},\mathsf {ct})\) of the oracle call. For other pairs, \(\mathsf {extra}=\bot \).

The partial transcript of P up to time t is the prefix \(T_P(t)\) of \(T_P\) of all oracle calls until time t. The \(\mathsf {RATCH}\)-transcript of P is the list \(T^\mathsf {RATCH}_P\) of all \(\mathsf {extra}\) elements in \(T_P\) which are not \(\bot \) (i.e. it only includes \(\mathsf {RATCH}\)/\(\mathsf {CHALLENGE}\) calls). Similarly, the partial \(\mathsf {RATCH}\)-transcript of P up to time t is the list \(T^\mathsf {RATCH}_P(t)\) of \(\mathsf {extra}\) elements in \(T_P(t)\) which are not \(\bot \).

Next, we formalize that a participant can be aware of which of his messages were received by his counterpart.

Definition 15

(Acknowledgment extractor). We consider a game \(\Gamma \) where the transcript \(T_P\) is formed for a participant P. Given a message \((\mathsf {ad},\mathsf {ct})\) successfully received by P at time t and which was sent by \(\overline{P}\) at time \(\overline{t}\), we let \((\mathsf {ad}',\mathsf {ct}')\) be the last message successfully received by \(\overline{P}\) before time \(\overline{t}\). (If there is no such message, we set it to \(\bot \).)

An acknowledgment extractor is an efficient function f such that \(f(T^\mathsf {RATCH}_P(t))=(\mathsf {ad}',\mathsf {ct}')\) for any time t when P is in a matching status (Definition 3).

Given this extractor, P can iteratively reconstruct the entire flow of messages, and which messages crossed each other during transmission.

We formalize awareness of a participant for the safety of each message.

Definition 16

(Cleanness extractor). We consider a game \(\Gamma \) where the transcript \(T_P\) is formed for a participant P. Let t be a time for P and \(\overline{t}\) be a time for \(\overline{P}\). Let \(T_P(t)\) and \(T_{\overline{P}}(\overline{t})\) be the partial transcripts at those time. We say that there is a cleanness extractor for \(C_\mathsf {clean}\) if there is an efficient function g such that \(g(T_P(t),T_{\overline{P}}(\overline{t}))\) has the following properties: if there is one \(\mathsf {CHALLENGE}\) in the \(T_P(t)\) transcript and, either P received \((\mathsf {ad}_\mathsf {test},\mathsf {ct}_\mathsf {test})\) or there is a round trip \(P\rightarrow \overline{P}\rightarrow P\) starting with P sending \((\mathsf {ad}_\mathsf {test},\mathsf {ct}_\mathsf {test})\) to \(\overline{P}\), then \(g(T_P(t),T_{\overline{P}}(\overline{t}))=C_\mathsf {clean}(\Gamma )\). Otherwise, \(g(T_P(t),T_{\overline{P}}(\overline{t}))=\bot \).

The function g is able to predict whether the game is “clean” for any challenge message. The case with an incomplete round trip \(P\rightarrow \overline{P}\rightarrow P\) starting with P sending \((\mathsf {ad}_\mathsf {test},\mathsf {ct}_\mathsf {test})\) to \(\overline{P}\) is when the tested message was sent but somehow never acknowledged for the reception. If the message never arrived, we cannot say for sure if the game is clean because the counterpart may later either receive it and make the game clean or have a state exposure and make the game not clean. In other cases, the cleanness can be determined for sure.

3.3 Strongly Secure \(\mathsf {ARCAD}\) with Security Awareness

In this section, we take a secure \(\mathsf {ARCAD}\) (it could be \(\mathsf {ARCAD}_\mathsf {DV}\), in the full version [4], or the hybrid one defined in Sect. 4) which we denote by \(\mathsf {ARCAD}_0\) and we transform it into another secure \(\mathsf {ARCAD}\) which we denote by \(\mathsf {ARCAD}_1=\mathsf {chain}(\mathsf {ARCAD}_0)\), that is security aware. We achieve security awareness by keeping some hashes in the states of participants. The intuitive way to build it is to make chains of hash of ciphertexts (like a blockchain) which will be sent and received and to associate each message to the digest of the chain. This enables a participant P to acknowledge its counterpart about received messages whenever P sends a new message.

We define a tuple \((\mathsf {Hsent}, \mathsf {Hreceived}, \mathsf {snt\_noack}, \mathsf {rec\_toack})\) and store it in the state of a participant. \(\mathsf {Hsent}\) is the hash of all sent ciphertexts. It is computed by the sender and delivered to the counterpart along with \(\mathsf {ct}\). It is updated with hashing key \(\mathsf {hk}\) and the old \(\mathsf {Hsent}\) every time a new \(\mathsf {Send}\) operation is called. Likewise, \(\mathsf {Hreceived}\) is the hash of all received ciphertexts. It is computed with \(\mathsf {hk}\) and the last stored \(\mathsf {Hreceived}\) by the receiver upon receiving a message. It is updated every time a new \(\mathsf {Receive}\) operation is run.

Using \(\mathsf {Hsent}\) and \(\mathsf {Hreceived}\) alone is sufficient for \(\mathsf {r\text {-}RECOVER}\) security but not for \(\mathsf {s\text {-}RECOVER}\) security.

\(\mathsf {rec\_toack}\) is a counter of received messages which need to be reported when the next \(\mathsf {Send}\) operation is run. For each \(\mathsf {Send}\) operation, the protocol attaches to \(\mathsf {ct}\) the last \(\mathsf {Hreceived}\) to acknowledge for received messages and reset \(\mathsf {rec\_toack}\) to 0. \(\mathsf {rec\_toack}\) is incremented by each \(\mathsf {Receive}\).

\(\mathsf {snt\_noack}\) is a list of the hashes of sent ciphertexts which are waiting for an acknowledgment. Basically, it is initialized to an empty array in the beginning and whenever a new \(\mathsf {Hsent}\) is computed, it is accumulated in this array. The purpose of such a list is to keep track of the sent messages for which the sender expects an acknowledgment. More precisely, when the participant P keeps its list of sent ciphertexts in \(\mathsf {snt\_noack}\), the counterpart \(\overline{P}\) keeps a counter \(\mathsf {rec\_toack}\) telling that an acknowledgment is needed. Remember that \(\overline{P}\) sends \(\mathsf {Hreceived}\) back to the participant P to acknowledge him about received messages. As soon as \(\overline{P}\) acknowledges, P deletes the hash of the acknowledged ciphertexts from \(\mathsf {snt\_noack}\).

The principle of our construction is that if an adversary starts to impersonate a participant after exposure, there is a fork in the list of message chains which is viewed by both participants and those chains can never merge again without making a collision.

We give our security aware protocol on Fig. 5. The security of the protocol is proved with the following lemmas.

Fig. 5.
figure 5

Our Security-Aware \(\mathsf {ARCAD}_1=\mathsf {chain}(\mathsf {ARCAD}_0)\) Protocol.

Theorem 17

If \(\mathsf {ARCAD}_0\) is correct, then \(\mathsf {chain}(\mathsf {ARCAD}_0)\) is correct.

The proof is straightforward.

Lemma 18

If H is collision-resistant, \(\mathsf {chain}(\mathsf {ARCAD}_0)\) is \(\mathsf {RECOVER}\)-secure (for both \(\mathsf {s\text {-}RECOVER}\) and \(\mathsf {r\text {-}RECOVER}\) security).

Proof

All \((\mathsf {ad},\mathsf {ct})\) messages seen by one participant P in one direction (send or receive) are chained by hashing. Hence, if \(\mathsf {received}^P_\mathsf {ct}=(\mathsf {seq}_1,(\mathsf {ad},\mathsf {ct}),\mathsf {seq}_2)\), the \((\mathsf {ad},\mathsf {ct})\) message includes (in the second field of \(\mathsf {ct}\)) the hash h of \(\mathsf {seq}_1\). If \(\mathsf {sent}^{\overline{P}}_\mathsf {ct}=(\mathsf {seq}_3,(\mathsf {ad},\mathsf {ct}),\mathsf {seq}_4)\), the \((\mathsf {ad},\mathsf {ct})\) message includes the hash h of \(\mathsf {seq}_3\). If H is collision-resistant, then \(\mathsf {seq}_1\ne \mathsf {seq}_3\) with negligible probability. Hence, we have \(\mathsf {r\text {-}RECOVER}\) security.

Additionally, all genuine \((\mathsf {ad},\mathsf {ct})\) messages include (in the third field of \(\mathsf {ct}\)) the hash \(\mathsf {ack}\) of messages which are received by the counterpart. This list must be approved by P, thus it must match the list of hashes of messages that P sent. Hence, if \(\mathsf {received}^P_\mathsf {ct}\) is prefix of \(\mathsf {sent}^{\overline{P}}_\mathsf {ct}\) and \(\overline{t}\) is the time when \(\overline{P}\) sent the last message in \(\mathsf {received}^P_\mathsf {ct}\), then this message includes the hash of \(\mathsf {received}^{\overline{P}}_\mathsf {ct}(\overline{t})\) which must be a hash of a prefix of \(\mathsf {sent}^P_\mathsf {ct}\). Thus, unless there is a collision in the hash function, \(\mathsf {received}^{\overline{P}}_\mathsf {ct}(\overline{t})\) is a prefix of \(\mathsf {sent}_\mathsf {ct}^P\) and we have \(\mathsf {s\text {-}RECOVER}\) security.    \(\square \)

Lemma 19

\(\mathsf {chain}(\mathsf {ARCAD}_0)\) has an acknowledgment extractor.

Proof

Let \((\mathsf {ad},\mathsf {ct})\) be a message sent by \(\overline{P}\) to P in a matching status. Let \((\mathsf {ad}',\mathsf {ct}')\) be the last message received by \(\overline{P}\) before sending \((\mathsf {ad},\mathsf {ct})\). Due to the protocol, \(\mathsf {ct}\) includes the value of \(\mathsf {Hreceived}\) after receiving \((\mathsf {ad}',\mathsf {ct}')\). Since this message is from P, P recognizes this hash \(\mathsf {Hreceived}=\mathsf {Hsent}\) from \(\mathsf {snt\_noack}\). Both \((\mathsf {ad}',\mathsf {ct}')\) and this hash can be computed from \(T^\mathsf {RATCH}_P(t)\). Hence, \(\mathsf {chain}(\mathsf {ARCAD}_0)\) has an extractor.    \(\square \)

Lemma 20

\(\mathsf {chain}(\mathsf {ARCAD}_0)\) has a cleanness extractor for the following predicates:

$$ C_\mathsf {leak}, C_{\mathsf {trivial}\mathsf {forge}}^{P_\mathsf {test}}, C_{\mathsf {trivial}\mathsf {forge}}^{A,B}, C_{\mathsf {forge}}^{P_\mathsf {test}}, C_{\mathsf {forge}}^{A,B}, C_\mathsf {ratchet}, C_\mathsf {noexp}$$

Hence, there is an extractor for all cleanness predicates which we considered.Footnote 12

The following result is trivial.

Lemma 21

If \(\mathsf {ARCAD}_0\) is \(\mathsf {PREDICT}\)-secure, then \(\mathsf {chain}(\mathsf {ARCAD}_0)\) is \(\mathsf {PREDICT}\)-secure.

Consequently, if \(\mathsf {ARCAD}_0\) is \(\mathsf {PREDICT}\)-secure, \(\mathsf {chain}(\mathsf {ARCAD}_0)\) is security-aware.

4 On-Demand Ratcheting

In this section, we define a bidirectional secure communication messaging protocol with hybrid on-demand ratcheting. The aim is to design such a protocol to integrate two ratcheting protocols with different security levels: a strongly secure protocol using public-key cryptography and a weaker but much more efficient protocol with symmetric key primitives. The core of the protocol is to use the weak protocol with frequent exchanges and to use the strong one on demand by the sending participant. Hence, we build a more efficient protocol with on-demand ratcheting. Yet, it comes with a security drawback. Even though the security for the former is to provide post-compromise security, we secure part of the communication only with the forward secure protocol.

The sender uses a \(\mathsf {flag}\) to tell which level of security the communication will have and apply ratcheting with public-key cryptography or the lighter primitives such as the \(\mathsf {EtH}\) protocol [13]. The \(\mathsf {flag}\) is set in the \(\mathsf {ad}\) input and it is denoted as \(\mathsf {ad}.\mathsf {flag}\). We call the strong protocol as \(\mathsf {ARCAD}_\mathsf {main}\) and the weak one as \(\mathsf {ARCAD}_\mathsf {sub}\). Ideally, the time to set the \(\mathsf {flag}\) for specific security can be decided during the deployment of the application using the protocol. This choice may also be left to the users who can decide based on the confidentiality-level of their communication. The more often the protocol turns the flag on, the more secure is the hybrid on-demand protocol. If we do it for every message exchange, then we obtain \(\mathsf {ARCAD}_\mathsf {main}\) without \(\mathsf {ARCAD}_\mathsf {sub}\). If we do it for no message exchange, then we obtain \(\mathsf {ARCAD}_\mathsf {sub}\).

4.1 Our Hybrid On-Demand \(\mathsf {ARCAD}\) Protocol

We give our on-demand \(\mathsf {ARCAD}\) protocol on Fig. 6. It uses two sub-protocols called \(\mathsf {ARCAD}_\mathsf {main}\) and \(\mathsf {ARCAD}_\mathsf {sub}\). The former is to represent a strong-but-slow protocol such as \(\mathsf {ARCAD}_\mathsf {DV}\) (Fig. 11). The latter is typically a weaker-but-faster protocol like \(\mathsf {EtH}\) [13]. The use of one or the other is based on a \(\mathsf {flag}\) that can be turned on and off in \(\mathsf {ad}\) (it is checked with \(\mathsf {ad}.\mathsf {flag}\) operation in the protocol). To have the \(\mathsf {flag}\) on lets the protocol run \(\mathsf {ARCAD}_\mathsf {main}\) while setting the \(\mathsf {flag}\) off means to run \(\mathsf {ARCAD}_\mathsf {sub}\). Assuming that \(\mathsf {ARCAD}_\mathsf {main}\) is ratcheting (i.e. post-compromise secure) and \(\mathsf {ARCAD}_\mathsf {sub}\) is not, this defines on-demand ratcheting. We denote our hybrid protocol as \(\mathsf {hybrid}\mathsf {ARCAD}=\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {main},\mathsf {ARCAD}_\mathsf {sub})\).

We use as a reference the (ec) number of messages in the \(\mathsf {ARCAD}_\mathsf {main}\) thread. Every \(\mathsf {ARCAD}_\mathsf {main}\) message creates a new \(\mathsf {ARCAD}_\mathsf {sub}\) send/receive state pair. The sending participant keeps the generated send state in a \(\mathsf {sub}[e,c]\) register under the (ec) number of the message and sends the generated receive state together with his message. The very first message which a participant sees (either in sending or receiving) forces the flag to indicate \(\mathsf {ARCAD}_\mathsf {main}\) as we have no initial \(\mathsf {ARCAD}_\mathsf {sub}\) state. The (ec) number if authenticated and also explicitly added in the ciphertext. The receiving participant checks that (ec) increases and uses the \(\mathsf {sub}[e,c]\) register state to receive the message.

Theorem 22

If the protocols \(\mathsf {ARCAD}_\mathsf {main}\) and \(\mathsf {ARCAD}_\mathsf {sub}\) are both correct, then the protocol \(\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {main},\mathsf {ARCAD}_\mathsf {sub})\) is correct.

The proof is provided in the full version [4].

Fig. 6.
figure 6

On-Demand \(\mathsf {hybrid}\mathsf {ARCAD}=\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {main},\mathsf {ARCAD}_\mathsf {sub})\) Protocol.

4.2 Application: Super-Scheme to (Re)set a Protocol

Our hybrid construction finds another application than on-demand ratcheting: defense against message loss or active attacks. Indeed, by using \(\mathsf {ARCAD}_\mathsf {main}=\mathsf {ARCAD}_\mathsf {sub}\), we can set \(\mathsf {ad}.\mathsf {flag}\) to restore an \(\mathsf {ARCAD}_\mathsf {sub}\) communication which was broken due to a message loss. Normal communication works in the \(\mathsf {ARCAD}_\mathsf {sub}\) session, hence with a flag down. However, we may use \(\mathsf {ARCAD}_\mathsf {main}\) to start a new \(\mathsf {ARCAD}_\mathsf {sub}\) session. If \(\mathsf {ARCAD}_\mathsf {sub}\) gets broken due to a message loss or an active attack on it, \(\mathsf {ARCAD}_\mathsf {main}\) can be used to restart a new \(\mathsf {ARCAD}_\mathsf {sub}\) session. We cannot resume if the \(\mathsf {ARCAD}_\mathsf {main}\) session is broken. However, we can also make nested hybrid protocols with more than two levels of protocols inside for safety. It may increase the state sizes but the performance should be nearly the same. Then, only persistent message drop attacks would succeed to make a denial of service.

4.3 Security Definitions

We modify the predicates and the notion of \(\mathsf {FORGE}\)-security from Sect. 2. In our hybrid protocol, each message \((\mathsf {ad},\mathsf {ct})\) has a clearly defined (ec) pair. A \(\mathsf {ct}\) which is input or output from \(\mathsf {RATCH}\) comes with an \(\mathsf {ad}\) which has a clearly defined \(\mathsf {ad}.\mathsf {flag}\) bit.

Sub-games. Given a game \(\Gamma \) for the \(\mathsf {hybrid}\mathsf {ARCAD}\) scheme with an adversary \(\mathcal {A}\), we define a game \(\mathsf {main}(\Gamma )\) for \(\mathsf {ARCAD}_\mathsf {main}\) with an adversary \(\mathcal {A}'\) which simulates everything but the \(\mathsf {ARCAD}_\mathsf {main}\) calls in \(\Gamma \). Namely, \(\mathcal {A}'\) simulates the enrichment of the states and all \(\mathsf {ARCAD}_\mathsf {sub}\) management together with \(\mathcal {A}\).

Given a game \(\Gamma _\mathsf {main}\) for \(\mathsf {ARCAD}_\mathsf {main}\) using no \(\mathsf {CHALLENGE}\) oracle and an (ec) pair, we denote by \(\mathsf {main}_{e,c}(\Gamma _\mathsf {main})\) the variant of \(\Gamma _\mathsf {main}\) in which the \(\mathsf {RATCH}\) \(\mathsf {Send}\) call making the message \((\mathsf {ad},\mathsf {ct})\) with pair (ec) is replaced by a \(\mathsf {CHALLENGE}\) query with \(b=1\). This perfectly simulates \(\Gamma _\mathsf {main}\) and produces the same value, and we can evaluate a predicate \(C_\mathsf {clean}\) relative to this challenge message. We define \(C_\mathsf {clean}^{e,c}(\Gamma _\mathsf {main})=C_\mathsf {clean}(\mathsf {main}_{e,c}(\Gamma _\mathsf {main}))\). Intuitively, \(C_\mathsf {clean}^{e,c}(\Gamma _\mathsf {main})\) means that the message of pair (ec) was safely encrypted and should be considered as private because no trivial attack leaks it.

We also define \(\mathsf {sub}_{e,c}(\Gamma )\) and \(\mathsf {sub}'_{e,c}(\Gamma )\). We let P be the sending participant of the \(\mathsf {ARCAD}_\mathsf {main}\) message of pair (ec). In \(\mathsf {sub}'_{e,c}(\Gamma )\), the adversary \(\mathcal {A}'\) simulates everything but the \(\mathsf {ARCAD}_\mathsf {sub}\) calls involving messages with pair (ec). The initial states of P and \(\overline{P}\) are also set by the game \(\mathsf {sub}'_{e,c}(\Gamma )\). However, it makes an \(\mathsf {EXP_{st}}(\overline{P})\) call at the beginning of the protocol to get the initial state \(\mathsf {st}_R\) for \(\mathsf {ARCAD}_\mathsf {sub}\). With this state, \(\mathcal {A}'\) can simulate the encryption of \(\mathsf {st}_R\) with \(\mathsf {ARCAD}_\mathsf {main}\) and all the rest. Clearly, the simulation is perfect but it adds an initial \(\mathsf {EXP_{st}}(\overline{P})\) call.

The \(\mathsf {sub}_{e,c}(\Gamma )\) game is a variant of \(\mathsf {sub}'_{e,c}(\Gamma )\) without the additional \(\mathsf {EXP_{st}}(\overline{P})\). To simulate the encryption of \(\mathsf {st}_R\), \(\mathcal {A}'\) encrypts a random string instead. When it comes to decrypt the obtained ciphertext, the random plaintext is ignored and the \(\mathsf {RATCH}\) calls with \(\mathsf {st}_R\) are simulated with the \(\mathsf {RATCH}\) calls for the \(\mathsf {ARCAD}_\mathsf {sub}\) game. The simulation is no longer perfect but it does not add an \(\mathsf {EXP_{st}}(\overline{P})\) call.

Hybrid Cleanness. We assume two cleanness predicates \(C_\mathsf {clean}\) and \(C_\mathsf {main}\) (which could be the same) for \(\mathsf {ARCAD}_\mathsf {main}\) and one cleanness predicate \(C_\mathsf {sub}\) for \(\mathsf {ARCAD}_\mathsf {sub}\). We define a hybrid predicate \(C^{C_\mathsf {clean}}_{C_\mathsf {main},C_\mathsf {sub}}\) as follows. By abuse of notation, we write \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\) instead, for more readability. Let \(\Gamma \) be a game played by an adversary \(\mathcal {A}\) against \(\mathsf {hybrid}\mathsf {ARCAD}\).

We let \((\mathsf {ad},\mathsf {ct})\) be the challenge message \((\mathsf {ad}_\mathsf {test},\mathsf {ct}_\mathsf {test})\) if it exists. Otherwise, \((\mathsf {ad},\mathsf {ct})\) is the last message in \(\Gamma \). We let (ec) be the number of \((\mathsf {ad},\mathsf {ct})\). We let

$$ C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}(\Gamma )= \left\{ \begin{array}{ll} \mathsf {\ if\ }(\mathsf {ad},\mathsf {ct})\mathsf {\ belongs\ to\ }\mathsf {ARCAD}_\mathsf {main}: &{} C_\mathsf {main}(\mathsf {main}(\Gamma )) \\ \mathsf {else}: \quad \left\{ \begin{array}{l} \mathsf {if\ } C^{e,c}_\mathsf {clean}(\mathsf {main}(\Gamma )): \\ \mathsf {else}: \\ \end{array}\right. &{} \begin{array}{l} C_\mathsf {sub}(\mathsf {sub}_{e,c}(\Gamma )) \\ C_\mathsf {sub}(\mathsf {sub}'_{e,c}(\Gamma )) \\ \end{array} \\ \end{array}\right. $$

This means that if the challenge holds on an \(\mathsf {ARCAD}_\mathsf {main}\) message, we only care for \(\mathsf {main}(\Gamma )\) to be \(C_\mathsf {main}\)-clean. Otherwise, either the \(\mathsf {ARCAD}_\mathsf {main}\) message initiating the relevant \(\mathsf {ARCAD}_\mathsf {sub}\) session is \(C_\mathsf {clean}\) or not. If it is clean, we can replace it and consider \(C_\mathsf {sub}\)-cleanness for \(\mathsf {sub}_{e,c}(\Gamma )\). Otherwise, the initial \(\mathsf {ARCAD}_\mathsf {sub}\) state \(\mathsf {st}_R\) trivially leaked (or was exposed, equivalently) and we consider \(C_\mathsf {sub}\)-cleanness for \(\mathsf {sub}'_{e,c}(\Gamma )\). The role of \(C_\mathsf {clean}\) is to control which of the two games to use. \(C_\mathsf {clean}\) must be a privacy cleanness notion for \(\mathsf {main}\). Contrarily, \(C_\mathsf {main}\) and \(C_\mathsf {sub}\) could be either privacy or authenticity notions.

Note that \(C_\mathsf {sub}(\mathsf {sub}'_{e,c}(\Gamma ))=\mathsf {false}\) for \(C_\mathsf {sub}=C_\mathsf {noexp}\), due to the \(\mathsf {EXP_{st}}\) call.

We easily obtain the following result.

Lemma 23

If \(\mathsf {ARCAD}_\mathsf {main}\) is \(C_\mathsf {main}\)-\(\mathsf {IND\text {-}CCA}\)-secure and \(\mathsf {ARCAD}_\mathsf {sub}\) is \(C_\mathsf {sub}\)-\(\mathsf {IND\text {-}CCA}\)-secure, then \(\mathsf {hybrid}\mathsf {ARCAD}\) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\) with \(C_\mathsf {clean}=C^\mathsf {main}_{\mathsf {main},\mathsf {sub}}\).

Proof (sketch)

Footnote 13 Let us assume that \(\Gamma \) is clean in the sense of \(C_\mathsf {clean}\).

Let \((\mathsf {ad},\mathsf {ct})\) be the challenge (or last) message. If \((\mathsf {ad},\mathsf {ct})\) belongs to \(\mathsf {ARCAD}_\mathsf {main}\), then \(\mathsf {main}(\Gamma )\) is \(C_\mathsf {main}\)-clean. The outcome of \(\mathsf {main}(\Gamma )\) and \(\Gamma \) is the same. Due to the \(C_\mathsf {main}\)-\(\mathsf {IND\text {-}CCA}\) security of \(\mathsf {ARCAD}_\mathsf {main}\), the advantage in \(\Gamma \) is negligible. Let us now assume that \((\mathsf {ad},\mathsf {ct})\) belongs to \(\mathsf {ARCAD}_\mathsf {sub}\).

\(C_{C_\mathsf {main}}^{e,c}\) indicates if the \(\mathsf {ARCAD}_\mathsf {main}\) message of pair (ec) can be replaced by the encryption of something random to produce the same result, except with negligible probability. In this case, \(\mathsf {sub}_{e,c}(\Gamma )\) produces the same outcome as \(\Gamma \) and \(C_\mathsf {clean}\) implies that it must be \(C_\mathsf {sub}\)-clean. Due to the \(C_\mathsf {sub}\)-\(\mathsf {IND\text {-}CCA}\) security of \(\mathsf {ARCAD}_\mathsf {sub}\), the advantage in \(\Gamma \) is negligible.

Similarly, if \(C_{C_\mathsf {main}}^{e,c}(\Gamma )\) does not hold, \(C_\mathsf {clean}\) implies that \(\mathsf {sub}'_{e,c}(\Gamma )\) is clean. It produces the same outcome as \(\Gamma \). Due to the \(C_\mathsf {sub}\)-\(\mathsf {IND\text {-}CCA}\) security of \(\mathsf {ARCAD}_\mathsf {sub}\), the advantage in \(\Gamma \) is negligible.    \(\square \)

In the \(\mathsf {FORGE}\) game, we replace the \(C_\mathsf {trivial}\) predicate. Typically, by taking \(C_\mathsf {main}\) as the predicate that tests if the last \((\mathsf {ad},\mathsf {ct})\) message is a trivial forgery and by taking \(C_\mathsf {sub}\) as the predicate that additionally tests if no \(\mathsf {EXP_{st}}\) occurred, the \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\) predicate defines a new \(\mathsf {FORGE}\) notion for \(\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {DV},\mathsf {EtH})\). More generally, if \(\mathsf {ARCAD}_\mathsf {main}\) is \(C_\mathsf {main}\)-\(\mathsf {FORGE}\)-secure and \(\mathsf {ARCAD}_\mathsf {sub}\) is \(C_\mathsf {sub}\)-\(\mathsf {FORGE}\)-secure, we would like to have \(C^{C_\mathsf {clean}}_{C_\mathsf {main},C_\mathsf {sub}}\)-\(\mathsf {FORGE}\)-security.

Fig. 7.
figure 7

Relaxed \(\mathsf {FORGE}\) Security.

We almost have the reduction but there is something missing. Namely, a forgery for \(\mathsf {hybrid}\mathsf {ARCAD}\) in \(\Gamma \) may not be a forgery for neither \(\mathsf {ARCAD}_\mathsf {main}\) in \(\mathsf {main}(\Gamma )\) nor \(\mathsf {ARCAD}_\mathsf {sub}\) in \(\mathsf {sub}_{e,c}(\Gamma )\). This happens if the adversary in \(\Gamma \) drops the delivery of the last messages in a \(\mathsf {sub}\) scheme. We relax \(\mathsf {FORGE}\)-security using the \(\mathsf {FORGE}^*\) game in Fig. 7. Only Steps 4 and 8 are new. Our \(\mathsf {chain}\) strengthening in Sect. 3 can later make the protocols fully \(\mathsf {FORGE}\)-secure. We easily prove the following result.

Lemma 24

If \(\mathsf {ARCAD}_\mathsf {main}\) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure and \(C_\mathsf {main}\)-\(\mathsf {FORGE}^*\)-secure and if \(\mathsf {ARCAD}_\mathsf {sub}\) is \(C_\mathsf {sub}\)-\(\mathsf {FORGE}^*\)-secure, then \(\mathsf {hybrid}\mathsf {ARCAD}\) is \(C_\mathsf {hybrid}\)-\(\mathsf {FORGE}^*\), where \(C_\mathsf {hybrid}=C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\).

Proof (sketch)

Footnote 14 If \((\mathsf {ad},\mathsf {ct})\) belongs to \(\mathsf {ARCAD}_\mathsf {main}\) and \(\Gamma =\mathsf {FORGE}^*\) succeeds to return 1, then \(C_\mathsf {main}(\mathsf {main}(\Gamma ))\) holds and \(\mathsf {main}(\Gamma )\) succeeds to return 1 as well. Similarly, if \((\mathsf {ad},\mathsf {ct})\) belongs to \(\mathsf {ARCAD}_\mathsf {sub}\) and \(\Gamma \) returns 1, then, depending on \(C_\mathsf {clean}^{e,c}(\Gamma )\), either \(C_\mathsf {sub}(\mathsf {sub}_{e,c}(\Gamma ))\) or \(C_\mathsf {sub}(\mathsf {sub}'_{e,c}(\Gamma ))\) holds, and either game succeeds to return 1 (thanks to \(\mathsf {IND\text {-}CCA}\) security in the latter case). Applying \(\mathsf {FORGE}^*\) security of those protocols, this occurs with negligible probability.    \(\square \)

What \(\mathsf {FORGE}^*\) security does not guarantee is that some forgeries in a sub-scheme may occur in the far future, due to state exposure. Fortunately, our protocol mitigates this problem by making sure that old sub-protocols become obsolete. Indeed, our protocol makes sure that sent messages always have an increasing sequence of (ec) pairs, and the same for received messages. Hence, we cannot have a forgery with an old (ec) pair. Another problem which is explicit in Step 8 of the game is that the adversary may prevent P from receiving a sequence \(\mathsf {seq}_2\) sent from \(\overline{P}\) (namely in a sub-protocol). In Sect. 3, making the protocol \(\mathsf {r\text {-}RECOVER}\)-secure fixes both problems. (See Lemma 26.) Hence, we will obtain \(\mathsf {FORGE}\)-security.

4.4 Security-Aware Hybrid Construction

In this section, we apply our results from Sect. 3.3 to our hybrid constructions.

Lemma 25

Let \(C_\mathsf {clean}\in \{C_\mathsf {trivial},C_\mathsf {noexp}\}\) and \(\mathsf {ARCAD}_1=\mathsf {chain}(\mathsf {ARCAD}_0)\). If \(\mathsf {ARCAD}_0\) is \(C_\mathsf {clean}\)-\(\mathsf {FORGE}\)-secure (resp. \(C_\mathsf {clean}\)-\(\mathsf {FORGE}^*\)-secure), then \(\mathsf {ARCAD}_1\) is \(C_\mathsf {clean}\)-\(\mathsf {FORGE}\)-secure (resp. \(C_\mathsf {clean}\)-\(\mathsf {FORGE}^*\)-secure).

Proof

We reduce an adversary playing the \(\mathsf {FORGE}\) game with \(\mathsf {ARCAD}_1\) to an adversary playing the \(\mathsf {FORGE}\) game with \(\mathsf {ARCAD}_0\) by simulating the hashings. \(\mathsf {ARCAD}_1\) is an extension of \(\mathsf {ARCAD}_0\) such that an \(\mathsf {ARCAD}_1\) message \((\mathsf {ad},(\mathsf {ct}',h,\mathsf {ack}))\) is equivalent to an \(\mathsf {ARCAD}_0\) message \(((\mathsf {ad},h,\mathsf {ack}),\mathsf {ct}')\). It is just reordering \((\mathsf {ad},\mathsf {ct})\). Hence, a forgery for \(\mathsf {ARCAD}_1\) must be a forgery for \(\mathsf {ARCAD}_0\). \(\mathsf {FORGE}^*\)-security works the same.    \(\square \)

Lemma 26

Given \(\mathsf {ARCAD}_\mathsf {main}\) and \(\mathsf {ARCAD}_\mathsf {sub}\), let

$$ \mathsf {ARCAD}_0=\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {main},\mathsf {ARCAD}_\mathsf {sub}) \;,\; \mathsf {ARCAD}_1=\mathsf {chain}(\mathsf {ARCAD}_0) $$

If \(\mathsf {ARCAD}_\mathsf {main}\) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure and \(C_\mathsf {main}\)-\(\mathsf {FORGE}^*\)-secure and \(\mathsf {ARCAD}_\mathsf {sub}\) is \(C_\mathsf {sub}\)-\(\mathsf {FORGE}^*\)-secure, then \(\mathsf {ARCAD}_1\) is \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\)-\(\mathsf {FORGE}^*\)-secure. If H is additionally collision-resistant, then \(\mathsf {ARCAD}_1\) is \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\)-\(\mathsf {FORGE}\)-secure.

Proof

Due to Lemma 24, \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\)-\(\mathsf {FORGE}^*\)-security works like in the previous result. To extend to \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\)-\(\mathsf {FORGE}\)-security, we just observe that \(\mathsf {ARCAD}_1\) is \(\mathsf {r\text {-}RECOVER}\)-secure due to Lemma 18. We thus deduce \(\mathsf {seq}_2=\bot \) from having \(\mathsf {receive}^P_\mathsf {ct}=(\mathsf {seq}_1,(\mathsf {ad},\mathsf {ct}))\) and \(\mathsf {sent}^{\overline{P}}_\mathsf {ct}=(\mathsf {seq}_1,\mathsf {seq}_2,(\mathsf {ad},\mathsf {ct}),\mathsf {seq}_3)\). Hence, we have a full forgery, except with negligible probability.    \(\square \)

Lemma 27

Let \(C_\mathsf {clean}=C_\mathsf {leak}\), \(C_\mathsf {ratchet}\), \(C_\mathsf {noexp}\), or \(C_{t\mathsf {forge}}^S\) (\(t=\mathsf {trivial}\) or \(\bot \}\), \(S=P_\mathsf {test}\) or \(\{A,B\}\)), If \(\mathsf {ARCAD}_0 \) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure, then \(\mathsf {ARCAD}_1\) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure.

Proof

We reduce an adversary playing the \(\mathsf {IND\text {-}CCA}\) game with \(\mathsf {ARCAD}_1\) to an adversary playing the \(\mathsf {IND\text {-}CCA}\) game with \(\mathsf {ARCAD}_0\) by simulating the hashings. We easily see that the cleanness is the same and that the simulation is perfect.    \(\square \)

We easily extend this result to hybrid constructions. We conclude with our final result.

Theorem 28

Given \(\mathsf {ARCAD}_\mathsf {main}\) and \(\mathsf {ARCAD}_\mathsf {sub}\), let

$$ \mathsf {ARCAD}_0=\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {main},\mathsf {ARCAD}_\mathsf {sub}) \;,\; \mathsf {ARCAD}_1=\mathsf {chain}(\mathsf {ARCAD}_0) $$

We assume that 1. H is collision-resistant; 2. \(\mathsf {ARCAD}_\mathsf {main}\) is \(C_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure and \(C_\mathsf {main}\)-\(\mathsf {FORGE}^*\)-secure; 3. \(\mathsf {ARCAD}_\mathsf {sub}\) is \(C_\mathsf {sub}\)-\(\mathsf {FORGE}^*\)-secure and \(C'_\mathsf {clean}\)-\(\mathsf {IND\text {-}CCA}\)-secure. Then, \(\mathsf {ARCAD}_1\) is 1. \(\mathsf {r\text {-}RECOVER}\)-secure, 2. \(\mathsf {s\text {-}RECOVER}\)-secure, 3. \(C^\mathsf {clean}_{\mathsf {main},\mathsf {sub}}\)-\(\mathsf {FORGE}\)-secure, 4. \(C^\mathsf {clean}_{\mathsf {clean},\mathsf {clean}'}\)-\(\mathsf {IND\text {-}CCA}\)-secure, 5. with acknowledgement extractor.

Corollary 29

Let \(\mathsf {ARCAD}_1=\mathsf {chain}(\mathsf {hybrid}(\mathsf {ARCAD}_\mathsf {DV},\mathsf {EtH}))\) (where \(\mathsf {ARCAD}_\mathsf {DV}\) is defined on Fig. 11) and let \(C_\mathsf {clean}=C_\mathsf {leak}\wedge C_\mathsf {forge}^{A,B}\). With the assumptions from Theorem 30 and the \(\mathsf {EtH}\) result [13, Th.2], if H is collision-resistant, \(\mathsf {ARCAD}_1\) is \(C^\mathsf {clean}_{\mathsf {trivial},\mathsf {noexp}}\)-\(\mathsf {FORGE}\)-secure, \(C^\mathsf {clean}_{\mathsf {clean},\mathsf {sym}}\)-\(\mathsf {IND\text {-}CCA}\)-secure, and with security-awareness.

In particular, when a sender deduces an acknowledgment for his message m from a received message \(m'\), if he can make sure that \(m'\) is genuine and that no trivial exposure for m happened, then he can be sure that his message m is private, no matter what happened before or what will happen next.

5 Conclusion

We revisited the \(\mathsf {DV}\) security model. We proposed an hybrid construction which would mostly use \(\mathsf {EtH}\) and occasionally a stronger protocol, upon the choice of the sender, thus achieving on-demand ratcheting. Finally, we proposed the notion of security awareness to enable participants to have a better idea on the safety of their communication. We achieved what we think is the optimal awareness. Concretely, a participant is aware of which of his messages arrived to his counterpart when he sent the last received one. We make sure that any forgery (possibly due to exposure) would fork the chain of messages which is seen by both participants and result in making them unable to continue communication. We also make sure that assuming that the exposure history is known, participants can deduce which messages leaked.