Hugo Beguinet
email: hugo.beguinet@ens.fr

Céline Chevalier
email: celine.chevalier@ens.fr

Thomas Ricosset
email: thomas.ricosset@thalesgroup.com

Hugo Senet
email: hugo.senet@ens.fr

Formal Verification of a Post-Quantum Signal Protocol with Tamarin

Keywords: Secure instant messaging, Signal protocol, Quantum resistant, Formal verification, Tamarin prover, X3DH, Double ratchet

The Signal protocol is used by billions of people for instant messaging in applications such as Facebook Messenger, Google Messages, Signal, Skype, and WhatsApp. However, advances in quantum computing threaten the security of the cornerstone of this protocol: the Diffie-Hellman key exchange. There actually are resistant alternatives, called post-quantum secure, but replacing the Diffie-Hellman key exchange with these new primitives requires a deep revision of the associated security proof. While the security of the current Signal protocol has been extensively studied with hand-written proofs and computerverified symbolic analyses, its quantum-resistant variants lack symbolic security analyses.

In this work, we present the first symbolic security model for post-quantum variants of the Signal protocol. Our model focuses on the core state machines of the two main sub-protocols of Signal: the X3DH handshake, and the so-called double ratchet protocol. Then we show, with an automated proof using the Tamarin prover, that instantiated with the Hashimoto-Katsumata-Kwiatkowski-Prest postquantum Signal's handshake from PKC'21, and the Alwen-Coretti-Dodis KEMbased double ratchet from EUROCRYPT'19, the resulting post-quantum Signal protocol has equivalent security properties to its current classical counterpart.

Introduction

The Signal protocol is divided into two sub-protocols: X3DH [START_REF] Perrin | The x3dh key agreement protocol[END_REF], and the double ratchet protocol [START_REF] Perrin | The double ratchet algorithm[END_REF]. The X3DH protocol can be seen as an Authenticated Key Exchange (AKE) protocol. It ensures the authenticity of an initial key shared between two users. It is an asynchronous protocol, which means that there is no need for users to be online at the same time to initialize the protocol. To use the X3DH protocol, each user must first generate a long-term static pair of public and private keys for them to be authenticated, as well as a batch of ephemeral pairs of public and private keys. Both long-term public keys and ephemeral key batches are then stored on an honest intermediate server which acts as a buffer. When Bob wants to start a conversation with Alice, he sends a request to the server, and then receives the Alice's long-term public key and a fresh Alice's ephemeral public key from her batch. These two public keys enable Bob to perform the X3DH handshake protocol by sending a message to Alice, which will enables her to derive their X3DH pre-shared secret key when she is online.

The double ratchet protocol is used to encrypt messages to send through the Signal protocol with an Authenticated Encryption with Associated Data (AEAD) scheme and a session key that is shared between the two parties. The session key is renewed each time a message is sent, using symmetric and asymmetric mechanisms called ratchets. The double ratchet protocol is initialized with the X3DH pre-shared key as session key, and an ephemeral public key from the corresponding batch as public key. Then, to send a message, the public key is used to exchange a fresh secret key, from which the new session key is derived with the output of a one-way function applied to the current session key. In addition, a new ephemeral key pair is generated whose public key is encrypted then sent with the message, using this new session key. This protocol is repeated for each message sent to ensure strong security properties such as forward secrecy and post-compromise recovery against passive adversaries.

The current Signal protocol heavily uses the well-known, flexible, and efficient, but vulnerable to quantum attacks, Diffie-Hellman (DH) key exchange protocol. However, with the threat of upcoming quantum computers, post-quantum alternatives are subject to extensive analysis in order to gain assurance in their security. In 2016, the NIST initiated a process to evaluate and standardize quantum-resistant key-establishment and signature schemes, but all remaining candidates in the key-establishment category are key encapsulation mechanisms (KEMs) like RSA, and not key exchanges like DH. Consequently, the integration of post-quantum KEMs in cryptographic protocols is quite challenging due to the differences between KEMs and DH, which requires some fundamental adjustments to these protocols to maintain the same security guarantees.

Aside from that, the active area of formal protocol verification is increasingly accompanying protocol specifications. Designing cryptographic protocols is known to be hard to get right and hand-written proofs remain highly complex and error-prone. At the design level, automatic verification aims to manage the complexity of security proofs and even reveal subtle flaws or as-yet-unknown attacks as the historic example of the man-in-the-middle attack [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using FDR[END_REF]. Efficient automatic verification tools as Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] or ProVerif [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF] have been used to analyze large, real-world protocols. For instance, ProVerif has been used to analyze TLS 1.3 [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF] and Signal [START_REF] Kobeissi | Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach[END_REF] and Tamarin as been used to analyze the 5G AKE protocol [START_REF] Basin | A formal analysis of 5g authentication[END_REF] and TLS 1.3 [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1[END_REF].

Related Works. The security of the (EC)DH-based Signal protocol has been extensively studied using hand-written proofs [START_REF] Cohn-Gordon | A formal security analysis of the signal messaging protocol[END_REF]. Those proofs were completed with a symbolic analysis [START_REF] Kobeissi | Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach[END_REF] using the ProVerif prover. Regarding the transition to post-quantum cryptography, there are KEM-based alternatives to the Signal sub-protocols X3DH [START_REF] Hashimoto | An efficient and generic construction for signal's handshake (X3DH): post-quantum, state leakage secure, and deniable[END_REF][START_REF] Brendel | Towards post-quantum security for signal's X3DH handshake[END_REF] (the security properties in [START_REF] Hashimoto | An efficient and generic construction for signal's handshake (X3DH): post-quantum, state leakage secure, and deniable[END_REF] being closer to that of X3DH, in particular thanks to the encryption of the signature) and double ratchet [START_REF] Alwen | The double ratchet: Security notions, proofs, and modularization for the Signal protocol[END_REF], with hand-written proofs for the same security properties as the current Signal protocol. Such KEM-based protocols can be instantiated with post-quantum KEMs from the NIST competition such as Kyber [START_REF] Avanzi | CRYSTALS-Kyber -Submission to round 3 of the NIST post-quantum project[END_REF], which will be the first NIST PQC standard for key-establishment. However, those potential replacements for X3DH and double ratchet have so far lacked computer-verified symbolic analyses which results in a limited trust in these protocols. By contrast, some other protocols, such as WireGuard [START_REF] Hülsing | Post-quantum Wire-Guard[END_REF] and (KEM)TLS [START_REF] Schwabe | Post-quantum TLS without handshake signatures[END_REF][START_REF] Celi | A tale of two models: Formal verification of KEMTLS via Tamarin[END_REF], already have computerverified symbolic analyses for post-quantum variants, both using the Tamarin prover.

Contributions. We present the first symbolic proof of a post-quantum variant of the Signal protocol. Our model focuses on the core state machines of the two main subprotocols of this variant: the Hashimoto-Katsumata-Kwiatkowski-Prest post-quantum X3DH handshake [START_REF] Hashimoto | An efficient and generic construction for signal's handshake (X3DH): post-quantum, state leakage secure, and deniable[END_REF] which we refer to as PQ-X3DH, and the Alwen-Coretti-Dodis KEM-based double ratchet [START_REF] Alwen | The double ratchet: Security notions, proofs, and modularization for the Signal protocol[END_REF] that we call KEM-Double-Ratchet. Then we show, using the Tamarin prover, that these two protocols meet the same security properties as classical X3DH and double ratchet protocols. In addition, we prove the well-formedness of the two models, which informally means that their behavior is as expected.

Our PQ-X3DH Tamarin symbolic analysis ensures the integrity of the two exchanged messages, the authentication of users, the resistance to unknown key-share attacks and replay attacks, and other properties, such as the weak forward secrecy [START_REF] Krawczyk | HMQV: A high-performance secure diffie-hellman protocol[END_REF] and the key compromise attack resistance, to mitigate the leak of secret information.

With regard to KEM-Double-Ratchet, our Tamarin model ensures the integrity of all the messages, the forward secrecy, and the post-compromise recovery [START_REF] Alwen | The double ratchet: Security notions, proofs, and modularization for the Signal protocol[END_REF]. It is worth noting that in the particular case of Signal, post-compromise recovery is met only if the adversary is passive during the recovering process. While within the double ratchet protocol two parties can exchange a potentially infinite number of messages, we model only three exchanges, which represents the minimum number of exchanges for each security property to hold. A simple induction argument then enables us to generalize these properties to any number of exchanges. To our knowledge, our formal verification model is the first one that covers the post-compromise recovery security property.

Outline. In section 2 we present the two sub-protocols of the considered variant of the Signal protocol and their Tamarin model. Then we present in section 3 the Tamarin formalism used in our symbolic analysis, the different security properties verified, and the results of our formal verification.

A KEM-Based Signal Protocol

In this section, we describe the KEM-based variant of the Signal protocol that is the subject of our symbolic analysis. As explained in the introduction, the Signal protocol is separated in two sub-protocols providing different functionalities, we respect this separation for this KEM-based variant in order to facilitate its analysis and clearly identify the contribution of each sub-protocol in the security of the whole protocol. The first sub-protocol named PQ-X3DH is used as authenticated key agreement while the second one named KEM-double-ratchet is used for secure instant messaging by refreshing the session key at each time a message is sent.

The PQ-X3DH Protocol

Alice

Bob Public Parameters : (s, pp KEM , pp wKEM , pp Sig )

lpk A ={epk A , ltpk A } lsk A ={esk A , ltk A } lpk B ={epk B , ltpk B } lsk B ={esk B , ltk B } (epk T , esk T ) ← -wKEM.KeyGen(pp wKEM ) Init: epk T (K, C) ← -KEM.Encap(epk A ) (K T , C T ) ← -wKEM.Encap(epk T ) sid B := ltpk A ||ltpk B ||lpk A ||epk T ||C||C T ||K kroot|| k ← -HKDF(K T , sid B ) σ ← -S.Sign(ltk B , sid B ) c ← -AEAD.Enc(σ, k) Respond: C, C T , c K ← -KEM.Decap(esk A , C) K T ← -wKEM.Decap(esk T , C T ) sid A := ltpk A ||ltpk B ||lpk A ||epk T ||C||C T ||K kroot|| k ← -HKDF(K T , sid A ) σ ← -AEAD.Dec(c, k) S.Verify(ltpk B , sid A , σ) ? = 1
Fig. 1. The PQ-X3DH protocol.

X3DH [START_REF] Perrin | The x3dh key agreement protocol[END_REF] is an asynchronous protocol that generates a shared secret between the communicating parties to initialize their communication as well as authenticate themselves. It fully authenticates the receiver Bob and partially authenticates the initiator Alice. It is called asynchronous because both parties can initiate the connection while the other is offline. Such property provides flexibility but could completely break the protocol in the case of a malicious server. Apart from such a case the asynchronous protocol is highly secure. We consider here the PQ-X3DH presented in [START_REF] Hashimoto | An efficient and generic construction for signal's handshake (X3DH): post-quantum, state leakage secure, and deniable[END_REF] which preserve the security properties of the classical protocol and we focus on the variant of PQ-X3DH that does not use a signature to fully authenticate Alice. The motivation for this change is to allow Alice to deny having taken part in the exchange, in the same way that Bob can deny it thanks to the encryption of his signature.

The PQ-X3DH sub-protocol is presented in Figure 1. Two key encapsulation mechanisms, KEM and wKEM, are employed as building blocks in this key agreement protocol. wKEM, which is IND-CPA secure, is for ephemeral use. KEM is IND-CCA secure here. Tamarin considers the public-key encryption as ideal (thus IND-CCA), but for an ephemeral use, IND-CPA is sufficient. Tamarin model. Since Tamarin has no built-in KEM we replace the KEM with an asymmetric encryption scheme encrypting a fresh ephemeral key. The two approaches are equivalent considering the idealization of cryptographic primitives used in Tamarin. Our model for the PQ-X3DH protocol is represented as the state machine in Figure 2 with nine transition rules:

PP PKI

A Init A Recv A End B Init B End Init A A B Send A Recv Init B B Recv
-PKI and PP: these rules formalize the Public Key Infrastructure (PKI), the Public Parameters (PP). PKI assigns only once a long term key with an ephemeral key to a user. Instead of handling non-replayability with a batch of ephemeral one-time keys we directly use restrictions to ensure the a key can only be used once. -Init_A and Init_B: each user get from PKI and PP the public parameters and public keys needed for the PQ-X3DH protocol. -A_B_Send: Alice sends an ephemeral public key to initiate a key encapsulation.

-B_Recv_Then_Send: Bob receives Alice's ephemeral public key, encapsulates two secret keys into two KEM ciphertexts, one with Alice's ephemeral public key and wKEM, the other by using Alice's long-term public key and KEM. Bob also sign the protocol transcript and send his signature encrypted with an AEAD scheme.

-A_Recv: Alice receives Bob's ciphertext and signature and derives a session key that will be used by Alice and Bob to communicate. Then, she decrypts and verifies the signature. -RevealE: Reveals to the attacker the ephemeral secret keys.

-RevealL: Reveals to the attacker the long-term secret keys.

The KEM-double-ratchet Protocol

The double ratchet protocol (DR for short) is used for securing an ongoing exchange of messages between two peers by repeatedly producing fresh session keys while saving the authentication made with the PQ-X3DH initialization.

This protocol is self-healing, which means that it is made so that if at some point a user's key is intercepted by an attacker, the upcoming renewal of the session key is there to protect the secrecy of the future messages. This property is sometimes called postcompromise security. To satisfy this property, a cryptographic ratchet based on a key exchange method, such as Diffie-Hellman in the classical case, is used in the protocol, and a ratchet based on key derivation functions enables key renewal without interaction between the peers.

In order to communicate securely, the double ratchet protocol derives three types of shared secrets: root, chain and message secrets. They are used respectively as master, derivation and a message keys [START_REF] Perrin | The double ratchet algorithm[END_REF]. Since we consider a KEM-based double ratchet, we deviate a bit from this definition. As specified in Figure 3, in KEM-Double-Ratchet the two communicating peers Alice and Bob start the KEM-DR sub-protocol with a common pre-shared key k root . This key comes from the key agreement protocol PQ-X3DH.

Tamarin model. As shown in Figure 4 we only perform three exchanges of the KEMdouble-ratchet protocol. Three exchanges are sufficient to verify all considered security properties as discussed in section 3. Our KEM-DR model has nine transition rules:

-Init_A and Init_B: each user get a secret preshared key and Bob gets an Alice's KEM ephemeral public key. -Send_B1, Send_A, and Send_B2: the user encapsulates a fresh secret key with the current KEM public key, derives a new session key, encrypts the message, then sends it encrypted with the KEM ciphertext and a new ephemeral KEM public key. -Recv_A1, Recv_B, and Recv_A2: the user receives a message, derives the new session key, and verifies the integrity. -LeakState: Reveals to the attacker the current user secrets.

Tamarin Formal Verification

In Tamarin, a protocol is seen as a state machine. A state is a multiset of facts, and rules are transitions which shift the state when some conditions are fulfilled. A rule consists of three sets of facts: premise, action facts, and conclusion. If all the premise Alice Bob External Key Agreement :

k root epk A,1 f etch ← ----KeyBatch[Alice] esk A,1 r d = k root r d = k root (K T , C)← -wKEM.Encaps(epk A,1 ) (r d , k d ) ← -HKDF(r d , K T ) K T ← -Hash(k d ) (epk B,2 , esk B,2 ) ← -wKEM.Keygen() E ← -AEAD.Enc(K T ,(ts,m)) Send : (C ,epk B,2 ), E K T = wKEM.Decaps(C, esk A,1 ) (m, ts) ← -AEAD.Dec(K T , E) (r d , k d ) ← -HKDF(r d , K T ) K T ← -Hash(k d ) Verify: ts exchange 1 (K T , C)← -wKEM.Encaps(epk B,2 ) (r d , k d ) ← -HKDF(r d , K T ) K T ← -Hash(k d ) (epk A,3 , esk A,3 ) ← -wKEM.Keygen() E ← -AEAD.Enc(K T ,(ts,m)) Send : (C ,epk A,3 ), E K T = wKEM.Decaps(C, esk B,2 ) (m, ts) ← -AEAD.Dec(K T , E) (r d , k d ) ← -HKDF(r d , K T ) K T ← -Hash(k d )
Verify: ts exchange 2

(K T , C)← -wKEM.Encaps(epk A,3 ) (r d , k d ) ← -HKDF(r d , K T ) K T ← -Hash(k d ) (epk B,4 , esk B,4 ) ← -wKEM.Keygen() E ← -AEAD.Enc(K T ,(ts,m)) Send : (C ,epk B,4 ), E K T = wKEM.Decaps(C, esk A,3 ) (m, ts) ← -AEAD.Dec(K T , E) (r d , k d ) ← -HKDF(r d , K T ) K T ← -Hash(k d )
Verify: ts exchange 3 Fig. 3. The KEM-double-ratchet protocol. facts exist, then the rule is applied. Applying a rule means consuming premise facts to produce conclusion facts while recording action facts in the protocol trace.

A Init A Recv A Send A End B Init B Send B Recv B End Init A Recv A1 Send A Recv A2 Init B Send B1 Recv B Send B2
Some facts are native in Tamarin such as In() and Out() to model inputs and outputs of the protocol following the Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF]. Moreover, the Fr() fact is used to produce fresh or unique variables.

Tamarin proposes a set of built-ins cryptographic primitives to model protocols, including symmetric and asymmetric encryption, hash function, and signature. It also allows to define new primitives, via functions and equations commands. In the context of this work, we define a KEM as an asymmetric encryption scheme encrypting a fresh random key, and we consider the following AEAD Tamarin formalization from [START_REF] Hülsing | Post-quantum Wire-Guard[END_REF].

In some cases, we need to restrict some transitions in the protocol, e.g., to check the equality of two terms as shown below. Hence, when a rule has the restriction Eq(x,y) in its action facts, then the rule is applied if and only if x = y. restriction Eq: "All x y #i. Eq(x,y) @ #i ==> x = y" Tamarin uses the logic of first order to formalize security properties as lemmas. The keyword All stands for ∀, Ex for ∃ and @ represents a marker for chronological events. Lemmas use action facts produced by the rules to prove or disprove properties. A trivial lemma is given below, it means that if Action1() happened then Action2() happened too.

lemma example:

" All x #i. Action1(x) @ #i ==> Ex y #k. Action2(y) @ #k "

In order to verify that a protocol has given security property, Tamarin takes as input the protocol model, with all its possible transitions as rules, and a lemma corresponding to this security property. Then, if Tamarin completes its verification process, it will either output a proof of the property or an attack trace which falsifies it.

Security Properties

The security properties verified in our symbolic analysis of PQ-X3DH and KEM-DR are the same properties as those considered in the formal verification of classical X3DH and Double-Ratchet protocols [START_REF] Kobeissi | Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach[END_REF].

Integrity. Integrity is an important property for key exchange protocols. It allows the receiver of a message to have the assurance that the message has come unaltered from the intended sender. We separate the integrity of a message that can be verified upon receipt, called instantaneous integrity, and that which can be verified upon receipt of a subsequent message, called delayed integrity.

Authentication. We consider two authentication notions: the partial authentication from definition 1 and the full authentication from defintion 2.

Definition 1 (Partial Authentication).

A user U is partially authenticated to another user V if V can prove that the message she receives comes from the same user as the one with whom she has initialized the session.

Definition 2 (Full Authentication).

A user U is fully authenticated to another user V if U is partially authenticated to V and V can prove the identity of U. Forward Secrecy. Here again we consider two different notions: the perfect Forward Secrecy (FS) from definition 3 and the weak Forward Secrecy (wFS) from definition 4. In this work, we also consider a new notion called weak state Forward Secrecy (wsFS) that we define as the wFS property except that the leakage concerns states instead of long term keys. Definition 3 (perfect Forward Secrecy (FS) [START_REF] Menezes | Handbook of Applied Cryptography[END_REF]). A protocol is said to have perfect forward secrecy if compromised long-term keys does not compromise past session keys. Definition 4 (weak Forward Secrecy (wFS) [START_REF] Krawczyk | HMQV: A high-performance secure diffie-hellman protocol[END_REF]). Any session key established by uncorrupted parties without active intervention by the attacker is guaranteed to remain secrete even if the parties to the exchange are corrupted after the session key has been erased.

Key Compromise Impersonation Resistance. The KCI resistance from definition 5 is related to the use of long term public/private keys. Since there is no use of long term public/private key in the KEM-DR protocol, the KCI property is only applicable to the PQ-X3DH protocol.

Definition 5 (Key Compromise Impersonation (KCI) Resistance). Even if an adversary compromises the long term private key of a user U, this adversary can not use this key to impersonate (to U) another user V that is communicating to U.

Unknown Key-Share Resistance. We recall the definition of a UKS attack in definition 6. UKS attacks can be seen as implicit impersonation. Thus, in the same way as for the KCI resistance, this property is only applicable to the PQ-X3DH protocol.

Definition 6 (Unknown Key-Share (UKS) attack [START_REF] Blake-Wilson | Unknown key-share attacks on the station-to-station (STS) protocol[END_REF]). An unknown key-share attack on an AKE protocol is an attack whereby a user U ends up believing she shares a key with V, and although this is in fact the case, V mistakenly believes the key is instead shared with an entity W U.

Post-Compromise Recovery. We recall the post-compromise recovery property in definition 7. By definition, this property is only applicable when a protocol is iterated repeatedly between the parties, this is the case for KEM-DR but not for PQ-X3DH.

Definition 7 (Post-Compromise Recovery (PCR) [START_REF] Alwen | The double ratchet: Security notions, proofs, and modularization for the Signal protocol[END_REF]). If the attacker remains passive, i.e., the attacker does not inject any messages, and if users have access to fresh randomness, then the users recover a secure state from a compromised state after a few communication rounds.

Tamarin Formalization

Before describing in more detail the Tamarin formalization of the different security properties presented above, we need to define some notations that will be useful later. In the rest of the paper, we use the following notations:

-L = {0, 1, 2} is the set of iteration indices, i.e., the three first exchanges ; -M ⊂ {0, 1} * is the set of messages sent via the Signal protocol ; -K ⊂ {0, 1} k is the set of secret keys where k is the key length ; -S ⊂ {0, 1} * is the set of message indices, i.e., the message numbers ; -Σ is the set of protocol states.

-Γ is the set of user states. Moreover, using the Tamarin formalism, we note:

-KU(x): The adversary sent x and therefore has knowledge of x ; -K(x): The adversary has knowledge of x.

In Table 1, respectively Table 2, we introduce the Tamarin action facts and their abbreviations needed in our symbolic analysis of PQ-X3DH, respectively KEM-DR. These action facts are used to define the Tamarin lemmas corresponding to the security properties. In Tamarin, the user state is the current set of the secrets of this user. In order to characterize respectively full and partial knowledge of the user's secrets by the attacker, we define the revealed state in definition 8 and the compromised state in definition 9.

Definition 8 (Revealed State).

A state is said to be revealed if the adversary has knowledge of every hidden elements of the state.

Definition 9 (Compromised State).

A state is said to be compromised if the adversary has knowledge of any hidden element of the state.

PQ-X3DH Security Properties. For the sake of clarity, we describe the security properties verified with Tamarin in the usual mathematical formalism. Let E = A < t B the notation < t means that E is true if and only if event A occurs before event B. For lack of space, the definitions of the corresponding Tamarin lemmas are presented in the full version of this paper.

Integrity. The integrity is checked on both messages transmitted through the PQ-X3DH protocol. Nothing in this protocol allows an immediate integrity check of the first transmitted message. However, if both parties share the same key at the end of the protocol, then the integrity of this message is ensured in a delayed manner. For this reason, we define the following condition under which the delayed integrity of the first message is assured:

The following properties insure, for any user A, B that have shared a common secret k by respectively sending message m 1 and receiving message m 2 on the first exchange, that m 1 = m 2 . Which leads with Tamarin formalism too:

∀A, B ∈ U, ∀m 1 , m 2 ∈ M, ∀k ∈ K. S A (A,B,k) ∧ S B (B,A,k) ∧ Send A,1 (m 1 ) ∧ Recv B,A,1 (m 2 ) =⇒ m 1 = m 2 .
The integrity of the second message can be immediately verified thanks to the signature. Thus the condition to check the immediate integrity is modeled as: For any user A and B, any message m 1 , m 2 if in the second flow of the exchange B sent m 1 and A received m 2 without any corruption of the long term key of B and ephemeral key of A before the reception of the second flow by A then m 1 = m 2 . Which leads to the following Tamarin formalism:

∀A, B ∈ U, ∀m 1 , m 2 ∈ M. Send B,2 (m 1 ) ∧ Recv A,B,2 (m 2 )∧ ∧ ¬ R E (A) ≤ t Recv A,B,2 (m 2 ) ∧ ¬ R L (B) ≤ t Recv A,B,2 (m 2 ) =⇒ m 1 = m 2 .
Authentication. We consider two different notions of authentication depending on the role of the user in the PQ-X3DH protocol. Indeed, the initiator, Alice, does not sign any message and her KEM long term key is provided by a server without guaranteeing its authenticity. In these conditions, Alice can only be partially authenticated according to definition 1. In the case where the equivalent of a certificate of the Alice's KEM long term key was added, then she could be fully authenticated at the end of the PQ-X3DH protocol. The second user, Bob, signs the message which allows Alice to explicitly authenticates him under the classical conditions of a public key infrastructure. The following condition is for the full authentication of Bob by Alice:

∀A, B ∈ U. EA(B,A) ≤ t R L (B) =⇒ [SS(B,A) ∧ RC(A,B) ∧ (SC(A) ∧ SS(B,A) ≤ t EA(B,A)) ∧ (SC(A) ≤ t SS(B,A)) ∧ (RC(A,B) = t SS(B,A))] .
This can be described as for any user A and B, if the explicit authentication has been done before any corruption on B's long term key, then the protocol has been honestly executed by A and B.

weak Forward Secrecy. The following condition verifies the wFS property on k root and k keys of the PQ-X3DH protocol in case of future compromise of the initiator's shortterm and responder's signing keys.

∀A, B ∈ U, ∀k ∈ K. ¬R L (B) ≤ t wFS A,B (k 1 , k 2 ) ∧ ¬R E (A) =⇒ ¬KU(k) .
It means that for any user A and B that have agreed on a common key k, if at a certain point no corruption on the long term key of B has happened and if no corruption on the ephemeral key of A has happened then the adversary does not know the common key k. KCI resistance. The only possible scenario in which a KCI attack occurs is when the signing long-term key of the responder is compromised, in this case it must be guaranteed that an attacker cannot use this key to impersonate any of the users. Thus we have the following condition for KCI resistance: In other word if A or B have shared a key k with a user S and if respectively A or B's long term key has been corrupted and if A or B have agreed with respectively B or A on the key k too, then respectively the user S is B or A and cannot another user.

UKS resistance. The UKS resistance consists of ensuring that if two users have agreed on a common session key, then they have the assurance that if neither key is compromised then no other user can impersonate either of them.

∀A, B, C, S ∈ U, ∀k ∈ K. S A (A,S,k) ∧ S B (B,C,k) =⇒ S = B ∧ C = A .
This is a somewhat stronger approach compared to the previous properties that insure that no impersonation will occurs. Double-Ratchet Security Properties. Regarding the KEM-DR protocol, we verify the classical security properties as well as the post-compromise recovery from [START_REF] Alwen | The double ratchet: Security notions, proofs, and modularization for the Signal protocol[END_REF].

Integrity. For each exchange, we verify that the message sent is indeed the message received thanks to the integrity provided by the AEAD scheme. PCR. As this property ensures that for a corruption during a given exchange it is enough to wait for two exchanges before the session key is secret again, it is necessary to check this condition on three consecutive exchanges. Then this base case allows to prove theorem 1 by induction.

∀A, B ∈ U, ∀st ∈ Σ. H A,B (st) ∧ R(B,0) ∧ H A,B (st) < t R(B,0) =⇒ ¬K(st) ∨ R(B,2) ∨ R(A,1) .
As it can be deduced this properties is proven only on the three first messages. This can be proven using Tamarin for any fixed triplet (n, n + 1, n + 2) of ratchet exchange. However for pure theoretical insurance we prove it using induction using this case as the base case of the induction proof.

weak state Forward Secrecy. Similarly, two consecutive exchanges of the KEM-DR protocol are sufficient to prove by induction the wsFS property in theorem 2.

∀A, B ∈ U, ∀st ∈ Σ. FS(A,B,0,st) ∧ R(A,1) ∧ FS(A,B,0,st) < t R(A,1) =⇒ ¬K(st) ∨ R(B,0) .

Formal Verification Results

In Table 3 we present the results obtained from the automatic verification with Tamarin of the security properties considered for the PQ-X3DH and KEM-DR protocols.

-X3DH ✗ ✓ ✓ ✓ ✓ ✗ ✓ NA NA KEM-Double-Ratchet ✓ NA NA NA NA ✓ NA ✓ ✓
Since the KEM-DR protocol admits an arbitrary number of interactions, properties impacting previous or future states of the protocol require an additional proof in order to holds for any exchange of the protocol. Only the PCR and wsFS properties fall in this case, the others are trivially proven. To be more precise Tamarin allows these propreties to be true for any k < n with n fixed. We therefore propose to extend it to arbitrary n by induction for theoretical purposes. Proof. We prove theorem 1 by induction for all integer n > 0. The base case has been proven using Tamarin. Suppose that the theorem is true for all integer k < n, and that: Which ends our induction proof. □

¬
We introduce the notion of healing ball in definition 10 to prove the wsFS property in theorem 2.

Definition 10 (Healing Ball). We define the healing ball B h for all user state S ∈ Γ, as B h (S ) = {γ ∈ Γ | Revealed(γ) =⇒ ¬ Healed(S )}. Proof. We prove theorem 2 by induction for all integer n > 1. The base case has been proven using Tamarin. Suppose that the theorem is true for all integer ℓ ≤ n, and that State n+1 has been compromised. Then, we have:

Compromised(State n+1 ) =⇒ Revealed(State n ) ∨ Revealed(State n+1 )
and by definition, for all ℓ:

Revealed(State ℓ ) =⇒ Compromise(State ℓ )
If State n has been revealed and not State n+1 , we apply the induction hypothesis. Now suppose that State n+1 has been revealed but not State n , we then use the fact that KEM.decaps is supposed ideal by Tamarin and then deterministic, so regarding the backward analysis State n+1 is a deterministic function of State n . Finally, if both states have been revealed, then we apply the induction hypothesis. □

Fig. 2 .

 2 Fig. 2. Graph of the Tamarin PQ-X3DH model.

Fig. 4 .

 4 Fig. 4. Graph of the Tamarin KEM-Double-Ratchet model.

(

  ∀A, B, S ∈ U, ∀k ∈ K.S A (A,S,k) ∧ R L (A) ∧ S B (B,A,k) =⇒ S = B) ∧ (∀A, B, S ∈ U, ∀k ∈ K.S A (A,B,k) ∧ R L (B) ∧ S B (B,S,k) =⇒ S = A) .

  ∀n ∈ S, ∀m 1 , m 2 ∈ M, ∀k ∈ K. I S (n,m 1 ,s) ∧ I R (n,m 2 ,s) ∧ ¬K(k) =⇒ m 1 = m 2 .

Theorem 1 (

 1 KEM-Double-Ratchet Post Compromise Security). For all user state State n with n > 0: Compromised(State n ) ∧ ¬ Revealed(State n+1 ) ∧ ¬ Revealed(State n+2 ) =⇒ Healed(State n+2 ) .

Theorem 2 (

 2 KEM-Double-Ratchet weak state Forward Secrecy). For all user state State n with n ≥ 2:Compromised(State n ) ∧ (∀k < n, S ∈ B h (State k ), ¬ Revealed(S )) =⇒ ¬ Compromised(State k ) .

Table 1 .

 1 Tamarin action facts for PQ-X3DH, abbreviations and definitions

	Action fact Abbreviation Definition
	SessA	S A (A,B,k) A accepts the key k as valid to communicate with B
	ExplicitAuth EA(B,A) A explicitly authenticates B
	RevealL	R L (A)	The long-term key of A is revealed to the attacker
	RevealE	R E (A)	The ephemeral key of A is revealed to the attacker
	SendConnect	SC(A)	A initiates the PQ-X3DH protocol
	RecvConnect RC(A,B) B receives the initialization message from A
	SendSign	SS(B,A) B sends its signature to A
	weakFS	wFS A,B (k) Saves k to check its resistance against future reveal
	Send/Recv	Send A,n (m) A sends the message m of index n
		Recv B,A,n (m) B checks the integrity of message m of index n from A

Table 2 .

 2 Tamarin action facts for KEM-Double-Ratchet, abbreviations and definitions

	Action fact Abbreviation Definition
	IntegS/IntegR I S/R (n,m,s) Sends or receives message m of index n associated
			with session key s and checks its integrity in reception
	FS	FS(A,B,n,st) Saves the current state st associated with the sending
			of the message of index n between A and B in order to
			check its resistance against future reveal
	Healed	H A,B (st) Checks if the state st has recovered from a previous
			reveal in the communication between A and B
	Reveal	R(A,n)	Reveals the secrets of A associated with the message
			of index n.

Table 3 .

 3 Results of Tamarin verification for PQ-X3DH and KEM-Double-Ratchet protocols.

	Protocols	Integrity Instant Delayed	Auth.	Imp. resistance Forward secrecy PCR KCI UKS FS wFS wsFS
	PQ

  Healed(State n+3 ) with ¬ Compromised(State n+3 ) First: Compromised(State n+1 ) =⇒ ∃k ≤ n + 1, Revealed(State k ) Let name i = max{k ≤ n + 2, Revealed(State k )}, if i < n + 2 then by definition of i: ¬ Revealed(State i+1 ) ∧ ¬ Revealed(State i+2 )and by induction hypothesis, the state i + 2 is healed which means that the state n + 3 is healed too since there is no reveal in between step i + 1 and n + 3. Now if i = n + 2 let remind the definition of an healed state: By definition of a healed state, for all n > 2 we have:Healed(State n ) ⇐⇒ ∃k < n, [Revealed(State k ) ∧ ¬ Compromised(State n )] ∧ ¬Revealed(State n )And thus:¬ Healed(State n ) =⇒ ∀k < n, [¬Revealed(State k ) ∨ Compromised(State n )] ∨ Revealed(State n ) =⇒ ∀k < n, [¬Revealed(State k ) ∨ ∃ j ≤ n,Revealed(State j )] ∨ Revealed(State n ), by definition of Compromised Since we have i = n + 2 then: Revealed(State n+2 ). Additionally: ∀k ≤ n, ¬Revealed(State k ) ⇐⇒ ¬Compromised(State n )

	Therefore:
	¬Healed(State

n+3 ) =⇒ ¬Compromised(State n+1 ) ∨ Revealed(State n+2 ) ∨ Revealed(State n+3 )]

Acknowledgement

We wish to thanks Matthieu Giraud and Renaud Dubois for help on the Tamarin prover as well as helping discussions on the subject and lastly the reviewers for highlighting some typos.


Farzin Beygui
email: beygui-f@chu-caen.fr

Eric Van Belle

Patrick Ecollan

Jacques Machecourt

Christian W Hamm

Esteban Lopez De Sa

Marcus Flather

Freek Verheugt

Eric Vicaut

Faiez Zannad

Esteban Lopez De Sa

Bertram Pitt1

Gilles Montalescot

Pr Farzin Beygui

Individual participant data analysis of two trials on aldosterone blockade in myocardial infarction

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Rationale

High aldosterone plasma levels early after myocardial infarction are associated with mortality, sudden cardiac death and heart failure. [START_REF] Beygui | High plasma aldosterone levels on admission are associated with death in patients presenting with acute ST-elevation myocardial infarction[END_REF][START_REF] Palmer | Plasma aldosterone levels during hospitalization are predictive of survival post-myocardial infarction[END_REF][START_REF] Beygui | Aldosterone and long-term outcome after myocardial infarction: A substudy of the french nationwide Observatoire sur la Prise en charge hospitalière, l'Evolution à un an et les caRactéristiques de patients présentant un infArctus du myocarde avec ou sans onde Q (OPERA) study[END_REF][START_REF] Beygui | Usefulness of biomarker strategy to improve GRACE score's prediction performance in patients with non-ST-segment elevation acute coronary syndrome and low event rates[END_REF][START_REF] Montalescot | Effect of irbesartan and enalapril in non-ST elevation acute coronary syndrome: results of the randomized, double-blind ARCHIPELAGO study[END_REF] Experimental studies have shown that early administration of MRA after myocardial infarction could improve myocardial healing and both electrical and structural remodeling. [START_REF] Fraccarollo | Immediate mineralocorticoid receptor blockade improves myocardial infarct healing by modulation of the inflammatory response[END_REF][START_REF] Perrier | Mineralocorticoid receptor antagonism prevents the electrical remodeling that precedes cellular hypertrophy after myocardial infarction[END_REF] Small-sized studies have also reported a benefit of MRAs, initiated early after myocardial infarction in the prevention of left ventricular remodeling [8,[START_REF] Pasquale | Effects of canrenoate plus angiotensinconverting enzyme inhibitors versus angiotensin-converting enzyme inhibitors alone on systolic and diastolic function in patients with acute anterior myocardial infarction[END_REF] and life-threatening arrhythmia. [START_REF] Denis | Value of potassium canrenoate in the prevention of arrhythmia during the acute phase of myocardial infarction[END_REF][START_REF] Beygui | Early mineralocorticoid receptor blockade in primary percutaneous coronary intervention for ST-elevation myocardial infarction is associated with a reduction of life-threatening ventricular arrhythmia[END_REF] Mineralocortoid receptor antagonists (MRA) spironolactone and eplerenone reduce mortality in the setting of congestive heart failure with reduced ejection fraction and myocardial infarction complicated by left ventricular dysfunction and heart failure. [START_REF] Pitt | The effect of spironolactone on morbidity and mortality in patients with severe heart failure. Randomized Aldactone Evaluation Study Investigators[END_REF][START_REF] Zannad | Eplerenone in patients with systolic heart failure and mild symptoms[END_REF][START_REF] Pitt | Eplerenone, a selective aldosterone blocker, in patients with left ventricular dysfunction after myocardial infarction[END_REF] The Double-Blind, Randomized, Placebo-Controlled Trial Evaluating The Safety And Efficacy Of Early Treatment With Eplerenone In Patients With Acute Myocardial Infarction (REMINDER) [START_REF] Montalescot | Early eplerenone treatment in patients with acute ST-elevation myocardial infarction without heart failure: the Randomized Double-Blind Reminder Study[END_REF] showed that eplerenone used within the first 24 hours of ST-segment elevation MI (STEMI) excluding patients with heart failure, was safe and effective on a composite outcome mainly driven by the biological outcome of a lower plasma level of Btype natriuretic peptide. More recently the Aldosterone Lethal effects Blockade in Acute myocardial infarction Treated with or without Reperfusion to improve Outcome and Survival at Six months follow-up (ALBATROSS) failed to demonstrate a benefit of a spironolactonebased MRA regimen in improving outcome in the general setting of STEMI or non-STEMI irrespective of heart failure, but suggested a potential significant reduction of rates of death by the MRA in the STEMI subgroup of patients (77% of the population). [START_REF] Beygui | Early Aldosterone Blockade in Acute Myocardial Infarction: The ALBATROSS Randomized Clinical Trial[END_REF] Both ALBATROSS and REMINDER studies were undersized to detect a difference in rates of hard clinical outcomes. A pooled analysis of individual participant-level data was preplanned by the steering committees of the 2 trials prior to the end of the inclusion periods.

Objectives

The aim of this pooled analysis of patient-level data was to investigate the effect of a MRA regimen initiated early after the onset of STEMI, irrespective or in absence of heart failure, on mortality and the composite of death or resuscitated sudden death.

Methods

Study design and population

Our study used pooled individual patient-level data of the STEMI subgroup of the ALBATROSS [START_REF] Beygui | Early Aldosterone Blockade in Acute Myocardial Infarction: The ALBATROSS Randomized Clinical Trial[END_REF] and the total population of the REMINDER [START_REF] Montalescot | Early eplerenone treatment in patients with acute ST-elevation myocardial infarction without heart failure: the Randomized Double-Blind Reminder Study[END_REF] randomized trials. Both trials studied the efficacy of an MRA regimen in addition to standard therapy in comparison with either standard therapy alone or associated with a placebo. The designs of the studies are briefly depicted in supplementary table 1. ALBATROSS-and REMINDER-eligible patients were men and non-pregnant women presenting with STEMI within 72 and 24 hours of symptom onset respectively. REMINDER included STEMI patients only while ALBATROSS included not only STEMI (n=1229) but also Non-STEMI patients (n=369) with a significant interaction between the presentation type and treatment with respect to mortality. Hence only STEMI patients of the ALBATROSS trial were included in the present analysis. Other differences between the ALBATROSS and REMINDER studies included the treatment (IV potassium canrenoate followed by oral spironolactone versus oral eplerenone), the timing of the randomization with respect to symptom onset (within 24 versus within 72 hours) and the duration of follow-up (182±40 versus 317±218 days). Furthermore, to be included in REMINDER no sign of heart failure was to be present at randomization while in ALBATROSS patients were included regardless of signs of heart failure. The comparison between the patients' characteristics of the 2 studies is reported in supplementary table 2.

Outcomes

The primary outcome of the ALBATROSS trial was the composite of death, resuscitated cardiac arrest, significant ventricular arrhythmia, class IA indication [START_REF] Zipes | ACC/AHA/ESC 2006 guidelines for management of patients with ventricular arrhythmias and the prevention of sudden cardiac death: a report of the American College of Cardiology/American Heart Association Task Force and the European Society of Cardiology Committee for Practice Guidelines (Writing Committee to Develop Guidelines for Management of Patients With Ventricular Arrhythmias and the Prevention of Sudden Cardiac Death)[END_REF] for implantable defibrillator, new or worsening heart failure over the period of 6 months following randomization. The primary outcome of the REMINDER trial was the composite of cardiovascular mortality, re-hospitalization or extended initial hospital stay for heart failure or sustained ventricular tachycardia or ventricular fibrillation, left ventricular ejection fraction ≤ 40% ≥1 month postrandomization or high BNP or NT-proBNP levels. [START_REF] Montalescot | Early eplerenone treatment in patients with acute ST-elevation myocardial infarction without heart failure: the Randomized Double-Blind Reminder Study[END_REF] The primary efficacy outcome of the present study was mortality of any cause. As BNP was not measured in ALBATROSS and there were differences between definitions of events between the trials such as heart failure (requiring any treatment versus hospitalization or emergency room visit) or sustained/significant ventricular tachycardia (requiring any treatment versus hospitalization), any endpoint other than mortality was considered as a secondary endpoint. The key secondary efficacy outcome was the composite of death and resuscitated sudden death. Other secondary efficacy outcomes analyzed included cardiovascular death, resuscitated cardiac death, ventricular fibrillation, any ventricular arrhythmia (ventricular tachycardia or fibrillation), stroke, implanted cardiac defibrillator, class IA [START_REF] Zipes | ACC/AHA/ESC 2006 guidelines for management of patients with ventricular arrhythmias and the prevention of sudden cardiac death: a report of the American College of Cardiology/American Heart Association Task Force and the European Society of Cardiology Committee for Practice Guidelines (Writing Committee to Develop Guidelines for Management of Patients With Ventricular Arrhythmias and the Prevention of Sudden Cardiac Death)[END_REF] indication for defibrillators-whether implanted or not-and recurrent myocardial infarction -study specific definitions-. An independent committee adjudicated all outcomes in both trials.

Safety outcomes included Hyperkalemia > 5.5 and > 6 mmol/L at any time after randomization and acute renal failure defined by an increase in estimated glomerular filtration rate (eGFR) of ≥25% in comparison with admission eGFR. For the present analysis, eGFR was calculated for all patients based on Cockroft-Gault method.

Statistical analysis

All analyses used individual patient-level data of the pooled STEMI subgroup of the ALBATROSS and the total population of the REMINDER trials. The pooled analysis of the two patient populations was pre-planned by the steering committees of the two trials. The full raw datasets were provided by the studies' organizers and analyzed independently from the published data. All data were assessed within the 2 sets for completeness and coherence. No specific issue was observed.

A one stage approach was used for the analysis. Data were compared between treatment arms using the Cochran-Mantel-Haenszel test and a 2-way ANOVA both using the study identifier as the stratification variable. χ2 test and Student's t test were used for the comparison of the variables between the studies.

All efficacy endpoints were analyzed as time-to-event outcomes using Cox models systematically stratified on the study identifier with a follow-up time of 188 days equal to the median follow-up time of the pooled data. Kaplan-Meier cumulative hazards curves were drawn for the comparison of the primary and key secondary outcomes between treatment groups. Safety endpoints were analyzed as binary variables compared between treatment groups using a Cochran-Mantel-Haenszel test stratified on the study identifier.

Post hoc sensitivity analyses were performed for all efficacy endpoints using the Cox models stratified on the study identifier and adjusted on variables unequally distributed between the treatment arms with a p value threshold of <0.20.

Inter-study heterogeneity assessments were performed by the measurement of the interaction between the study identifier and the treatment arm using a cox model for efficacy endpoints and a logistic regression model for safety endpoints without stratification.

Interaction between subgroups pre-defined in the two trials and treatment was tested using the Cox models stratified on the study identifier when data were available for both trials. version 3.2.3 for Mac (R foundation for statistical computation).

Results

A total of 2241 patients were randomly assigned to the MRA regimen (1118 patients) or control regimen (1123 patients). Despite the differences between ALBATROSS and REMINDER trials (supplementary table 1), the active and control groups were well balanced with respect to most baseline characteristics and treatment strategies (Table 1) with the exception of significantly higher heart rate (p=0.02) and systolic blood pressure (p=0.02), as well as higher rates of Killip class ≥ II on admission in the control group (p=0.02). The standard of care for the index event included fibrinolysis in 189 (8.4%), primary percutaneous coronary intervention (PCI) in 1954 (87.2%), any PCI in 2060 (91.9%) and coronary artery bypass surgery in 41 (1.8%) patients. The results were consistent among all subgroups with respect to the primary and secondary key outcomes (supplemantry Figure). HR could not be calculated in the patient subgroups with a Killip class ≥2 in the active arms, as well as all patients with a grace score <109 because of absence of any primary or secondary key outcome. HR could also not be calculated for death in patients <65 because of absence of event in the active arm.

Hyperkalemia > 5•5 mmol/L occurred in 37 (3.3%) and 20 (1.8%) patients in the active and control groups, respectively (stratified OR 1.89; 95% CI, 1.09 to 3.29, p=0.03) while rates of Hyperkalemia > 6 mmol/L and acute renal failure were not significantly different between the two groups. A trend toward (p=0.09) and a significant inter-study heterogeneity (p=0.04) were detected with respect to the hyperkalemia >5.5 and 6 outcomes.

Discussion

Our analysis based on the pooled patient-level data of the two recent randomized trials addressing the question of early MRA blockade in low risk STEMI shows reduced rates of death compared to standard therapy. Although the subgroup analysis should be considered as only exploratory, it suggests a consistent effect of the treatment. MRA blockade appears to be associated with reduced risks of allcause mortality and the composite of death or resuscitated sudden cardiac death. However the analysis failed to show a benefit with respect to other endpoints including heart failure or ventricular arrhythmia. Rates of hyperkalemia > 5.5 mmol/L were significantly higher among patients treated with MRA.

Experimental studies have shown that the early use of MRA after MI reduces left ventricular expansion and extensive fibrosis by antagonizing activation of the mineralocorticoid receptor by aldosterone and cortisol. [START_REF] Fraccarollo | Immediate mineralocorticoid receptor blockade improves myocardial infarct healing by modulation of the inflammatory response[END_REF][START_REF] Mihailidou | Glucocorticoids activate cardiac mineralocorticoid receptors during experimental myocardial infarction[END_REF][START_REF] Modena | Aldosterone inhibition limits collagen synthesis and progressive left ventricular enlargement after anterior myocardial infarction[END_REF] The clinical benefit of MRA have been extensively demonstrated in heart failure irrespective of its ischemic or non-ischemic origin. [START_REF] Pitt | The effect of spironolactone on morbidity and mortality in patients with severe heart failure. Randomized Aldactone Evaluation Study Investigators[END_REF][START_REF] Zannad | Eplerenone in patients with systolic heart failure and mild symptoms[END_REF] MRA use is also associated with a reduction of mortality in patients with heart failure and reduced systolic ventricular function after myocardial infarction. [START_REF] Pitt | Eplerenone, a selective aldosterone blocker, in patients with left ventricular dysfunction after myocardial infarction[END_REF] Thus, the addition of MRAs to beta-blockers and angiotensin converting enzyme inhibitors has been highly recommended [START_REF] Mcmurray | ESC Guidelines for the diagnosis and treatment of acute and chronic heart failure 2012: The Task Force for the Diagnosis and Treatment of Acute and Chronic Heart Failure 2012 of the European Society of Cardiology. Developed in collaboration with the Heart Failure Association (HFA) of the ESC[END_REF][START_REF] Gara | ACCF/AHA guideline for the management of ST-elevation myocardial infarction: a report of the American College of Cardiology Foundation/American Heart Association Task Force on Practice Guidelines[END_REF][START_REF] Amsterdam | AHA/ACC Guideline for the Management of Patients with Non-ST-Elevation Acute Coronary Syndromes: a report of the American College of Cardiology/American Heart Association Task Force on Practice Guidelines[END_REF] in patients with heart failure and reduced left ventricular function irrespective of the etiology of heart failure.

In the Eplerenone Post Acute MI Heart Failure Efficacy and Survival Study (EPHESUS) 15 eplerenone was initiated 3 to 14 days after the onset of MI complicated by heart failure and reduced left ventricular function. The benefit observed was apparently driven by the group of patients treated earlier (i.e. 3-7 days). [START_REF] Adamopoulos | Timing of eplerenone initiation and outcomes in patients with failure after acute myocardial infarction complicated by left ventricular systolic dysfunction: insights from the EPHESUS trial[END_REF] This finding is consistent with other studies reporting high aldosterone plasma levels early after MI [START_REF] Sigurdsson | Short-and long-term neurohormonal activation following acute myocardial infarction[END_REF][START_REF] Foy | Neurohormonal changes after acute myocardial infarction. Relationships with haemodynamic indices and effects of ACE inhibition[END_REF] and the relationship of these levels with clinical outcomes. [START_REF] Beygui | High plasma aldosterone levels on admission are associated with death in patients presenting with acute ST-elevation myocardial infarction[END_REF][START_REF] Palmer | Plasma aldosterone levels during hospitalization are predictive of survival post-myocardial infarction[END_REF][START_REF] Beygui | Aldosterone and long-term outcome after myocardial infarction: A substudy of the french nationwide Observatoire sur la Prise en charge hospitalière, l'Evolution à un an et les caRactéristiques de patients présentant un infArctus du myocarde avec ou sans onde Q (OPERA) study[END_REF] The REMINDER study recruited low risk STEMI patients with no heart failure at admission and very low mortality rates. Although REMINDER showed a benefit of eplerenone over placebo, the benefit was driven by the B-type natriuretic peptide levels with only non-significant trends on clinical outcomes. [START_REF] Montalescot | Early eplerenone treatment in patients with acute ST-elevation myocardial infarction without heart failure: the Randomized Double-Blind Reminder Study[END_REF] The ALBATROSS trial recruited a broader STEMI population at higher risk as compared with REMINDER. ALBATROSS STEMI population included all-comers presenting for primary PCI, few with heart failure (6.7%), with significantly higher admission GRACE scores but also more contemporary and optimal treatment as compared to REMINDER. Although the study failed to show the benefit of MRAs on the primary outcome it highlighted a significant signal in favor of a MRA effect on mortality in STEMI. The present pooled analysis includes a relatively young and lowto-intermediate risk STEMI population (mean grace score 140) treated optimally with very high rates of revascularization and optimal medical therapy. The mortality reduction with MRAs in addition to an optimal management in such a low risk population should not be neglected. The previously mentioned pre-clinical and clinical data, the reduction of mortality in the setting of chronic heart failure or post myocardial infarction heart failure as well as the strength of the association support the plausibility of a MRA effect on mortality in the setting of STEMI. The early blunting of biological effects of MR activation after acute coronary artery occlusion [START_REF] Perrier | Mineralocorticoid receptor antagonism prevents the electrical remodeling that precedes cellular hypertrophy after myocardial infarction[END_REF][START_REF] Fraccarollo | Immediate mineralocorticoid receptor blockade improves myocardial infarct healing by modulation of the inflammatory response[END_REF][START_REF] Mihailidou | Glucocorticoids activate cardiac mineralocorticoid receptors during experimental myocardial infarction[END_REF], may lead to a favorable effect in STEMI through the un-triggering of the neurohormonal activation and the subsequent post-MI fibrosis and remodeling both leading to higher risk of death.

A recently published study-level meta-analysis of eleven randomized trials showed also the benefit of MRAs on mortality [START_REF] Bossard | Mineralocorticoid receptor antagonists in patients with acute myocardial infarction -A systematic review and meta-analysis of randomized trials[END_REF]. The study included STEMI and non-STEMI patients, with heart failure as an inclusion criteria or not. However the benefit of the MRAs was driven by studies that included patients with heart failure. Compared to the latter study, our patient-level analysis pooling only STEMI patients, without heart failure as an inclusion criteria and with a more adequate univariable and adjusted analysis of censored data may be considered as more sensitive in detecting differences between groups.

Interestingly, the MRA-related reduction of mortality found in our study was not associated with a concordant significant reduction of major ventricular arrhythmia or heart failure, although both events occurred numerically less in the active treatment group.

Sustained ventricular tachycardia or fibrillation have been reported to occur in 5.2% of patients after primary PCI essentially in the 48 first hours in the relatively recent analysis of the Harmonizing

Outcomes with RevasculariZatiON and Stents in Acute Myocardial Infarction (Horizons-AMI) randomized trial. [START_REF] Mehta | Incidence of and outcomes associated with ventricular tachycardia or fibrillation in patients undergoing primary percutaneous coronary intervention[END_REF] In the latter study, such events did not portend decreased survival. The rates of ventricular tachycardia or fibrillation were approximately 4% in the pooled population of our analysis, with a difference between rates in the ALBATROSS (7.2%) and the REMINDER trials (0.4%). Such a difference is likely to be due to the difference of the definitions of ventricular tachycardia (requiring hospitalization) in REMINDER but also due to a more selected patient population without heart failure at admission, with preserved ejection fraction and with extremely low event ratesi.e death, heart failure, indication for ICD-. The absence of effect on rates of ventricular arrhythmia in our study is not in contradiction with a possible MRA effect on mortality. Concordant with our study, in both Randomized Aldosterone Evaluation Study (RALES) [START_REF] Pitt | The effect of spironolactone on morbidity and mortality in patients with severe heart failure. Randomized Aldactone Evaluation Study Investigators[END_REF] and EPHESUS [START_REF] Pitt | Eplerenone, a selective aldosterone blocker, in patients with left ventricular dysfunction after myocardial infarction[END_REF] trials mortality was reduced with MRA despite the absence of effect on the rates of ventricular arrhythmia. Moreover, in concordance with the above-mentioned study [START_REF] Mehta | Incidence of and outcomes associated with ventricular tachycardia or fibrillation in patients undergoing primary percutaneous coronary intervention[END_REF] most ventricular tachycardia were reported within only 48hours after randomization and such events may not impact mortality. Finally ventricular arrhythmia suppression after myocardial infarction is known not to improve survival. [START_REF] Arrhythmia | Preliminary report: effect of encainide and flecainide on mortality in a randomized trial of arrhythmia suppression after myocardial infarction[END_REF] Considering the trend towards a reduction of rates of ventricular fibrillation but not ventricular tachycardia in our analysis, it is plausible that MRAs may reduce the rates of lethal arrhythmia, or prevent the fatal issue of arrhythmia without affecting the frequency of post-STEMI arrhythmia in general.

The global rate of hospitalization for heart failure (4.4%) in a recent multicenter real-life cohort of STEMI patients undergoing primary PCI [START_REF] Taniguchi | Incidence and Prognostic Impact of Heart Failure Hospitalization During Follow-Up After Primary Percutaneous Coronary Intervention in ST-Segment Elevation Myocardial Infarction[END_REF] was higher than in REMINDER (1.4%) but lower than in ALBATROSS (6.3%). The differences in study definitions, the low-risk populations and the short durations of follow-up could explain the absence of detectable MRA effect on heart failure in the current analysis.

Our analysis also highlights the relative safety of the MRA regimens used in the studies. Although the rates of hyperkalemia >5.5 mmol/L were higher in the MRA group than in the control group, they remained lower than what has been previously reported [START_REF] Pitt | Eplerenone, a selective aldosterone blocker, in patients with left ventricular dysfunction after myocardial infarction[END_REF][START_REF] Montalescot | Early eplerenone treatment in patients with acute ST-elevation myocardial infarction without heart failure: the Randomized Double-Blind Reminder Study[END_REF] and the rates of hyperkalemia >6 mmol/L and acute renal failure were not different between treatment groups. However the results on hyperkalemia should be considered with great precaution because of a significant inter-study heterogeneity.

Our analysis has limitations inherent to its design pooling data from different studies with different designs and different active treatments. However a class effect is very likely between the drugs and the stratified and adjusted analyses as well as absence of detected inter-study heterogeneity may minimize the risk of bias. Furthermore event rates remained low and event definitions were different for ventricular tachycardia and heart failure. Nevertheless with respect to the primary and the key secondary outcomes of our study -death and death or resuscitated sudden death-the analysis may be considered as robust. The adjusted analysis should be interpreted with the consideration of low event rates, especially with respect to mortality. However the similar magnitude of effects and their confidence intervals between the un-adjusted and adjusted analyses supports the robustness of the findings. The subgroup analysis should be considered with great precaution because of the risk of multiple testing with low event rates. Whether the benefit of MRA may interact with the infarct location or the culprit vessel could not be assessed by our study because of lack of data.

Although the present report is the largest experience in STEMI outside of the scope of heart failure, it may lack power to detect differences between several studied outcomes. Larger and specifically designed studies are needed to assess such outcomes.

Conclusions

Our analysis based on pooled patient-level data from two randomized trials suggests a significant reduction of death and death or resuscitated sudden death associated with MRA regimens given early after low risk STEMI. Despite strong recommendations based on robust clinical evidence in the setting of heart failure, MRAs are still underused in routine clinical practice. Our data on both efficacy and safety of MRAs may contribute to extend the use of these life-saving and low-cost drugs. Although our study seems robust with respect to its primary outcome, the low event rates highlight the need for more studies adequately sized and specifically designed to confirm the potentially major clinical benefit associated with low-cost treatments.

Table 1 . Patient characteristics according to treatment

 1 As reported in table 2, after a median follow-up of 188 days (interquartile range 52 days), the primary outcome (Figure1) occurred in 5 (0.4 %) and 17 (1.5%) patients in the active and control groups, respectively (HR 0.30, 95% CI 0.11-0.81); p=0.01 and adjusted-HR 0.31, 95% CI 0.11-0.86; p=0.03). Two un-adjudicated deaths reported as security events 389 and 528 days after randomization in the control and the active groups of the REMINDER trial respectively were not included in the analysis. All resuscitated sudden deaths were reported within the analysis time. The key secondary outcome of death or resuscitated sudden death (Figure2) occurred in 6 (0.5 %) and 22 (2%) patients in the active and control groups, respectively (HR 0.27, 95% CI 0.11-0.67; p= 0.002 and adjusted-HR 0.26, 95% CI 0.10-0.65;

		Overall	Active	Control
	Variable				p
		n= 2241	n=1118	n=1123
	Age (years)	58±12	58±11	58±12	0.8
	Gender (Female)	377(16.8%) 178(15.9)	199(17.7)	0.3
	Admission characteristics
	Body mass index (Kg/m 2 )	27±5	27±5	27±5	0.12
	Heart rate (per minute)	73±15	73±15	74±15	0.02
	Systolic blood
		124±21	123±21	125±21	0.02
	pressure(mmHg)
	Killip class	1.05±0.28	1.03±0.22	1.06±0.33	0.007
	Killip class ≥ 2	82(3.7)	29(2.6)	53(4.7)	0.007
	Plasma creatinine (µmol/L)	81.8±22.3	82±22	81±23	0.4
	eGFR (mL/min)	104±36	102±35	105±37	0.14
	Plasma potassium (mmol/L)	4.02±0.5	4.03±0.5	4.01±0.4	0.3
	GRACE score	140±23	140±22	140±24	0.6
	Medical history
	Systemic hypertension	964(43.0)	464(41.5)	500(44.5)	0.15
	Diabetes mellitus	298(13.3)	145(13.0)	153(13.6)	0.7
	Hypercholesterolemia	883(39.4)	450(40.3)	433(38.6)	0.4
	Active smoking	772(34.5)	375(33.5)	397(35.4)	0.4
	Prior myocardial infarction	136(6.1)	71(6.4)	65(5.8)	0.6
	Prior stroke	44(2.0)	28(2.5)	16(1.4)	0.09

p=0.004). There were also trends toward lower rates of death from cardiovascular causes (p=0.06) and ventricular fibrillation (p=0.08 and adjusted-HR) in the active group. Other assessed efficacy endpoints did not differ between the two groups. The two trials were different with respect to the rates of the primary and secondary key outcomes as well as several other outcomes (supplementary table

3

). However with the exception of a trend (p=0.06) towards a heterogeneity in rates of recurrent myocardial infarction, no significant inter-study heterogeneity was detected.

Table 2 .

 2 Outcomes according to treatment arm

						Inter-study
	n (%)		Active versus control
						heterogeneity
	Active	Control
		HR (95% CI)	p	Adj-HR (95% CI)	p	p for interaction
	n=1118	n=1123

*The composite of death, resuscitated sudden death, ventricular arrhythmia, heart failure and indication for ICD. Adj-HR: HR adjusted on variable unequally distributed between treatment arms with a threshold p value <0.2 -i.e. baseline binary killip class, heart rate, systolic blood pressure, eGFR, body mass index and, history of systemic hypertension and stroke.

The REMINDER trial was approved by each participating centre's ethics committee; the ALBATROSS trial was approved by the French National Institutional Ethical Review Board.

What is already known about this subject?

Mineralocorticoid receptor antagonists reduce mortality in the setting of myocardial infarction complicated by heart failure.

What does this study add?

The study shows that regardless of heart failure, mineralocorticoid receptor antagonists reduce mortality in the setting of ST elevation myocardial infarction, in addition to optimal treatment.

How might this impact on clinical practice?

The use of very low cost mineralocorticoid receptor antagonists may be considered in ST elevation myocardial infarction patients irrespective of heart failure to reduce mortality The first and last author had full access to all the data, prepared the first draft of the manuscript. The manuscript was approved by all co-authors, who made the decision to submit the manuscript for publication and assumed responsibility for data accuracy.

The Corresponding Author has the right to grant on behalf of all authors and does grant on behalf of all authors, an exclusive license on a worldwide basis to the BMJ Publishing Group Ltd and its Licensees to permit this article to be published in HEART editions and any other BMJPGL products to exploit all subsidiary rights

Competing interests

F Beygui has received institutional grants and/or lecture or consultancy honoraria from AstraZeneca, Medtronic, Boston Scientific, Biosensor and Acist.

C Hamm has received speaker fees from Pfizer G Montalescot declares his competing interests on http://action-coeur.org/declarations-dinterets/

Ethics approval


Zitouna Rim

Molénat Jérôme

Raclot Damien

Albergel Jean

Voltz Marc

Omere Team

SUSTAINABLE MANAGEMENT OF ECOSYSTEMS FOR AN AGROECOLOGICAL TRANSITION AND FOOD SECURITY

• Paysages : modélés de longue date par l'activité humaine via l'agriculture notamment

• Sols : vulnérables, généralement minces même si très variables spatialement

••

  Climat : très fortement variable au sein de l'année et d'une année à l'autre, forte occurrence d'évènements extrêmes (crue / sécheresse) Documenter, sur le long-terme, les teneurs, les stocks et les flux d'eau, de sédiments et de contaminants • Identifier les facteurs naturels et anthropiques qui les contrôlent à court et long-terme • Comprendre l'impact agrégé des pratiques et aménagements du milieu sur les teneurs, stock et flux de la parcelle à l'échelle du bassin versant • Dériver des modes de gestion durable des milieux méditerranéens cultivés basés sur un large panel de services écosystémiques que ces milieux délivrent (e.g., production agricole, eau bleue, régulation des crues et de l' érosion des sols, régulation de la contamination des eaux et des sols…) observation du climat et des activités humaines Suivi des stocks et des flux d'eau et de matières associées... Mesure de l'évapotranspiration réelle le ratio ET / ET0 suit la dynamique des cultures annuelles : -fort de l'automne au printemps (ET = 4 mm/jour en avril) -très faible en été (ET = 1 mm/jour en juillet-août) mesure de l'ETR par covariances turbulentes surface échantillonnée ≈ 18 ha Zitouna et al., 2018, Atmosphere (INRGREF, LISAH) R a i n f a l l W a d i R u n o f f H i l l s l o p e R u n o f f E v a p o r a t i o n I n f i l t r a t i o ., 2015, Hydrological Processes (ENIT, LISAH)

Conclusion

Un dispositif franco-tunisien structurant de la recherche, multi/transdisciplinaire, pour une vision holistique de la zone critique