Cas Cremers

Caroline Fontaine

Charlie Jacomme

A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols

We provide the first mechanized post-quantum sound security protocol proofs. We achieve this by developing PQ-BC, a computational first-order logic that is sound with respect to quantum attackers, and corresponding mechanization support in the form of the PQ-Squirrel prover.

Our work builds on the classical BC logic [7] and its mechanization in the Squirrel [5] prover. Our development of PQ-BC requires making the BC logic sound for a single interactive quantum attacker. We implement the PQ-Squirrel prover by modifying Squirrel, relying on the soundness results of PQ-BC and enforcing a set of syntactic conditions; additionally, we provide new tactics for the logic that extend the tool's scope.

Using PQ-Squirrel, we perform several case studies, thereby giving the first mechanical proofs of their computational post-quantum security. These include two generic constructions of KEM based key exchange, two sub-protocols from IKEv1 and IKEv2, and a proposed post-quantum variant of Signal's X3DH protocol. Additionally, we use PQ-Squirrel to prove that several classical Squirrel case studies are already post-quantum sound.

Introduction

In recent years, multiple highly-successful tools have been developed to analyze and verify cryptographic protocols and primitives [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF][START_REF] Blanchet | Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif[END_REF][START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF][START_REF] Swamy | Dependent types and multi-monadic effects in F*[END_REF]. They have proven the usefulness and necessity of computer-aided cryptography, both uncovering critical attacks against widely deployed protocols and helping in the design of new standards [2, 10, 15, 25, 28-30, 32, 33, 46, 47, 50].

In anticipation of developments in quantum computing that would break a lot of widely-used cryptographic primitives, the security community has started to develop many new security primitives and protocols, and revisit old protocols. Additionally, an extensive multi-year NIST standardization process is ongoing to develop new primitives and protocols. These efforts aim to establish mechanisms that are provably secure against quantum attackers. At some level of abstraction, this implies (i) designing new primitives and prove (or assume) that they are secure against a quantum attacker, and (ii) proving that a concrete protocol that uses such primitives is indeed secure against a quantum attacker. In this work, we focus on the latter, and in particular how we can mechanize such proofs.

A classical strategy for proving a protocol's security is a so-called reduction proof, which yields computational security guarantees against a polynomial-time attacker. This approach is used in most pen-and-paper proofs by cryptographers, and involves constructing a reduction from any attack on the protocol to an attack on the used cryptographic assumptions, and then reasoning by contradiction. This is a well studied approach with respect to classical (non-quantum) attackers: different flavors of such proofs can be mechanized by tools such as CryptoVerif [START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF] and EasyCrypt [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF]. However, some proof steps commonly used in reductions that are valid for a classical attacker, such as rewinding, are in general not valid anymore for quantum attackers. This result is similar to the no-cloning theorem [START_REF] Wootters | A single quantum cannot be cloned[END_REF], which implies that one must be careful when talking about the state of a quantum attacker. As a consequence, a given by Proverif and Tamarin; on the other side, it operates at a higher level of abstraction than EasyCrypt and CryptoVerif. Consequently, Squirrel is less expressive and thus less suited to reason about cryptographic primitives, but tends to scale better to larger construct. However, Squirrel does not provide any concrete security bounds, and in security proofs over unbounded protocols, the number of sessions is arbitrary and not attacker chosen. For a detailed comparison between Squirrel, EasyCrypt and CryptoVerif, we refer the reader to [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF]Appendix E].

CryptoVerif does not have any support for quantum attackers yet, it might be possible to make it quantum-sound by using ideas from our work, such as forbidding some manipulations over the attacker state, and ensuring that a unique quantum attacker process can continue without having to alter or inspect its internal state.

The previously mentioned EasyCrypt is a toolset for constructing cryptographic proofs, which currently mainly targets cryptographic primitives. It was first adapted to the quantum setting with qRHL [START_REF] Unruh | Quantum Relational Hoare Logic[END_REF], a formal security prover based on a quantum relational Hoare logic, and later (in concurrent work to ours) to the post-quantum setting with EasyPQC [START_REF] Barbosa | EasyPQC: Verifying post-quantum cryptography[END_REF]. The qRHL approach works on quantum constructions, which substantially complicates proving classical constructions. For example, there is no equivalent to the classical implication operation over quantum predicates (see e.g., [START_REF] Luisa | Reasoning in quantum theory: sharp and unsharp quantum logics[END_REF]). EasyPQC avoids this overhead by only considering classical constructions.

Similar to our approach, EasyPQC adds new side conditions to its core logic, such as forbidding case distinctions on the attacker's internal state. It is difficult to compare their side conditions to ours, since the conditions are deeply linked to the underlying logics, which are of a very different nature. Notably, EasyPQC supports reasoning in the Qantum Random Oracle Model (QROM). The BC logic does not yet support the ROM (nor QROM), and hence neither do we. This is not an inherent restriction of the logic and could be future work. For our current case studies, we prefer the use of the PRF assumption over the QROM.

EasyPQC and our approach inherit their focus from their starting points: the EasyCrypt approach is more geared towards cryptographic primitives, while BC is designed for protocols. All current EasyPQC case studies are cryptographic primitives, whereas our case studies are protocols. In particular, our case studies for KEM based key exchanges are the first mechanized proofs with computational guarantees of such protocols.

2 Background: the classical BC logic and Squirrel Below we first recall the main elements of the original BC logic [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF] that are relevant for understanding our work in the following sections. In Section 2.5 we describe the Squirrel prover [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF], which mechanizes reasoning in the BC logic.

In the computational model, the security of a protocol is established by showing that the protocol cannot be distinguished from its idealized version by any polynomial-time attacker w.r.t. a security parameter. Such security proofs of protocols rely on two ingredients:

• a base assumption, where we assume that some computational problem cannot be solved efficiently, e.g. integer factoring or discrete logarithm;

• a security reduction, where one shows that if there exists an attacker against the protocol, there exists an attacker against the base assumption.

But the construction of security reductions is difficult and error-prone. To ease this process, the BC logic proves the security of protocols inside a first-order logic. This approach requires that within BC, everything is modeled using only terms, i.e., purely syntactic constructs. This is very different from the game-based modeling, where protocols are expressed as abstract programs with procedure calls, states, and side effects. With terms, all protocol actions become pure functional calls, which tends to ease the formal reasoning. This leads to some core elements in the design of the logic: one needs to 1. define terms, as well as an interpretation from protocols to terms so that the terms syntactically describe all the behaviours of the protocol, 2. define logical predicates and rules (which include axioms) to reason about our terms, and 3. show that the rules are sound, i.e., that the rule applications correspond to correct reductions.

We provide an overview of the first two elements in the following, and refer the reader to [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF] for details of the rules and their soundness. However, all three elements will be discussed when we present the modified post-quantum sound logic in the following sections.

2.1 Specifying protocol behaviours using syntactic terms

From protocols to terms

Let us consider a very simple example protocol process P , using an informal syntax.

Example 1 (Protocol).

P := new sk.in(x).new r.out(enc(x, r, sk)).in(y).new r .out(enc(y, r , sk)).

Process P samples a secret key sk, and uses it to encrypt some attacker input x using the random seed r (explicitly modeling probabilistic encryption). It then encrypts a second input y with random seed r .

Equivalently, in the game-based notation with a stateful probabilistic attacker A and security parameter η, the experiment that returns the attacker-observable values is defined as:

Experiment Exp P enc,A (η) sk $ ← -{0, 1} η x $ ← -A(1 η ) r $ ← -{0, 1} η y $ ← -A(1 η , enc(x, r, sk))
r $ ← -{0, 1} η return (enc(x, r, sk), enc(y, r , sk))

To syntactically represent such observable sequences of values using terms, one can use the following constructions:

• fresh values n sampled from an infinite set N , representing randomly sampled bitstrings, such as r, r , and sk above;

• public function symbols f ∈ Σ, to model e.g., encryption functions such as enc; and

• variables such as x and y from the set of variables X , modeling attacker inputs.

Any protocol computation can then be modeled as applications of public functions to either fresh values modeling randomly generated values (such as nonces and secret keys), or variables modeling attacker inputs. This is essentially the Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF], where the protocol can be described with the following term sequence: enc(x, r, sk), enc(y, r , sk)

This sequence of terms, that we will refer to as the frame of the protocol, represents the possible messages that an attacker can observe during the protocol's execution.

Modeling attacker computations

The sequence of terms in Eq. [START_REF]The Squirrel Prover repository[END_REF] is not yet sufficient to reason syntactically about protocols, because it does not capture that y probabilistically depends on the value of enc(x, r, sk). From a high-level point of view the logic must satisfy • locality -a term must explicitly contain all its probabilistic dependencies.

Essentially, it needs to syntactically capture that y is the result of an attacker's unknown computation, which depends on the previous messages, e.g., in our example, y depends on r and sk. The BC logic uses free function symbols att i that represent unknown pieces of code, i.e., attacker computations that receive as arguments the previous messages seen by the attacker.

The previous frame can now be expressed as:

enc(att0(), r, sk), enc(att1(enc(att0(), r, sk)), r , sk)

att 0 () representing the first message (x) computed by the attacker, when it does not have access to any information from the protocol, and att 1 (enc(att 0 (), r, sk)) being its second message (y), which is a function of the protocol's first output. The term-based notation is more akin to a functional view: one cannot use variables such as x to refer to previously computed values. For this reason, att 0 () occurs twice in Eq. ( 2). However, attacker computations such as att 0 are probabilistic algorithms, and hence two different invocations might yield different results. This is not the intended interpretation, and it therefore introduces a new requirement on terms:

• stability -two occurrences of the same term must evaluate to the same value.

When one evaluates the value of the previous frame, this implies that the two occurrences of att 0 () evaluate to the same value. This requirement captures that within a single protocol execution, identical terms refer to the same value and not to separate (probabilistic) attacker calls.

Adding conditionals

A last issue to syntactically capture the frame of a protocol is the fact that protocol outputs often depend on conditionals. Let us consider a new example:

Q := new n.new n .out(c, n ).in(c, x).if x = n then out(c, ok) else out(c, ko).
This protocol randomly samples two values, i.e. two names, gives one to the attacker, and finally outputs ok if the attacker can provide the second one. Here, the attacker cannot guess with non-negligible probability the name, so ok should almost never be obtained.

To represent this inside terms, the idea is to add to the public function symbols set Σ, a ternary function symbols ite(_, _, _), that we will in fact denote for clarity if _ then _ else _. This symbol will always be interpreted so that it matches the computations of a conditional. One also needs to write the condition and the outputs, so the BC logic introduces a function symbol of arity 2 that test equality, _ . = _, along with two arity 0 symbols ok and ko. The frame of the protocol is then expressed by: n , if att 0 (n ) .

= n then ok else ko

Looking at this frame, we can see one of the first strength of the syntactical approach. If we consider the condition att 0 (n ) .

= n, it is easy to see that the attacker computation att 0 (n ) is completely independent of n, so we can conclude that this equality test cannot succeed with non-negligible probability. This matches the intuition that Q is in fact indistinguishable from:

Q := new n.new n .out(c, n ).in(c, x).out(c, ko).

Reasoning about terms

The BC logic contains in its syntax a binary predicate ∼. This predicate expects two sequences of terms and intuitively represents their indistinguishability. Note that ∼ has low operator precedence, but we often add parentheses for readability.

Example 2 (BC indistinguishability formula).

n , if att 0 (n ) . = n then ko else ok ∼ n , ok (3)
The protocol modeled on the left-hand side produces a fresh value n , sends it, and then waits to receive another value (represented by att 0 (n )). If the received value is the same as a freshly generated value n, the protocol outputs ko, otherwise ok. The formula expresses that the attacker cannot distinguish this protocol from the protocol that sends a fresh value n , waits for an input, and then outputs ok. To give a flavor of how proofs are performed in the BC logic, we provide some rule examples and prove that Eq. ( 3) holds in the logic.

Example 3 (Rules and proofs).

=ind (t . = n) ∼ false when n does not occur in t If-f φ ∼ false (u, v) ∼ w (u, if φ then s else v) ∼ w Refl u ∼ u
Logical rules are read bottom-up, where to prove the formula on the bottom, one can prove the formulas on the top. Rule =ind means that a term t that does not syntactically contain a fresh value n cannot be equal to it, and If-f tells us that if a conditional is always false, we can only consider its negative branch. The Refl rule encodes that ∼ is reflexive. With those rules, we can prove the formula that represents the indistinguishability of Q and Q : = att 0 ()

att0(n ) . = n ∼ false =ind (n , ok) ∼ (n , ok) Refl n , if att0(n ) . = n then ko else ok ∼ (n , ok) If-f

A faithful computational interpretation

We previously described the BC way to syntactically describe the behaviour of a protocol interacting with an attacker. To ultimately get to a logic that provides computational guarantees, those syntactic terms must capture all the behaviours of the protocol. To do so, BC provides a formal way to interpret those terms, so that their possible evaluations match those of the real protocol. Intuitively, given an attacker against the real world protocol, and given the syntactic frame (e.g., Eq. ( 2)), it should be possible to build a simulator producing the same results as the protocol. If this is possible, then the frame does indeed capture all the possible behaviours of the protocol, and we can thus use it to reason about its security.

Recall that we already mentioned two high-level desirable properties of our constructs:

• locality -a term should completely contain all its probabilistic dependencies.

• stability -our interpretation should interpret two occurrences of the same term to the same value.

Interpreting terms

We now describe how BC interprets a term, i.e., computes the probabilistic result of a term, while satisfying both locality and stability. The interpretation has three parameters: the security parameter η and two infinite random bitstrings ρ s and ρ r . The interpretation extracts the randomness used in probabilistic protocol functions from ρ s , and the attacker randomness from ρ r . By universally quantifying over those parameters and the attacker computations, it captures all the possible executions of a protocol.

The interpretation depends on a set of Polynomial Time Turing Machines (PTTM) that compute the evaluation function T of a term, i.e.,

• a machine T n for n: outputs the value of a given fresh value, depending on η and ρ s , which may typically extract a sequence of η bits from ρ s ;

• a machine T f for f : computes the output of a public function depending on its arguments;

• a machine T atti for att i : performs some attacker computation, depending on its arguments, η and ρ r .

To interpret a term, one can consider the term as a tree of (sub)terms, and recursively call the corresponding Turing machine from the leaves to the root. Going back to the term enc(att 0 (), r, sk) occurring in Eq. ( 2), its possible values are obtained by running the simulation described in Fig. 1.

By design, all Turing machines in the interpretation are deterministic: the randomness is explicitly passed to capture probabilistic behaviour (using ρ s and ρ r ). This ensures that the interpretation satisfies stability: two occurrences of att 0 () in the term imply two computations of T att0 that deterministically evaluate to the same value. For example, if we consider the function symbol . = that models equality testing, the evaluation of Fig. 2 always returns true, which is the expected behaviour.

Note that T att0 and T att1 do not share any implicit state and, more generally, nor would T atti and T atti+1 . This may seem counter-intuitive, as att i and att i+1 usually represent two unknown computations of the same attacker A, that can in practice maintain a state between successive calls. The BC logic does not explicitly ensure this, but by modeling conventions, we always give all the previous inputs of att i also to att i+1 . As a result, in the simulations one can make T atti+1 re-perform all the computations of T atti to recompute its state. Modelling each attacker call by a distinct machine is a crucial design choice of the BC logic that ensures locality.

Protocol interactions

We now focus on protocol interactions, as it will play an important role when moving to the quantum setting. We informally describe an attacker A in the real world as a sequence of unknown operations {A i }, that produces the message m i at step i, and implicitly maintains a state φ i between each computation. We can consider a protocol P as a sequence of operations split by in (receive) operations. The attacker's operations interact with the protocol sequence: a protocol operation P i typically uses out to send messages, providing more knowledge to the attacker, which can then use this knowledge to produce a message for P i+1 . E.g., considering Example 1, we define T att0 s.t. it simulates A 0 and returns m 0 , and T att1 s.t. on input u it first simulates A 0 to get φ 0 , and then runs A 1 on φ 0 and u.

Still considering P from Example 1, with the corresponding syntactic frame Eq. ( 2), we depict in Fig. 3 the simulation that produces the same result as the real-world interaction.

Indistinguishability predicate and logical rules

Once equipped with an interpretation for terms, BC defines the predicate ∼ that will return true over two sequence of terms if the advantage of any final distinguisher is negligible in η. As for any other attacker computation step, this final distinguisher does not inherit any states from the previous attacker calls, but it may recompute those states if it is given the same arguments.

Consider two protocols: one can build as previously described two sequences of terms that correctly capture all the behaviours of their interactions with an attacker. If there exists an attacker that can distinguish the two protocols, then there is a set of attacker Turing machines {T atti } that shows that the simulation of the two sequences of terms can be distinguished, and thus that ∼ does not hold over them. This constitutes the soundness of the BC logic.

Finally, one needs to prove the soundness of the logical reasoning rules by using reductions. For instance, a simple reduction would prove that a rule such as If-f from Example 3 is indeed a valid rule to reason about ∼.

The rules presented in this example can be proven sound for any Turing machine attacker, without limiting its computational power. Such rules form the core of the logic, and are referred to as structural rules. In addition, one also needs to integrate the classical cryptographic assumptions inside the logic.

Cryptographic assumptions

In BC, cryptographic assumptions are encoded as rules (also referred to as axioms). BC includes provenlysound rules to encode assumptions such as PRF, IND-CCA, EUF-CMA, ENC-KP, INT-CTXT, OTP, and DDH. Given a cryptographic assumption, one can translate it into a BC rule using terms: proving soundness of such a rule is done by providing a reduction showing that if there exists a model that breaks the BC assumption, then there exists an attacker that breaks the original cryptographic assumption. As the translation is often natural, the soundness proofs of the axioms are relatively straightforward, and are usually fully black-box reductions. We refer the reader to [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF][START_REF] Koutsos | Preuves symboliques de propriétés d'indistinguabilité calculatoire[END_REF] for the soundness proofs of the rules corresponding to the main cryptographic assumptions.

Example 4 (DDH assumption). In BC proofs, the full DDH assumption is not usually made: the encoded assumption can be seen as a generic version that is agnostic about the implementation. Concretely, one can see the DDH assumption of BC as a generic assumption over two function symbols, an extractor ext and a combiner comb, such that, for any names n 1 , n 2 , n 3 we have ext(n 1 ), ext(n 2 ), comb(ext(n 1 ), n 2 ), comb(ext(n 2 ), n 1 ) ∼ ext(n 1 ), ext(n 2 ), ext(n 3 ), ext(n 3 ) .

For a cyclic group with generator g, the extractor function would be ext(n) := g n and the combiner comb(t, u) := t u , and the DDH over the group assumption implies our generic assumption over the functions.

Example 5 (OTP assumption). For the exclusive-or operator ⊕, we only assume that it is a binary function symbol such that for any term t and fresh name n, it allows for a one-time pad, i.e., (t ⊕ n) ∼ n .

For any security proof of a protocol that uses ⊕, one typically does not need to specify that ⊕ may be associative and commutative. Such a proof then gives us security guarantees, regardless of whether the concrete implementation of ⊕ is associative or not.

To summarize, for proving with BC the full (computational) security of a protocol that uses concretely instantiated primitives, we first require a proof that the primitives instantiate cryptographic assumptions. Then, we use a translation of those assumptions in the BC proof to prove properties of the protocol. For example, to give a computational proof of a signed Diffie-Hellman protocol that uses Ed25519 signatures, we would use the proof that Ed25519 signatures satisfy EUF-CMA, and then use the corresponding EUF-CMA rule in the BC proof.

Note that it is also not uncommon to leave this question unanswered: i.e., to propose a protocol that relies on an assumption (e.g., PRF), for which we do not know an instantiation that provably meets it, and the guarantee is then phrased as "assuming that primitive X is a PRF, . . .". Such a proof can still be meaningful since it proves the absence of a class of attacks, or anticipates a future provable instantiation.

The Squirrel Prover

The Squirrel Prover mechanizes the BC logic, and offers additional features not present in BC. Two downsides of the original BC logic, which are solved by Squirrel, are:

1. to prove the security of a protocol, one must make a proof for each possible action orderings of the protocol, and 2. the logic only considers finite protocols, and therefore notably only a bounded number of sessions.

As the security proof of a protocol may be very similar for many action orderings, which are also called (symbolic) traces, the first point implies a lot of tedious repetitions inside proofs. The second point can be solved by performing induction over the number of sessions, but this cannot be done inside the BC logic, and instead requires external mathematical reasoning.

Protocol Specification

The Squirrel prover's protocol specification language is close to the well-known applied pi-calculus.

In Fig. 4 we give a simplified version of a key exchange protocol based on asymmetric encryption. An Initiator with secret and public keys (sk I , pk I ) sends some encrypted ephemeral secret k I to a responder with keys (sk R , pk R ), that answers with its own encrypted ephemeral share k R . Then, a shared key is derived as h(s, k I ) ⊕ h(s, k R ), where h is a PRF hash function and s a public seed. The derived key should only be computable by the intended peer. The protocol does not offer any explicit authentication.

A possible implicit authentication guarantee could be: If a party X derives a key k with intended peer Y, then whoever can also compute the key must be Y, and agree on the communication partners.

A basic model of this protocol is expressed in Squirrel as illustrated in Listing 1. The hash and aenc instructions declare function symbols that respectively satisfy either the PRF assumption or the IND-CCA assumption, and the name command declares fresh values. In the process declarations, out and in specify outputs and inputs, new specifies sampling fresh values, and | is for parallel composition. In the last step of the Initiator, the instruction sIR:= is used to store the derived key in a state. The last line of this example captures a security property, which we discuss in next Section.

Note that the threat model is part of the input file, and Squirrel can be used to verify many scenarios. For instance, more complex versions of this running example that will be discussed in Section 6.3 can

sk I , k I , pk R Initiator sk R , k R Receiver pk I , enc(k I , pk R ) enc(k R , pk I )
Derive key:= h(s, k I ) ⊕ h(s, k R ) Figure 4: Encryption based key exchange include an unbounded number of sessions and participants, and pk(sk I ) may not be hard-coded inside the Responder process but received as an input. The Squirrel paper [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF] introduces a meta-logic that introduces universal quantification over the possible traces of a protocol, as well as its number of sessions. As one can then reason at an abstract level on the traces, a single proof in the meta-logic covers multiple traces of the protocol, and it is now possible to consider unbounded protocols, thus solving both previous issues.

To do so, the logic is extended with timestamp variable τ to quantify over possible points in a trace, and macros that depend on a protocol P , such as:

• input P @τ , to refer to the input received by the protocol P at timestamp τ ;

• output P @τ for the output;

• frame P @τ for the full frame for the protocol up to this point, which is the sequence of all previous outputs.

If we denote by pre(τ ) the function that points to the previous timestamp in the trace, and abstracting away some details, frame P @τ would expand to frame P @pre(τ ), output P @τ . The indistinguishability of two protocols P and Q can be expressed in a single meta-logic formula frame P @τ ∼ frame Q @τ . This meta-logic formula then holds if for all possible traces of the protocol, and all possible τ over those traces, the BC frames of the protocol are indistinguishable. In the example of the KE protocol of Listing 1, the last line declares the security goal expressing the fact that the key derived by the initiator is indistinguishable from some fresh value k IR , even given all the messages sent over the network. The proof in Squirrel of this goal will be described at a high-level in Section 6.3.3.

We remark however that even though this implies a proof of security for each possible number of sessions, it does not imply the classical security for an unbounded number of sessions because no concrete security bounds are obtained. Over this meta-logic, there are two sets of rules. The first allows proving that some probabilistic statement is true with overwhelming probability, and the second is for proving indistinguishability properties. These two sets interact: for instance, one can first prove authentication properties of a key exchange using rules from the first set, and then rely on these properties to prove the secrecy of the key using the second set.

Squirrel's mechanization

The Squirrel prover is available at [START_REF]The Squirrel Prover repository[END_REF], along with the code of the running example and the case studies. It is an interactive prover with some built-in tactics that simplify low-level reasoning.

From a high-level point of view, most proofs inside Squirrel follow the following schema:

1. prove a set of probabilistic statements inside the dedicated prover, such as matching conversations, or that some bad states cannot be reached;

2. prove the desired indistinguishability, using the probabilistic statements as lemmas.

The second step often relies on an induction over the length of the trace. Concretely, the proof is usually done by assuming that frame P @pre(τ ) ∼ frame Q @pre(τ ) is true, and proving that frame P @τ ∼ frame Q @τ holds. By definition of the frame, this is equal to proving that frame P @pre(τ ), output P @τ ∼ frame Q @pre(τ ), output Q @τ and making a case distinction over possible values of output.

As a concrete example: Fig. 4 in Squirrel takes 20 lines to model, 20 lines of proof, and is then proved by Squirrel in under a second.

Adapting the BC logic and Squirrel to the post-quantum world

Proofs in the BC logic as presented in the previous section do not guarantee security against quantum attackers.

Recall that computational proofs rely on (i) computational assumptions, and (ii) reductions. In the context of the BC logic, the computational assumptions are the easiest to deal with when going to the post-quantum world: if we know that no post-quantum secure instantiations exist for a particular assumption, we can no longer use it in proofs. For example, if a previous proof relied on an axiom that states that integer factorization is hard, the proof is unsound as we can no longer use this axiom in the post-quantum setting.

The complexity of adapting the reductions that follow from the logic mostly revolves around revisiting the assumptions around the term interpretation and the proof rules, which implicitly encode attacker manipulations. Where previously the attacker was modeled using polynomial time Turing machines, we now need to change this to a quantum attacker.

It turns out that this modification is less straightforward than we expected. As explained previously, the classical BC logic uses a term representation that essentially corresponds to a tree in which computations, including those of the attacker, are performed in a purely local fashion. In the classical BC setting, this allows for modeling a single attacker using multiple local attackers: instead of explicitly communicating, subsequent local attackers effectively recompute the results of previous ones. This recomputation was possible since we made all operations deterministic and moved the probabilistic aspects (of both protocol and attacker) to two explicit random tapes. This modeling relies on a classical result for modeling probabilistic Turing machines as deterministic machines with a random tape.

However, for a quantum polynomial time attacker, we have no corresponding result. Notably, a quantum attacker may produce internal random state that we cannot influence nor extract. This phenomenon manifests itself in the so-called no-cloning theorem [START_REF] Wootters | A single quantum cannot be cloned[END_REF]: We cannot duplicate the quantum state of a quantum machine, nor can we run a quantum machine twice and expect to obtain the same inner state.

This directly breaks the stability of the previous interpretation, and for instance, the evaluation of Fig. 2 could now return false. Furthermore, in the interpretation of Fig. 3, we would not be able to recompute inside T att1 the same attacker state as the one computed during T att0 , and therefore this evaluation would not correspond to the run of a single interactive quantum attacker, as was the case for classical attacker. Similarly, the classical BC interpretation also allows for rewinding the attacker, which is impossible for quantum attackers based on the same no-cloning theorem.

We solve these issues by defining an interpretation where the attacker is a single black-box interactive machine, as opposed to a set of one-shot Turing machines. This allows us to verify a set of conditions that when met, ensure that we can provide a sound interpretation for a quantum attacker. Concretely, to interpret att 0 , we query the interactive machine once, and to interpret att 1 (t), we interpret t, and give it as input to the same interactive machine. This effectively changes the term interpretation from a tree to a directed acyclic graph. We will formally define such an interpretation later, but it would intuitively be pictured as in Fig. 5. Changing the term interpretation in this fashion leads to a wide range of subtle changes throughout the logic.

We provide three conditions to ensure that we can give a sound interpretation for a quantum attacker. We provide intuition for them below, and formally define them in Section 4.

Condition 1 -Consistency In the classical BC logic, the attackers need not be consistent. We provide a concrete example, that intuitively corresponds to the simulation of rewinding the attacker. For two distinct terms u, v, consider the sequence of terms att 1 (att 0 (), u), att 1 (att 0 (), v). This corresponds to running att 0 , running its continuation with u, and then making it forget that we ever gave it u (rewind the attacker) and calling it on v.

Against a quantum attacker or black-box attacker, we cannot do this operation, as it morally implies that we are duplicating the attacker's inner state at the end of att 0 , using each copy to run att 1 once on u and once on v.

We therefore add a syntactic condition on terms to forbid such cases, and force that all occurrences of att i are made with the same arguments.

Condition 2 -Monotonicity With the new term interpretation, att 0 and att 1 implicitly share states. This means that when interpreting att 1 , we will always get an answer that depends on the argument previously given to att 0 .

Consider for example the terms: att 0 (n), att 1 () .

= n

In the classical BC logic, the second term would evaluate to false, as att 1 () does not depend on the distribution of n. But if we are forced to interpret the symbols using a black box attacker, the computation of att 1 () does depend on n. Thus, we lose the locality of our logic on some terms, that we will need to restore by further reducing the set of terms. This result in a second syntactic condition, where the arguments of the successive att i must form a growing sequence of terms.

Condition 3 -Balance In the classical BC logic, we can write formulas that do not model interactions between a single attacker with a protocol, and for instance prove indistinguishability formulas that would be trivially false against a single attacker, but true for an independent set of attackers. For instance, consider the formula att 0 () .

= n ∼ att 1 (att 0 (), n ) .

= n . Both sides evaluate to false, because the attacker is completely independent of n (this is the =ind rule). In the classical BC logic, the final distinguisher is also a disjoint machine, which typically does not know how many other attacker machines were executed: therefore, the formula is true in classical BC. This reflects that classical BC allows modeling a weaker threat model with independent attackers. In the PQ-BC interpretation, the final attacker will be a final call to the interactive machine, which of course knows how many times it was previously called.

Thus, under the new and strictly stronger interpretation with a single attacker, some formulas that held under the classical BC logic might no longer hold. We therefore have to ensure that none of our logical rules allows for deriving such formulas. We implement this by introducing a syntactic condition for PQ-BC that essentially requires that the number of attacker calls is balanced, i.e., the number of calls is equal on both sides of an indistinguishability operator, and which will be a side condition of all our logical rules.

Design choices for the conditions While the above three conditions solve issues in designing a post-quantum sound BC logic, they were additionally chosen because they also form a small sufficient set of conditions to derive a usable PQ-BC logic, as we prove in the following section. It would have been possible, for instance, to replace the balance condition by a specific and more refined condition for each logical rule, that as a set would have been equivalent to the balance condition. However, the balance condition is both necessary and more generic, and hence we decide to use this one within PQ-BC. Overall, the three conditions allow for a generic implementation in the Squirrel prover, and yield a logic usable in practice.

We write t or t 1 , . . . , t n for sequences of terms. This notation is not a construction inside the terms, and is thus different to defining a function symbol to model tuples inside terms.

Functional model

Recall that while we consider a quantum attacker, we model honest protocol participants as classical Polynomial Time Turing Machines (PTTMs). To interpret terms, we introduce the notion of a functional model M f , a library implementing the public function symbols and names that are used in the protocol: for each function symbol f (encryptions, signatures,. . . ), T f is a PTTM, which we view as a deterministic machine with an infinite random tape and taking the security parameter as input. The functional model also contains a PTTM T n for each n ∈ N , which will extract from the random tape a bitstring of length η. We give η in unary to the PTTMs, as they are expected to be polynomial time w.r.t. η in the computational model. Definition 2. A functional model M f is a set of PTTMs, one for each name and symbol function, such that:

1. if n ∈ N (i.e., n is a name), n is associated to the machine T n that on input (1 η , ρ s ) extracts a word of length η from the tape ρ s . Different names extract disjoint parts of the random tape.

2. if f ∈ Σ is of arity n, f is associated to a machine T f which, on input 1 η , expects n more bitstrings, and does not use ρ s .

We model public functions as deterministic functions: if randomness is required, it should be given explicitly as an argument to the function symbol. This modeling is needed for the stability of the interpretation.

We can now define the basic interpretation of terms, assuming that we have been given the output bitstring corresponding to each attacker call. Based on this first interpretation, we will then define the one where there is an actual attacker. Definition 3. Given a functional model M f , the security parameter η, a mapping σ from terms att i (φ) to bitstrings, and an infinite sequence of bitstrings ρ s , we define the interpretation of terms such that all occurrences of att i (φ i ) are in the domain of σ as:

[[n]] η,σ M f ,ρs := T n (1 η , ρ s ) , if n ∈ N [[f ( u)]] η,σ M f ,ρs := T f ([[ u]] η,σ M f ,ρs ) , if f ∈ Σ [[att i ( u)]] η,σ M f ,ρs := att i ( u)σ
, for all i

We assume that the functional model contains function symbols that expresses propositional formulas, which are interpreted as expected. We denote those connectives by the . =, . ∧, . ⇒, . . . -note these are marked with a dot.

We will ultimately use two different sets of logical connectives: (1) the dot variants, used in terms, and (2) the variants without a dot that are part of the logic we are building. We will illustrate their combination in Example 7.

Computational Model

To define the interpretation of terms with attacker function symbols, we view terms as directed acyclic graphs from leaves to their root. Example 6. Consider a variant of Example 1, where we denote tuples using . . . :

P := new sk. in(c, x). new r. out(c, enc(x, r, sk)).
in(c, y). new r . out(c, enc( y, x, y , r , sk)).

In the second step, the protocol encrypts the tuple made with twice the second protocol input on and once the first input.

The frame corresponding to this protocol would be t 0 , t 1 :

• t 0 := enc(att 0 (), r, sk)

• t 1 := enc( att 1 (t 0 ), att 0 (), att 1 (t 0 ) , r , sk) We give the original terms and the acyclic graph variant for this frame in Fig. 6.

The acyclic representation leads to a natural interpretation that we can execute even when we are only given access to a black-box straight line attacker, for instance a sequence of {C i } as in Fig. 12. We illustrate this interpretation in Fig. 7. An interesting side effect of this be interpretation, is that the computation time of the simulator actually matches the original execution time of the attacker and the protocol in the real-world. This was not at all the case with the original interpretation of the BC logic, where for instance the interpretation t 0 and t 1 of Example 6 would have executed four times A 0 and two times A 1 . When we model the interactions with an interactive attacker, this corresponds to the high-level change between Fig. 3 and Fig. 5.

We assume that the attacker is an oracle Quantum Turing Machine (QTM) to obtain post-quantum soundness. We provide the formal definition of such machines in Appendix A For our purpose here, it suffices to know that such a machine behaves as a quantum computer that interactively performs oracle queries and receives the answers. Importantly, the oracle queries and answers are classical bitstrings, and do not contain any quantum state. This models a quantum computer interacting over a network with a classical protocol. One can also abstract such an attacker as a straight-line black-box interactive process, which is what we do in most of our proofs. Definition 4. A computational model M A is an extension of a functional model M f , which provides an additional oracle QTM A that takes as input a security parameter 1 η .

Given M A , η, σ, ρ s and ρ r , we define the interpretation [[t]] η M A ,ρs of a term t as: 1. First, evaluate att 0 , by running A on input 1 η until the first oracle query, and store the content of the oracle query tape o inside the substitution σ 0 : {att 0 () → o}.

2. Then, we assume that we have a substitution σ i mapping all occurrences of att j , j < i to a bitstring. We find the smallest subterm occurrence of a att l (t 1 , . . . , t l ) in t. Then, for k from i to l, we write on A's oracle answer tape the value

[[t k ]] η,σ k-1
M f ,ρs , then continue A and wait for the next oracle query, and store the content of the oracle query tape o inside the substitution σ k = σ k-1 ∪{att k (t 1 , . . . , t k ) → o}.

3. Finally, given σ l , where l corresponds to the biggest occurrence of a att l , return [[t]] η,σ l M f ,ρs . This interpretation does not require that a term contains all intermediate calls to the attacker. Thus, interpreting the term att 1 (t) or the sequence att 0 (), att 1 (t) leads to the same interactions with the attacker.

Well-defined interpretation

Our previous definition is not defined over all possible terms: there may not be a unique smallest occurrence of a att l . This is expected, as there exist terms that correspond to experiments that are not realisable with a quantum attacker. Notably, recall that in this context, we cannot interpret the sequence att 0 (), att 1 (u), att 1 (v). Indeed, if the attacker is straight-line and black-box, it means that we can only get one attacker answer corresponding to att 1 . Therefore, to ensure that a term corresponds to a valid experiment with respect to a quantum attacker, we require consistency: att i should always occur with the same arguments in the terms, i.e., corresponds to the same unique call of this attacker's interactive step.

Definition 5 (Consistency). A sequence of terms t is consistent if all function symbol att i occurs with the same arguments.

Lemma 1. [[ t]] η M A ,ρs is well-defined if t is consistent.
Proof. Let M A be a computational model and t a consistent sequence of terms. We show that

[[t]] η M A ,ρs
is well-defined, i.e., that it corresponds to a possible evaluation given the interactive attacker A defined by M A . Recall that A is seen as interacting with an oracle, where intuitively the oracle corresponds to the protocol execution, a query to the oracle is thus an input given by the attacker to the protocol, and the oracle answer is the protocol output.

1. σ 0 simply corresponds to executing A in a black-box fashion until it makes an oracle query. The content of the query is classical (non quantum), and we can thus store this inside σ 0 .

2. We assume that σ i has been computed, that A has made i oracles queries and is waiting for an answer, and that for all subterms t of t that only contain occurrences of att k with k ≤ i, [[t]] η,σi M f ,ρs is well-defined. As t is consistent, there exist a unique smallest subterm occurrence of a att l (t 1 , . . . , t l ) in t such that l is the smallest new index bigger than i. Then, t 1 , . . . , t l only contains occurrences of att k with k ≤ i (otherwise l is not the smallest index bigger than i). By the induction hypothesis, we can thus compute the value of all

[[t k ]] η,σi M f ,ρs , 1 ≤ k ≤ l.
We can thus continue the execution of A, giving him as answer to its i-th oracle query [[t i+1 ]] η,σi M f ,ρs , waiting for its next query and storing it inside σ i+1 , and so on until we submit [[t l ]] η,σi M f ,ρs as answer, and it continues up to its next query, storing the content of the query in σ l .

With 1) and 2), we thus have by induction that σ l can be computed given an interactive quantum attacker, and we can then finally evaluate [[ t]] η,σ l M f ,ρs , which is simply a classical computation (recall that all values in σ l correspond to classical oracle queries made by A. The interpretation is then well-defined.

Restoring locality

In the evaluation of the sequence att 0 (), att 1 (u), att 2 (v, v ), the value of att 2 (v, v ) depends on u in the new interpretation. Yet, this is not reflected inside the term and introduces an implicit dependency that breaks some BC rules as it breaks locality. In particular, it breaks the =ind rule presented in Section 2.

To repair it, we introduce the second term restriction.

Definition 6 (Monotonicity).

A sequence of terms t satisfies the monotonicity restriction if for all occurrences of att i (t 1 , . . . , t i ) and att j (t 1 , . . . , t j ) with i < j, we have for all 1 ≤ k ≤ i that t i = t i .

Essentially, to restore locality, we require that attacker function symbols must always be called on at least the same set of argument as the previous attacker calls.

Note that in the definition of monotonicity, we do not specify that the sequence of attacker calls must be continuous w.r.t. to the indices. For instance, a sequence may contain att 1 but no att 0 . It is essential for the later proofs of protocol, because we sometimes remove some attacker calls in the proof process, replacing them by some other values.

A 0 T r T sk A enc A 1 T <•••> m 0 T enc [[u]] |φ 0 u st att (u) T r v [[v]]
Figure 8:

Those restrictions notably allow to show a lemma that concretely express the locality of the interpretation. The probability that some u evaluates to a value is independent of what we put around of it.

Lemma 2. Let u be a sequence of term. We have for any v such that u, v is a well-formed sequence that for any c ∈ {0, 1} * , any attacker A and computational model

M A , Pr{[[ u]] η M A ,ρs = c} = Pr{[[ u, v]] η M A ,ρs = c, _} Proof.
In this proof, we rely on a notation defined slightly later in Definition 15.

To provide some intuition, we first provide an example based on the interpretation previously presented in Fig. 7. With the notations of Example 6, when interpreting either the sequence t 1 , t 0 or the single element t 1 , the distribution corresponding to t 1 will be the same. This is because t 0 can only reuse some computations of t 1 . We illustrate this in Fig. 8. In general, we could also add a t 2 that would perform further attacker calls, but that would not influence the values returned by the previous attacker calls.

Formally, this holds by Definition 4. Indeed, recall that this Definition of interpretation can intuitively be seen as interpreting bottom-up the acyclic graph, and reusing the previously computed values when needed through the mapping σ. In this definition, we see that the value of [[ u]] is determined by the value given to in the interpretation σ Maxatt( u) . This value is fully determined by the attacker A and the set of syntactical attacker calls of u. As u, v is well-formed, it is notably a consistent, and thus the set of syntactical attacker calls of u, v up to Max att ( u) is equal to the one of u. Thus, the distribution of σ Maxatt( u) when interpreting u, v is the same as the one of σ Maxatt( u) when interpreting u.

Interestingly, recall that in Section 2.1, when we described how to construct a syntactic frame that capture syntactically the attacker interactions with a protocol so that we can see all probabilistic dependencies syntactically, we concluded that we in fact needed to satisfy the monotonicity and consistency restrictions. At the time, we did not express it as a general restriction on terms, but only as a specification of the translation from protocols to terms. Our terms were more expressive, and it was not an issue because we could indeed give a meaning to all sort of terms, either corresponding to a frame or to anything else. In the quantum world, we cannot do so anymore, and we thus directly consider the set of terms that we can consider. But as we want to perform proofs of security protocols, we only care about writing terms that correspond to protocols. And thus, our restrictions will not restrict the proving capabilities of the previous BC logic.

From now on, we only allow in the logic terms that satisfy the consistency and the monotonicity properties.

Interpretation of formulas

Atomic formulas of the logic are built using a set of predicate symbols ∼ n of arity 2n. Given terms t 1 , . . . , t n , s 1 , . . . , s n , the predicate ∼ n (t 1 , . . . , t n , s 1 , . . . , s n ) will be interpreted as computational indistinguishability between the two sequences of terms. We use infix notation, and always omit n as it is clear from the context, thus denoting the previous equivalence by (t 1 , . . . , t n ) ∼ (s 1 , . . . , s n ). The first order formulas are then built using the usual logical connectives ∨, ∧, , ⊥, ⇒, ∃, ∀, ¬. Note that these connectives are not marked with a dot, and are part of the logic, not the terms.

Example 7. Given terms u, v, t, we can write the formula:

(u . ⇒ v) ∼ t ⇔ ( . ¬ u . ∨ v) ∼ t
This formula holds because we assume that for all functional models, . ⇒, . ¬ and .

∨ are classically interpreted.

To define a distinguisher between sequences of terms, we must define this distinguisher as a continuation of the interactive attacker A, and thus pass to it the quantum state of A. This is only a technicality, and in practice we simply consider that the continuation is the last stage of the interactive attacker. Definition 8. Given a computational model M A , and two sequences of ground terms t, u, the formula t ∼ u is satisfied by M A , denoted by M A |= t ∼ u, if, for every polynomial time QTM B,

|Pr ρs {B([[ t]] η M A ,ρs , 1 η , φ t M A ,ρs,η ) = 1} -Pr ρs {B([[ u]] ,η M A ,ρs , 1 η , φ u M A ,ρs,η ) = 1}|
is negligible in η. Here, ρ s is drawn according to a distribution such that every finite prefix is uniformly sampled, and the probabilities also depend on the inherent probabilistic behavior of the two QTMs. The satisfaction relation is extended to full first-order logic as usual.

At a high level, the proof follows naturally from our previous design of a faithful interpretation of terms that is sound for black-box interactive attackers. We directly obtain that by quantifying over all possible M A , the value of [[ t]] η M A ,ρs describes all possible behaviours of the protocol modelled by t interacting with any black-box interactive attacker. Thus, if there exists an attack on the protocol in the real world, it will correspond to an attack on the (computational) interpretation of the terms. Furthermore, because Definition 8 exactly quantifies universally over all M A , if there is an attack on the protocol, the predicate is not valid, and if there is none, it is valid. Finally, because an interactive black-box attacker soundly models a quantum attacker, the logic is shown to be post-quantum sound.

Overwhelming probabilistic truth

The classical BC logic as well as Squirrel has a subset of its rule dedicated to proving the validity of statements of the form u ∼ true.

In our case the attacker A from the computational model and the final distinguisher B share their (quantum) tape, while in the classical BC definition [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF], A and B do not share their working tape, but only their source of randomness Thus, compared to the classical BC definition, as soon as u executes an attacker machine, (u . = u) ∼ true will not hold, as B simply checks if an attacker machine was executed. Note that in the classical BC logic, a proof that u ∼ true is in fact a statement independent of the final distinguisher: we just prove that u is equal to true with overwhelming probability. This is what we call a probabilistic statement.

For PQ-BC, we thus define a predicate dedicated to proving overwhelming probabilistic truth, for which we inherit all the truth rules of BC and Squirrel. Definition 9. Given a computational model M A and a ground term t, T(t) is satisfied by M A , denoted by

M A |= T(t), if, Pr ρs {[[ t]] η M A ,ρs = 1} is overwhelming in η.
The satisfaction relation is extended to full first-order logic as usual.

Post-Quantum soundness

In order to prove the soundness of our logic, we must first define the classical computational indistinguishability of protocols.

Protocols

Our building blocks for protocols are actions. An action essentially models a single protocol step of an input and output that can occur under a condition. The attacker specifies to which actions he wishes to send a value by giving a dedicated channel identifier c from a fixed channel set C. Definition 10. A protocol term is a term without attacker function symbols and built over an infinite set of variables X .

An action A = (c A , x A , φ A , f A ) is given by a channel identifier c ∈ C, a variable x A ∈ X , and two protocol terms φ A , f A .

Intuitively, action A captures the protocol in(c, x A ); if φ A then out(c, f A ) else out(c, 0). We can then define a protocol as a set of such actions, and by adding sequential dependencies between some actions. Definition 11. A protocol is given by a set of actions {A i } and a partial-order < over actions, such that for all

i, f v(f Ai ) ∪ f v(φ Ai ) ⊂ {x B |B < A}.
This definition simply means that some actions must occur before some others, and an action output and condition may only depend on the input variables of the actions that it depends on.

We now define, given a protocol, the protocol oracle that models the protocol behaviour.

Definition 12. Given a functional model M f , a protocol P = {A i }, a security parameter η and an infinite secret random tape ρ s , we define the protocol oracle O P as the stateful oracle that:

1. initializes an empty substitution σ and an empty set of actions E;

2. on input (c, m), it fetches the action A ∈ P such that c A = c, update σ to σ ∪ {x A → m} and E = E ∪ {A} and

• if {B|B < A} ⊂ E and [[φ A ]] η,σ M f ,ρs evaluates to true, returns [[f A ]] η,σ M f ,ρs ; • else returns 0.
In this definition we assume that there is a single action A ∈ P that corresponds to the given channels. Such protocols are called action deterministic, and we will always assume that we are given such protocols.

Indistinguishability

With the definition of a protocol oracle, we can define in the expected sense the post-quantum indistinguishability of two protocols: Definition 13. Given a functional model M f and protocols P, Q, we write P ∼ = Q if for every QTM A, the attacker's advantage Adv P ∼ =Q equal to

|Pr ρs {A O P (1 η ) = 1} -Pr ρs {A O Q (1 η ) = 1}|
is negligible in η.

Soundness

We first formally define the set of frames of a protocol, that is the set of sequence of terms that will capture all the protocols behaviours. We define one such sequence of terms for each possible sequence of actions. Fixing the sequence of actions essentially fixes the sequence of channel identifiers sent by the attacker.

Definition 14. Let P be a protocol. A scheduling τ = A 1 , . . . , A n of the protocol is an executable sequence of protocols actions. Given a scheduling τ = A 1 , . . . , A n , we define inductively the frame ψ τ P as:

• ψ A P := if φ A {x A → att 0 ()} then f A {x A → att 0 ()} else 0; • ψ A 1 ,...,A n P := ψ A 1 ,...,A n-1 P , if φ A {x A → att n-1 (ψ A 1 ,...,A n-1 P )} then f A {x A → att n-1 (ψ A 1 ,...,A n-1 P
)} else 0 Lemma 3. For any P and τ , the sequence ψ τ P satisfies the consistency and monotonicity properties. Proof. Direct by definition.

Based on those definitions, we now prove the post-quantum computational soundness of the logic. Lemma 4. Given two simple protocols P, Q with the same set T of schedulings, a random tape ρ s and a functional model M f , we have:

∀τ ∈ T, ∀M ⊃ M f . M A |= ψ τ P ∼ ψ τ Q ⇒ P ∼ = Q Proof.
Let us proceed by contradiction. We are given a distinguisher B against P ∼ = Q. We thus have,

Adv P ∼ =Q B = |Pr ρs {B O P (1 η ) = 1} -Pr ρs {B O Q (1 η ) = 1}|
is non-negligible. We must find τ and M A such that M A |= ψ τ P ∼ ψ τ Q

Find a trace τ

We split this probability, by conditioning over the observable traces. We denote by E τ the event "τ is the scheduling produced by B".

By dichotomy, we have

Adv P ∼ =Q B = |Pr ρs {B O P (1 η ) = 1} -Pr ρs {B O Q (1 η ) = 1}| = τ ∈T Pr ρs {E τ }× |Pr ρs {B O P (1 η ) = 1 | E τ } -Pr ρs {B O Q (1 η ) = 1 | E τ }|
We of course have that for any τ , Pr ρs {E τ } ≤ 1. We thus obtained the following upper-bound.

Adv P ∼ =Q B ≤ τ ∈T |Pr ρs {B O P (1 η ) = 1 | E τ } -Pr ρs {B O Q (1 η ) = 1 | E τ }|
As the advantage is overwhelming, so is the sum. Recall that as P and Q are simple, they are finite, and in particular T is finite. Now, we classically have that a finite sum is overwhelming if and only if one of its element is overwhelming. Thus, there exists a trace τ such that |Pr ρs

{B O P (1 η ) = 1 | E τ } -Pr ρs {B O Q (1 η ) = 1 | E τ }| is overwhelming.

Build the model M A

Let us consider this τ of length n given. We consider two QTM A and B , where A is B running until the last oracle query of B when B follows τ , and B is the remainder of B. A and B return a fixed default value when B does not follow the scheduling τ .

By definition of their construction, ψ P τ exactly matches the oracle answers from the execution of B O P when it follows the trace τ .

Thus, in the model M A defined by M f with attacker machine A , the oracle answers from the execution of B O P follows the same distribution as the [[ψ τ P ]] η M A ,ρs when conditioning over E τ . Thus, we have that whenever we condition over event E τ , B and B distinguish with the same probability, i.e.,

|Pr ρs {B ([[ψ τ P ]] η M A ,ρs , 1 η ) = 1 | E τ } -Pr ρs {B ([[ψ τ Q ]] η M A ,ρs , 1 η ) = 1 | E τ }| = |Pr ρs {B O P (1 η ) = 1 | E τ } -Pr ρs {B O Q (1 η ) = 1 | E τ }|
Thus, both of these terms are overwhelming, and we have that Notice that with our interpretation of terms, the soundness is actually simpler to prove than the original soundness proof of [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF], which need to split the original attacker into many multiple pieces. Furthermore, the total running time of the attacker machines is the same, in the logic or in the original computational model. This will be a key point that will enable us to instrument the logic with concrete security bounds.

|Pr ρs {B ([[ψ τ P ]] η M A ,ρs , 1 η ) = 1} -Pr ρs {B ([[ψ τ Q ]] η M A ,ρs , 1 η ) = 1}| is also overwhelming. In other terms, B is a witness that M A is a computational model such that M A |= ψ τ P ∼ ψ τ Q , which concludes the proof. =-refl T(u . = u) =-ind T(u . = n) when n is not a subterm of u =-sym T(u . = v) T(v . = u) =-trans T(u . = v) T(v . = w) T(u . = w) =-subst T(u 1 . = v 1 ) . . . T(u n . = v n ) T(h(u 1 , . . . , u n ) . = h(v 1 , . . . , v n ))

Logical rules

Probabilistic statements

We introduce some of the logical rules to reason about the T() predicate, which are all direct transpositions of the rules of the BC logic that are statements about formulas of the form u ∼ true. Their soundness proofs are completely similar, as the corresponding BC rules are in fact sound for any Turing Machine, even with unbounded computational power. This means that if the premices are valid, so are the conclusions. We present in Fig. 9 a subset of such rules that allows to reason about the equality between terms, with the other rules being transposed similarly. = is a PPTM which interprets a symmetric predicate, the interpretation of the term is equal both in the premice and the conclusion of the rule.

=-trans

For any model M A , thanks to the premices, we have that

Pr ρs {[[u . = v]] η M A ,ρs = 1} ≤ f (η) Pr ρs {[[v . = w]] η M A ,ρs = 1} ≤ g(η)
where f and g are negligible functions. So, we have that u . = v with overwhelming probability Pr u . =v = (1 -f (η)), and v .

= w with overwhelming probability Pr v . =w = (1 -g(η)). The probability that the two events happens at the same time is Pr u .

=v∧v

. =w = Pr u . =v + Pr v . =w -Pr u . =v∨v . =w ≥ Pr u . =v + Pr v . =w -1 ≥ 1 -f (η) -g(η)
=-subst We assume that Pr ui . =vi = (1 -f i (η)) is overwhelming. Then, we have that:

Pr h(u1,...,un) . =h(v1,...,vn) ≥ Pr 1≤i≤n ui . =vi ≥ Pr u1 . =v1 + Pr 2≤i≤n ui . =vi -Pr u1 . =v1∨ 2≤i≤n ui . =vi ≥ Pr u1 . =v1 + Pr 2≤i≤n ui . =vi -1 ≥ 1≤i≤n Pr ui . =vi -(n -1) ≥ 1≤i≤n (1 -f i (η)) -(n -1) ≥ 1 -1≤i≤n f i (η)
=-indep Thanks to the monotonicity property of u, the distribution of u is completely defined by its set of subterms. As n does not occur in the term u, the distribution of u and n are independent,

Pr ρs {[[u . = n]] η M A ,ρs = 1} = c Pr ρs {[[u]] η M A ,ρs = c ∧ [[n]] η M A ,ρs = c} = c Pr ρs {[[u]] η M A ,ρs = c} × Pr ρs {[[n]] η M A ,ρs = c} = c Pr ρs {[[u]] η M A ,ρs = c} × 1 2 η = 1 2 η REFL u ∼ u TRANS u ∼ v v ∼ w u ∼ w PERM (u 1 , . . . , u n ) ∼ (v 1 , . . . , v n ) (u π(1) , . . . , u π(n) ) ∼ (v π(1) , . . . , v π(n) ) SYM v ∼ u u ∼ v FRESH u ∼ g v ( u, n) ∼ g ( v, n )
when the new names do not occur in u, v α-equ u ∼ uα when α is an injective renaming of the names

FA u ∼ v h( u) ∼ h( v) RESTR ( u, s) ∼ ( v, t) u ∼ v when Max att ( u) = Max att ( v) DUP ( u, t) ∼ ( v, t) ( u, t, t) ∼ ( v, t, t) EQU T(s . = t) ( u, s) ∼ g ( u, t) when Max att ( u, s) = Max att ( u, t) IFT u, C[if s . = t then C 0 [s] else w] ∼ v u, C[if s . = t then C 0 [t] else w] ∼ v CS ( w, b, u) ∼ ( w , b , u ) ( w, b, v) ∼ ( w , b , v ) ( w, if b then u else v) ∼ ( w , if b then u else v ) when Max att ( w, b, u) = Max att ( w, b, v) = Max att ( w , b u ) = Max att ( w , b , v )
Figure 10: Indistinguishability rules of PQ-BC. We mark new side conditions in blue.

Indistinguishability rules

As mentioned earlier, some statements of classical BC are false under the single-attacker interpretation. For example, u ∼ true is false as soon as u contains an attacker symbol, because the final distinguisher also executes the corresponding attacker call, and could therefore differentiate the sides. Yet, such statements are provable inside BC, because it does not assume the final distinguisher sees all attacker calls. Thus, the existing BC rules are not correct in our new interpretation, and we must add a side condition to make PQ-BC sound. Similar to the rules for the truth predicate T(), the indistinguishability rules in Fig. 10 are also sound for any attacker, without any assumption on their computational power. Thus, the soundness issues only come from the fact that the distinguisher B now inherits the state of the attacker A. In the end, the main case where an existing BC rule becomes unsound is when it yields in the conclusion a ∼ statement where the attacker A is not called the same number of times on both sides, which corresponds to the balance condition.

Definition 15 (Balance). Given a sequence of terms u, we denote by Max att ( u) the biggest index i such that the function symbol att i appears in u. We say that u ∼ v satisfies the balance conditions, or is balanced, if Max att (u) = Max att (v).

Definition 16. We denote by st att ( u) the subterm of u with att Maxatt( u) as the top-level function symbol.

Most BC rules can then be transformed to PQ-BC rules by additionally requiring the balance condition over their indistinguishability. In practice, we will thus require that the balance condition holds over all indistinguishabilities appearing inside the proof tree. In the following, however, we only add the side condition where it is needed, in order to pinpoint which rules may break the balance condition. We present in Fig. 10 the new corresponding set of rules, using the color blue to indicate the new side-conditions. Note that the consistency and monotonicity conditions are enforced globally, and hence also hold for all terms appearing in rules. The CS rule requires a stronger condition than the balance condition. Though we provide it for completeness, this rule is not used in Squirrel nor in PQ-Squirrel, and the balance condition is thus sufficient for their rules to get post-quantum soundness. Lemma 6. The indistinguishability rules, shown in Fig. 10, are sound in the PQ-BC interpretation.

Intuitively, this means that whenever we construct a proof in the logic, then if there is an attack on the proven formula, there is an attack on the axioms. If we combine this with the soundness of the logic, we get that a proof in the logic implies the existence of a post-quantum sound reduction from an attack on the protocol to an attack on post-quantum sound cryptographic assumptions.

A 0 T r T sk A enc A 1 m 0 T enc [[u]] t 0 |φ 0 u st att (u) [[st att (u)]] T r
Figure 11:

By symmetry to the previous case, we can obtain that the advantage of B e in To show that the balance condition is not enough to restore the post-quantum soundness of the rule CS, we consider the following example.

M A against w, b, v ∼ w , b , v is |p l,t -p r,

Example 8.

if true then n else att 1 (n) ∼ if true then n else att 1 (n )

This equivalence does not hold in PQ-BC, as att 1 is always executed independently of the condition, and thus the final distinguisher always gets the value of n. However, if CS was sound just with the balance condition, we could prove the previous statement by proving:

true, n ∼ true, n ∧ true, att 1 (n) ∼ true, att 1 (n )
And both of those statements could trivially be proved true in the post-quantum setting.

We recall that we can still only consider the balance condition for PQ-Squirrel, as Squirrel does not rely on the CS rule, it only relies on its equivalent regarding probabilistic statements. Note that if one day the CS was needed in Squirrel, we could make it sound with the balance condition by adapting the PQ-BC interpretation, so that only the attacker symbols appearing in the executed branch of the conditional are executed. This would however make the interpretation depend explicitly on a fixed function symbol, and it would not be generic anymore.

Lemma 7. Let u be a sequence of term. For any attacker A, we denote by φ v A the (quantum) configuration reached by A during the computation of [[ v]] η M A ,ρs (which we do not denote by φ v A,M A ,ρs,η for concision). This corresponds to the quantum state forwarded to the final distinguisher B.

Let A be an attacker. We first have that

φ u A = φ statt( u) A (1)
We have for any v such that u, v is a well-formed sequence that

Max att ( v) = Max att ( u) ⇒ φ u A = φ v A ( 2
)
And if we set A as the attacker that drops all queries bigger than Max att ( u) and forwards the others to A, and set is final state as the final one of A, we have:

Max att ( u) ≤ Max att ( v) ⇒ φ u A = φ v A ( 3
)
PQ-BC yields guarantees for post-quantum attackers under the assumption that the previous axioms are instantiated in a post-quantum secure way, e.g., by a protocol that uses CRYSTALS-Dilithium [START_REF] Ducas | Crystals-dilithium: A lattice-based digital signature scheme[END_REF] to instantiate EUF-CMA, and see e.g. [67] for a post-quantum sound instantiation of a PRF. Out of these assumptions, the most debatable w.r.t. instantiability is likely ENC-KP, as discussed recently in [START_REF] Grubbs | Anonymous, Robust Post-Quantum Public Key Encryption[END_REF].

Mechanization in PQ-Squirrel and Case Studies

In this section, we describe PQ-Squirrel, our extension of Squirrel that produces post-quantum sound proofs in the PQ-BC logic. We give an overview of the post-quantum protocol analysis results that we obtained using PQ-Squirrel in Table 1. As we will show later, it turns out that despite the new term interpretation and corresponding new side conditions, several existing Squirrel proofs could be re-interpreted by PQ-Squirrel as post-quantum sound proofs in PQ-BC.

6.1 PQ-Squirrel

Ensuring post-quantum soundness

To make Squirrel post-quantum sound, we must specify which cryptographic axioms are post-quantum sound, and enforce the three syntactic side conditions from Definitions 5, 6 and 15. Furthermore, if there are cryptographic assumptions for which we know instantiations that are secure against classical attackers, but do not know any post-quantum secure instantiations, we no longer rely on them.

Recall that a substantial amount of work in adapting the BC logic to PQ-BC was due to the flexibility in specifying multiple attackers. In contrast, Squirrel specifications do not include attacker terms: Squirrel automatically produces the attacker terms from the input and output commands in the process specification, under the assumption that there is only one attacker. Concretely, the attacker terms are produced by the interpretation of input P @τ , which is equal to att τ (frame P @pre(τ )). While this means that Squirrel only supports a subset of the BC logic, it strongly simplifies protocol specification for the user, and prevents users from accidentally modeling a weaker threat model with multiple disjoint attackers. For our post-quantum purposes, this historical choice is very convenient: all terms produced by the meta-logic of Squirrel already satisfy the consistency and monotonicity properties.

We still need to ensure that PQ-Squirrel verifies the new side conditions w.r.t. the Max att () on both sides of the indistinguishability formulas from Fig. 10. Given a meta-logic formula u ∼ v, we need to check that for the maximal timestamp element τ of the trace, input@τ appears on both sides. If this is the case, we say that a formula satisfies the synchronization property.

We cannot check the synchronization property directly since Squirrel internally omits the inputs from the frames when they are redundant, and would lead to falsely discarding proof steps. We instead check a generalized property, which is true if either input@τ or frame@τ or frame@pre(τ ) occurs in the frame.

Lemma 9. Let Γ ⇒ u ∼ v be a meta-logic formula of the classical BC and Squirrel, where Γ is a set of ordering constraints over the timestamp variables appearing in u and v. Let Max Γ be the set of maximal elements implied by the partial ordering. If for all τ in Max Γ , we have that there exists an element e in {input@τ frame@τ, frame@pre(τ )} such that e ∈ u and e ∈ v, then, we have that:

Γ ⇒ ( w, u ∼ w, v ⇔ u ∼ v)
where w := input@τ 1 , . . . , input@τ k when Max Γ := {τ 1 , . . . , τ k }.

Further, every meta-logic rule that applies to u ∼ v can also be applied to w, u ∼ w, v.

Proof. In this proof, we refer to the rules of the Squirrel meta-logic from [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF]. By Restr, we can easily show that ( w, u ∼ w, v ⇒ u ∼ v). For the converse, we reason by case analysis over each τ i inside Max Γ .

• if input@τ i appears in u and v, we have that u ∼ v ⇒ u, input@τ i ∼ v, input@τ i using Dup.

• if frame@pre(τ ) does, we have that u ∼ v ⇒ u, input@τ i ∼ v, input@τ i using Fa-Dup.

• if frame@τ does, we first duplicate it with Dup, then expand the macro to add frame@pre(τ ) to frame (using Restr to drop the extra element of the frame, and then we are in the previous case. Now, given a proof step applied to u ∼ v, the same proof step can be applied over w, u ∼ w, v. Indeed, all the meta-logic rules allow for an extra context. And the side condition verified over this context are 1: PQ-Squirrel case studies: we constructed new models of key exchange protocols with static key compromise, and revisited previous Squirrel protocol models. PQ-Squirrel proves that these protocols are computationally post-quantum secure when they are implemented with post-quantum secure primitives for each of their assumptions.

performed by reasoning over the set of subterms appearing inside the frame. But w does not contain any new subterm.

This Lemma instantly gives us that any Squirrel proof where all indistinguishability predicate satisfy the extended synchronization condition can be mapped to a proof where the Max att () side condition is verified everywhere.

Implementation

PQ-Squirrel can operate in classic Squirrel mode. Additionally, it offers a post-quantum-mode switch that can be enabled inside proof files. When enabled, PQ-Squirrel operates in post-quantum mode: it only allows tactics and axioms that have been proven post-quantum sound, and checks synchronization for every indistinguishability appearing at any step of a proof.

The source-code of PQ-Squirrel is available at [START_REF]The Squirrel Prover repository[END_REF]. Thanks to our identification of a minimal set of simple syntactic conditions, the PQ-Squirrel extension could be concisely implemented, and only comprises a few hundred line of codes in addition to Squirrel's code base.

Case studies

We summarize the case studies we performed using PQ-Squirrel in Table 1. They fall into two categories: new case studies for the Internet Key Exchange (IKE) standards and of key exchange protocols based on Key-Encapsulation Mechanisms (KEMs); and previous Squirrel case studies that we could prove post-quantum sound in PQ-Squirrel.

All model files and the prover are at [START_REF]The Squirrel Prover repository[END_REF]. Required effort: In total, modeling the protocols took in the order of hours, and constructing their proofs in interaction with PQ-Squirrel took in the order of weeks. PQ-Squirrel verifies each resulting proof file in under 10 seconds on a laptop with a quad-core CPU at 1,8GHz.

As a side contribution, we also developed new generic tactics for the prover that enabled the case studies. We first present case studies in Sections 6.3 and 6.4, and then introduce the new tactics in Section 6.5.

Key exchange case studies: IKE and KEM-based

Threat model and security properties

We modeled five key exchange protocols, for which we proved, e.g.:

• Authentication -if a party accepts, another accepts (with the same parameters).

• Strong Secrecy -the keys derived by the parties are indistinguishable from fresh random values.

In these initial case studies, we consider the same threat model for all key exchange protocols: an arbitrary number of initiators and responders willing to answer to anybody, including to dishonest/compromised identities with attacker-controlled keys. We did not yet prove properties with respect to dynamic corruptions nor more complex security properties like perfect forward secrecy, and we consider them out of scope for this work. We stress however that in a similar fashion to EasyCrypt and CryptoVerif, PQ-Squirrel does not have any hard-coded threat model, and these case studies can be extended in future work.

IKE case studies

The IKE standards, version 1 [START_REF] Kaufman | Internet Key Exchange Protocol Version 2 (IKEv2)[END_REF] and 2 [START_REF] Kaufman | Internet Key Exchange Protocol Version 2 (IKEv2)[END_REF], specify suites of key exchanges. They are Diffie-Hellman key exchanges that support multiple authentication modes. RFC 8784 [START_REF] Fluhrer | Mixing Preshared Keys in the Internet Key Exchange Protocol Version 2 (IKEv2) for Post-quantum Security[END_REF] addresses the issue of quantum computers breaking the DDH assumption, and its authors claim that the authentication mode based on a pre-shared key in version 1 (IkeV1 psk ) is post-quantum sound. For the same purpose, they also define a way to extend version 2 so that the final key computation depends on a pre-shared key.

For IkeV1 psk , we use PQ-Squirrel to prove that a pre-shared key between two entities allows to derive an authenticated secret key indistinguishable from a random.

We also analyze the version 2 protocol with signatures for the authentication and extended with the pre-shared key, which we call IkeV2 sign psk . The proof of IkeV2 sign psk is simpler than IkeV1 psk , because the signatures simplify the derivation of the authentication property.

KEM based key exchanges

KEMs are currently considered as a possible replacement for DH-like key exchanges. KEMs abstract mechanisms that generate and send fresh key material encrypted to another party, from which both parties derive a fresh shared key. Some generic constructions of KEM based key exchanges have been proposed in [START_REF] Boyd | One-round key exchange in the standard model[END_REF][START_REF] Fujioka | Strongly Secure Authenticated Key Exchange from Factoring, Codes, and Lattices[END_REF], and have for instance been expanded into a full alternative to TLS in [START_REF] Schwabe | Post-Quantum TLS Without Handshake Signatures[END_REF] or as post-quantum sound variants of the Signal X3DH handshake [START_REF] Hashimoto | An efficient and generic construction for Signal's handshake (X3DH): Post-quantum, state leakage secure, and deniable[END_REF]. These key exchanges were specifically designed to not rely on any DH-like operations, and their security instead relies on assumptions on the corresponding KEM constructions, i.e., IND-CCA.

In PQ-Squirrel, we generally model KEM-based key exchanges by modeling some common internals of KEMs: generating fresh key material, sending this encrypted to the other party, and then deriving a key from this material at both parties using a key derivation function.

The basic KEM-based key exchange pattern is to perform the KEM operation at both parties with respect to their peer's long-term public keys, and then to xor the two resulting fresh keys (one for each direction). This generic pattern was illustrated in our example from Fig. 4. As the knowledge of both fresh keys is needed to derive the final key, the attacker cannot obtain it unless it knows both long-term private keys. Note that such schemes provide implicit authentication, but not (explicit) authentication: only a trusted party can derive the final key, but there is no guarantee that such a party exists.

In our specification, we use enc to talk about an abstract KEM construction, while in practice, it is referred to as the encapsulation mechanism, and the decryption is the decapsulation. Presenting it using an encryption symbol directly allows to model it inside PQ-Squirrel, but this does not affect the validity of the proofs.

For all our KEM based case studies, our models include an unbounded number of initiators with distinct secret decapsulation keys sk I , each willing to initiate an unbounded number of sessions with any honest responder with encapsulation key pk R , as well as an unbounded number of honest responders willing to engage with an unbounded number of sessions with any arbitrary public key that may be attacker-controlled.

Recall that a generic KEM based construction does not provide explicit authentication properties; thus, for KEM based key exchange we only prove the strong secrecy of the derived keys. In our basic example of Fig. 4, this would be achieved in three steps, first by using IND-CCA to hide the secret ephemeral keys k I and k R from the attacker; second by using the PRF assumption to derive valid keys, i.e., showing that kdf(e x ) is indistinguishable from a fresh random n x ; third by using the OTP assumptions that enforces the one-time pad property, and thus that the final key is indistinguishable from random, as it is always equal to n x ⊕ t for some t and fresh random bitstring n x . For illustration purposes, the actual PQ-Squirrel proof corresponding to this example can be found along with the other case studies at [START_REF]The Squirrel Prover repository[END_REF]. Interestingly, the proofs carried out in PQ-Squirrel follow this high-level structure for the multiple KEM based case studies, and were thus straightforward to establish.

Concrete case studies

The KE BCGNP protocol closely follows the generic pattern. KE FSXY uses an additional ephemeral key used for each session, as well as an additional round of PRF application to the key materials before xor-ing them. We prove the strong secrecy of the derived keys for both protocols.

The SC-AKE protocol, intended as a possible post-quantum replacement of Signal's X3DH, can be seen as a variant of KE FSXY extended with a third message send from the Responder to the Initiator, containing a signature to provide a form of deniable authentication. Instead of deriving a single key k := kdf(sid, e i ) ⊕ kdf(sid, e r ), it derives two keys k s and k f using kdf1 and kdf2. The first one is used to xor, and thus hide, the signature of the sid sent for authentication, and the second one is the derived key. Because of these constructions and their properties, SC-AKE is our most complex case study. The proof first requires proving the authentication of the responder to the initiator, by relying on the EUF-CMA assumption on the signature. After having shown that the material used by the initiator to derive the secret key is from an honest source, we can show that the secret key is strongly secret by following the previous pattern. Such proofs illustrate a strength of the PQ-Squirrel prover: it allows interactions between a part of the logic dedicated to proving reachability properties (e.g. authentication), and then use those properties inside indistinguishability proofs (e.g. secrecy).

Proving post-quantum soundness of Squirrel case studies

We used PQ-Squirrel to verify the proofs of the nine previous Squirrel case studies. Out of those, PQ-Squirrel was able to prove that six were post-quantum sound, and three were not, as they relied on the DDH assumption.

Thus, it seems that most existing proofs in Squirrel are already post-quantum sound, even though we know it is possible to prove statements in Squirrel that are not post-quantum sound. This appears to be because the proofs of realistic protocols rely on an induction on the length of the trace. We then reason on frames of protocols and prove that each of their possible last messages does not break the indistinguishability. This pattern seems to avoid violating the balance condition.

Additional tactics

A Non-Malleability tactic

Squirrel already had a tactic for the IND-CCA axiom, which is the one usually used for KEM. However, the IND-CCA axiom is not only used to provide secrecy in the context of KEM, but also a form of weak authentication. If a party receives the ciphertext of something that corresponds to an honest ephemeral share, then there exists a session of an honest initiator that sent it. To prove such an authentication property, the IND-CCA axiom is ill-suited, because we rely on the non-malleability property of the scheme, which is implied by IND-CCA [START_REF] Bellare | Relations among notions of security for public-key encryption schemes[END_REF][START_REF] Nagao | On the equivalence of several security notions of key encapsulation mechanism[END_REF]. We developed a new tactic that allows to say that encrypted honest secret share cannot have been tampered with by the attacker, and must have been sent by some honest party. We provide details in Appendix C Using this tactic, we could directly prove the weak authentication of the schemes.

Global tactics

Inside Squirrel proofs, we often consider statements of the form frame@pre(τ ), t frame@pre(τ ), t

We then show that t and t are indistinguishable while leaving the frame abstract. Most Squirrel tactics only allow manipulating the terms appearing inside t and t . However, we sometimes need to perform actions globally: not only on t and t but also on the terms that may appear inside frame@pre(τ ), i.e., all the terms inside the protocol. We implemented four new tactics that enable such global manipulations:

• a tactic to globally substitute a name by a fresh name;

• a tactic that allows to prove the indistinguishability of two protocols by proving their functional equivalence, i.e., that they in fact produce exactly the same distributions with overwhelming probability;

• an IND-CCA2 tactic to replace all occurrences of some cipher by a version with perfectly hidden plaintext; and

• a PRF tactic to replace all occurrences of the hash of a given message by the same random.

In comparison, the original Squirrel tactic for PRF only allows to replace one instance of a hash inside t by a random as long as one can prove this hash was never computed before by the protocol. Details are provided in Appendix D

7 Current limitations and future work

Minimality of the syntactic conditions

Each of the three syntactic conditions is needed to forbid unsound operations over quantum attackers, as illustrated by the three examples in Section 3. However, they may not be the minimal possible conditions, and our conditions do reduce expressivity. Notably, our current restrictions rule out zero knowledge proofs, whose security analysis often requires rewinding. However, our current assessment is that any weakening of the conditions would inherently be very domain specific, and thus only useful for a small set of protocols.

For instance, while we could have loosened the consistency condition to allow for some particular form of post-quantum sound rewinding [START_REF] Unruh | Quantum proofs of knowledge[END_REF][START_REF] Watrous | Zero-knowledge against quantum attacks[END_REF], all such techniques are dedicated to particular cases. We currently believe it would be very difficult to derive a general post-quantum rewinding technique (see e.g. [START_REF] Ambainis | Quantum attacks on classical proof systems: the hardness of quantum rewinding[END_REF]).

Scope of the tool

In terms of security properties, we have already used PQ-Squirrel to verify a range of properties like unlinkability, anonymity, strong secrecy, and authentication. In general, it allows expressing properties using arbitrary first-order logic formula, which can mix indistinguishability properties and reachability properties, and can thus be used to express all classical security properties. For protocols, PQ-Squirrel cannot currently carry out proofs that require rewinding or that are in the ROM, but such restriction do not hinder proving a wide range of protocols from the literature. As discussed previously, it is unclear which kind of rewinding should be integrated currently in Squirrel. Integrating the ROM (and QROM) into PQ-BC and PQ-Squirrel could be interesting future work. However, while (Q)ROM is often needed for the analysis of primitives, it is less often needed for protocols. A class of protocol we cannot typically verify are e-voting protocols, that often rely on the ROM. However, there is a long-standing debate on the ROM model, because it is not realizable in practice. Typically, it is often preferable to use the PRF assumption when a secret seed is derived in the protocol, as we did in our case studies. In other cases, integrating results such as [START_REF] Rogaway | Formalizing human ignorance[END_REF] into PQ-BC might offer a solution in the future.

Besides protocols whose proofs require rewinding or the ROM, we are not aware of any inherent limitations of the logic or the prover that would hinder the proofs of other post-quantum protocols.

Refining the case studies

The goal of our case studies is to show the usability and scalability of the tool, not to provide an exhaustive analysis of each of them. For example, our current key exchange analysis only consider a model with static compromise. However, this is not an inherent limitation of the logic, and the threat model is only part of the protocol modeling. As such, a natural future work is to refine our case studies and try to prove more advanced properties such as PFS or PCS.

Improving automation

Based on our first set of case studies, PQ-Squirrel shows the potential to tackle complex case studies such as the proposal of a recent post-quantum TLS [START_REF] Schwabe | Post-quantum TLS without handshake signatures[END_REF]. Performing such complex case studies would benefit from improving the automation in PQ-Squirrel. We see two main possible routes to achieve this. First, some low level reasoning about message equalities and inequalities is already automated in many cases, but could be improved by leveraging SMT solvers. Second, the unique abstraction level of our logic enables us to reason both at the high-level of the executions traces as well as at the low level of the indistinguishability of two messages. This abstraction opens the door for the application of more advanced constraint solving techniques, similar to the one used in symbolic tools, which can further improve automation.

Conclusion

We defined the PQ-BC logic for proving protocol security against quantum attackers, and a corresponding PQ-Squirrel prover to mechanize the reasoning. In the process of extending the BC logic for this purpose, we identified three simple syntactic side conditions that are both necessary and sufficient; these conditions, and the new tactics we developed for PQ-Squirrel, can be useful for the classical setting as well. Our initial case studies show that PQ-Squirrel can be effectively used to prove post-quantum protocol security.

[66] A Chi-Chih Yao. Quantum circuit complexity. In Proceedings of 1993 IEEE 34th Annual Foundations of Computer Science, pages 352-361. IEEE, 1993.

[67] Mark Zhandry. How to construct quantum random functions. Journal of the ACM (JACM), 68(5):1-43, 2021.

A Preliminaries on Quantum computing

We first present generalities about quantum computation with circuits, manipulating computation model for security similar to [START_REF] Gagliardoni | Quantum Security of Cryptographic Primitives[END_REF][START_REF] Song | A note on quantum security for post-quantum cryptography[END_REF]. As in the security context, attackers are more often described as Turing Machines, we then provide a high level definition of Quantum Turing Machines with access to a classical oracle.

Though we provide those preliminaries for completeness, remark we will not manipulate quantum states in the following. In the context of our logic, we will only perform black-box straight line reductions, where given an quantum attacker A, we construct a classical attacker B with oracle access to A, and A is only executed in a straight line fashion. Those reductions directly yield post-quantum security, if the assumptions are post-quantum secure. When we will need to bound explicitly the probability of success of polynomial time quantum machine, we will bound the probability of success of a polynomial space classical Turing Machine. Those two facts ensure that we do provide valid reduction to prove post-quantum security, but allow us to ignore the inner workings of quantum machines.

A.1 Quantum Computing with circuits In quantum systems, a (pure) state is described by a vector |φ in some Hilbert space H. We only wish to consider quantum circuits, and thus systems operating over Hilbert spaces of the form H = C N with N = {0, 1} * to model sequences of qbits. We consider a fixed orthonormal basis {|x | x ∈ N }, which is the computational basis. Each element of the computational basis is a classical state, and every pure quantum states can be seen as a superposition of elements of the computational basis. We now define the machine model, corresponding to a simplified version of the model of [START_REF] Unruh | Universally Composable Quantum Multi-party Computation[END_REF]. A quantum circuit operates on a state in H quant ⊗ H class and returns a state in H quant ⊗ H class , where H quant is a quantum state and H class is a classical state1 . Quantum circuit cannot perform all possible operations over quantum states, but details are not relevant to this work.

C 0 C 1 P 0 P 1 |φ 0 m 0 |φ 1 . . .
An interactive machine C is described by a sequence of quantum circuits {C i k } operating over H quant ⊗ H class , where intuitively H quant is the state of the machine, H class is used for incoming and outgoing messages, and C i k is the circuit ran at steps i of the execution, when the security parameter is equal to k. An interactive machine is quantum-polynomial-time if there exists a deterministic polynomial time classical Turing Machine that on input 1 k outputs the description of the sequence of circuits C i k . We now define the execution of an interactive quantum machine C with a protocol P . A protocol is simply an interactive quantum machine, and thus a sequence P i k of circuits. Fixing the k, we denote by |φ i ⊗ |m i the output of C i , and ψ i × l i the output of P i . |φ corresponds to the state passed between the C i , |m i is measured and given as input to P i and ψ i is the state passed between the P i . We describe informally in Fig. 12 the beginning of such an execution, where red wires are quantum, and black wires are classical. The execution of {C i k } interacting with {P i k } is given by, at step i, computing the result

|φ i ⊗ |m i of C i k over |φ i-1 ⊗ |l i-1
, where this is empty when i = 0, or ψ i-1 × l i-1 is the result of P i-1 over ψ i-1 ⊗ m i-1 , m i-1 being the result of the measurement of |m i-1 .

A.2 Quantum Computing with Turing Machines

In the following, we consider Post-Quantum Turing Machines with access to oracles, that have an input tape, a working tape, an output tape extra, and oracle query and answer tapes. We refer the reader to [14, Section 3] for the formal definitions of a Quantum Turing Machine.

Intuitively, a QTM can maintain a superposition of configurations, where one of the configuration can itself transition to a superposition of configurations, yielding the linear combination of the superposition. The final output of a QTM is obtained by measuring the quantum state, which corresponds to collapsing the superposition to a single one, where the probability to obtain a given configuration is specified by the superposition.

An oracle QTM can query an oracle by going inside a dedicated state, and writing the oracle input on a dedicated tape. It then gets in a single step the answer of the oracle. Note that in our case, we only have classical oracles, which means that oracle inputs are measured, and outputs are classical. It also means that to perform a query, all configurations in the superposition must be in a query state to perform a measurement and query the oracle.

Formally, we assume as given the Definitions of [14, Section 3] for multi-track Quantum Turing Machines. Such a machine accepts if it goes inside a superposition of configuration such that all configurations Definition 17. Given a classical Oracle O : {0, 1} * → {0, 1} * , an oracle Quantum Turing Machine is defined as a four tape Turing Machine, an input, a working tape, an output tape and an oracle query tape, with two dedicated pre-query and post-query states. When the Turing-machine is executed, it produces a linear superposition of configuration by following its transition table. Additionally, when all configurations of the superposition are in the pre-query state, in a single step of computation, the oracle query tape is measured, and its content is used as input for O, and then replaced by the oracle answer, and all configurations in the superposition go to the post-query state.

This model can also be seen as a sequence of QTM without oracle, with quantum input, quantum working tape and classical output. The first classical output is measured when the machine halts, it is given to the oracle, and then we run the second machine with quantum input the concatenation of the classical oracle answer and the content of the working tape of the previous machine.

Note that QTMs are equivalent to circuit based definitions [66] and thus our approach is similar to [START_REF] Gagliardoni | Quantum Security of Cryptographic Primitives[END_REF][START_REF] Song | A note on quantum security for post-quantum cryptography[END_REF]. See [START_REF] Boneh | Random oracles in a quantum world[END_REF] for a discussion on differences between classical and quantum oracles.

Given an oracle O, We denote A O a QTM with classical access to O. An execution of such a machine can be intuitively seen as a sequence of quantum computations interleaved with some partial measurements of the quantum state for oracle calls.

Polynomial time quantum computing is known to be more powerful than probabilistic attackers, but not more than polynomial space attackers (BPP ⊂ BQP ⊂ PSPACE [14, Theorem 8.3&8.4]). It allows us to bound the probability of success of a quantum attacker by bounding the probability of success of a polynomial space attacker.

B A rewinding example in BC

We provide in this section a small example of a proof of a protocol in the BC logic that relies on a rewinding, and describe how it breaks with our additional conditions. We use to this end the small MPC rewinding example of [START_REF] Backes | On the Necessity of Rewinding in Secure Multiparty Computation[END_REF]. Lemma 10. We can prove in the classical BC logic that the previous protocol securely implements f mult with perfect security in the stand-alone model.

Proof. We consider an attacker replacing Bob, whose first (output for Alice) and final outputs are denoted by att 1 (b, _) and att 2 (b_), where the hole corresponds to the input received by Bob. With those notations, we can write the final value of Alice as t A = if a = 0 then 0 else if att 1 (b, a) / ∈ {1, 2} then 1 else att 1 (b, a).

Security when Bob is corrupt is when there exists simulators s 1 , s 2 allowed to use att 1 and att 2 such that f (a, s 2 ) .

= t A (a), s 1 . = att 2 (b, a) ∼ true, true

We set: s 2 := if att 1 (b, 1) / ∈ {1, 2} then 1 else att 1 (b, 1) s 1 := if f (a, s 2 ) = 0 then att 2 (b, 0) else att 2 (b, 1)

If we evaluate the terms by case disjunction:

a t A f (a, s 2 ) = a × s 2 s 1 0 0 0 att 2 (b, 0) 1 s 2 s 2 (∈ {1, 2}) att 2 (b, 1)
This concludes the proof, modulo a tedious casting of the case disjunction inside the BC logic.

The good news is that the previous security proof breaks in the PQ-BC logic, because s 2 does not satisfy the consistency condition!

C The non malleability version of the IND-CCA 2 axiom

We define a new BC axiom that corresponds to the non malleability of a ciphertext. We rely on the axiom for Indistinguishability against Chosen Ciphertexts Attacks from [START_REF] Bellare | Relations among notions of security for public-key encryption schemes[END_REF] and its multi-users variants [START_REF] Bellare | Public-key encryption in a multi-user setting: Security proofs and improvements[END_REF].

First, the challenger computes a public/private key pair (pk(n), sk(n)) (using a nonce n of length η uniformly sampled), and sends pk(n) to the attacker. The attacker has access to two oracles: There already exists formalisations of the IND-CCA 2 axiom, see e.g. [START_REF] Koutsos | Preuves symboliques de propriétés d'indistinguabilité calculatoire[END_REF]. Yet, they are difficult to use in order to prove authentication, as they force us to render encryption after encryption the attacker view independent of the secret challenge used to establish some authentication, and finally, prove that only the honest execution can pass all the test of the protocol. To prove the strong secrecy of a name, an easily usable rule however, is CCA1.

To take a slightly different approach, we take ideas from the non-malleability axiom, and provide a reachability axiom, that says that the attacker cannot produce a message that has a significant link with a secret that it never saw non encrypted.

We propose the following base logic axiom REACH-CCA 2 , for all t, C, s such that

• sk only occurs in key position t, C, s;

• n only occurs under encryptions performed by keys that only occur in key position in t, C, s;

• n is fresh;

• all decryptions occurs under encryptions;

• all encryptions use valid fresh randomness. Intuitively, the attacker cannot produce the ciphertext of a message that holds a significant relation with n, as n only occurs under honest encryptions. Thus, unless it forwards an honest encryption, it cannot produce the term t(n), which holds a significant relation with n. The fact that t(n) holds a significant relation to n is witness by the fact that t(n) . = t(n ) ∼ false.

t(n)

Proposition 1. The axiom REACH-CCA 2 is sound in all models where the encryption is multi-user IND-CCA 2 .

Proof. Let us assume that we have a model that contradicts an instance t, C, s of the axiom, and thus a model where = t(n ) evaluates to true with negligible probability Pr t . We show how to construct an attacker that wins the IND-CCA 2 game with a non-negligible advantage.

The attacker B first receives pk(sk). Then it samples himself all the names occurring in the term s, t, C, and samples a duplicate n of n. The attacker is then going to simulate the construction of two messages in parallel, one intuitively corresponding to the message C[dec(s, sk)], and the other one to the same message, where all occurrences of n have been replaced by occurrences of n . To do so, consider the pair S(t) defined recursively by:

• S(n) = (n, n )

• S(f ( u)) = (f ( v l ), f ( v r )) when ( v l , v r ) = S( u) (we write as a shortcut f (m), to denotes the fact that the attacker simulates the PTTM corresponding to the function symbol f , either using a machine from the functional model, or an attacker machine from the model negating REACH-CCA 2 )

• S({u} r pk(sk) ) = (m, m), where m is the answer of O b LR (sk) given as input the pair S(u).

• S(dec(u, sk)) = (m l , m r ) where, with (u l , u r ) = S(u), if u l = u r is the result of a query (m l , m r ) to the left-right oracle, and else m l m l (resp. m r ) corresponds to the value returned by the decryption oracle over query u l (resp. u r ). Now, one can easily check that the couple S(s) = (s l , s r ) satisfies the property that, when b = 0, s l is the interpretation of s, and when b = 1, s r is the interpretation of s[n → n ]. Note that s r when b = 0 corresponds to the interpretation of some term that mixes n and n , and we cannot say a lot about it. Furthermore, for every term in which n only occurs under encryption, s l = s r , as the two components are made equal whenever we encounter an encryption symbol (the result of the left-right oracle), and are only made dis-equal when encountering n.

Equipped with the definition of S, the attacker B then performs the following steps:

1. compute (s l , s r ) = S(C(dec(s, sk))); 2. returns t(n) = s l .

We know that n only occurs under encryption symbols. Thus, in the execution of B, we have that s l = s r . Further, we have that, when b = 0, s l has exactly the same distribution as C[dec(s, sk)], and thus B outputs true with non-negligible probability Adv REACH-CCA2 . When b = 1, the distribution of s r is completely independent of n (the left-right oracle always returned the part of the pair depending only on n ). We can conclude if Pr(s l = t(n)) is negligible.

By contradiction, let us assume that Pr n,ρ (s l = t(n)) is non-negligible (where we denote ρ r all randomness on which depends s l ), then there exists a constant c such that Pr n (c = t(n)) is non-negligible. Indeed, sup c (Pr n (c = t(n))) is non-negligible, as: Finally, Pr n,n (t(n ) = t(n)) = Pr n,ρ (s l = t(n)) 2 is non-negligible, which contradicts the fact that t(n) = t(n ) with negligible probability Pr t . Thus, when b = 1, B outputs true with at most probability Pr t , and thus outputs true with negligible probability.

We conclude that we have a distinguisher against the IND-CCA 2 game, which outputs true with non-negligible probability when b = 0, and with negligible probability when b = 1. Transposing to KEMs The IND-CCA 2 axioms for KEM is in fact slightly weaker than the one for publickey encryption schemes. Instead of asking that the ciphertexts of any two messages are indistinguishable, it only asks that the ciphertext of a key is indistinguishable from the ciphertext of a uniformly sampled key.

Note that BC axioms, both for IND-CCA 2 and CCAreachtwo, can easily be restricted to model this behaviour, by asking that we only consider ciphertexts over names.

We refer the reader to [START_REF] Nagao | On the equivalence of several security notions of key encapsulation mechanism[END_REF] for multiple notions of non-malleability over KEMs.

C.1 Rules inside Squirrel

We provide in Fig. 13 the reachability rule NM2 for Squirrel.

= t(n)

.

⇒ false ∼ true

We then obtain the soundness of the final rule with a small derivation:

Figure 1 :Figure 2 :

 12 Figure 1: enc(att 0 (), r, sk)

Figure 3 :

 3 Figure 3: Final BC simulation of attacker/protocol interactions. Note the recomputation of, e.g., T att0 .

Figure 5 :

 5 Figure 5: Quantum compatible simulation of attacker/protocol interactions without recomputation in PQ-BC. Compare this to Fig. 3.

Figure 6 :Figure 7 :

 67 Figure 6: From the classical BC to the acyclic graph representation in PQ-BC

Definition 7 .

 7 Let v be a sequence of term. For any computational model M A , we denote by φ v M A ,ρs,η the final (quantum) configuration reached by A during a computation of [[ v]] η M A ,ρs .

Figure 9 :

 9 Figure 9: Truth rules of PQ-BC (identical to those of BC)

Lemma 5 .

 5 The truth rules, shown in Fig.9, are sound in the PQ-BC interpretation.Proof. =-refl In any model, u . = u evaluates to true with probability 1.=-sym As.

m 1 ψ 1 Figure 12 :

 112 Figure 12:

Definition 18 .

 18 The functionality f mult takes an input a ∈ {0, 1} from Alice and an input b ∈ {1, 2} from Bob and returns a × b.If we have a term t A (resp. t B ) corresponding to the output of Alice (resp. Bob), we easily write in a term the result of the function as t A × t B .We consider the following protocol: Alice := in(c, a); out(bob, a); in(alice, r) if a = 0 then out(c, 0) else if a = 1&r / ∈ {1, 2} then out(c, 1) else out(c, r) Bob := in(c, b); in(alice, a); if a / ∈ {0, 1} then out(alice, 0); out(c, 0) else out(alice, a × b); out(c, a × b)

•

  The left-right oracle O b LR (n), that takes two messages m 0 , m 1 , and returns {m b } r pk(n) , where b is a Boolean. • The decryption oracle O dec (n), that given m, returns dec(m, sk(n)), if m does not correspond to an output of the left-right oracle, and a sequence of zeros of length m otherwise.

=

  t(n ) ∼ false ⇒ if . {x} r pk(sk) ∈s s . = {x} r pk(sk) then C[dec(s, sk)] . = t(n) else false ∼ false

  dec(s, sk)] . = t(n) evaluate to true with non-negligible probability Adv REACH-CCA2 , and t(n).

  Pr n,ρ (s l = t(n)) = c Pr n,ρ (c = t(n) ∧ c = s l ) = c Pr n (c = t(n)) × Pr n,ρ (c = s l ) < c sup c (Pr n (c = t(n))) × Pr ρ (c = s l ) ≤ sup c (Pr n (c = t(n))) × c Pr ρ (c = s l ) ≤ sup c (Pr n (c = t(n))) × 1

Figure 13 :

 13 Figure 13: Rule NM2 (meta logic)

Proposition 2 .

 2 NM2 is sound in any model where the encryption is multi-user IND-CCA 2 . Proof. Let us denote by H = . {x} r pk(sk) ∈s s . = {x} r pk(sk). First, we trivially derive from the base logic the soundness of the following rule:NM-aux ∅ t(n) . = t(n ) Γ, H, C[dec(s, sk)] . = t(n)) false Indeed, assume t(n) . = t(n ) ∼ false (which is equivalent to t(n) . = t(n ) ∼ true).Then, the base-logic axiom gives us if H then C[dec(s, sk)] . = t(n) else false ∼ false Now, negating this, we get if H then C[dec(s, sk)] . = t(n) else true ∼ true which translates in therm of implication to H . ⇒ C[dec(s, sk)] .= t(n) ∼ true, and we have:H . ⇒ C[dec(s, sk)] . = t(n) ∼ true ⇔ ¬H ∨ C[dec(s, sk)] . = t(n) ∼ true ⇔ ¬(¬H ∨ C[dec(s, sk)] . = t(n)) . ⇒ false ∼ true ⇔ H ∧ C[dec(s, sk)].

  ∅ t(n) = t(n ) Γ, H, C(dec(s, sk)) = t(n) false Γ, C(dec(s, sk)) = t(n) ¬H Γ, ¬H, C(dec(s, sk)) = t(n) φ Γ, C(dec(s, sk)) = t(n) φ

  t | up to a negligible quantity. To conclude, we observe that the advantage of B in M A against s ∼ t is |p l,t + p l,f -p r,t -p r,f |, which is upper-bounded by triangle inequality by |p l,t -p r,t | + |p l,f -p r,f |. AS the advantage of B is non-negligible, it follows that at either the advantage of B t or B e must also be, and thus one of the premice is false.

Table

	Protocol	LoC	h	Primitives and Assumptions sign enc	⊕	Security properties
			New case studies of key exchange protocols
	IkeV1psk [23]	850	PRF				Strong Secrecy & Authentication
	IkeV2 sign psk [37, 44]	300	PRF	EUF-CMA			Strong Secrecy & Authentication
	KE BCGNP [21]	355	PRF		IND-CCA	OTP	Strong Secrecy
	KE FSXY [38]	620	PRF		IND-CCA	OTP	Strong Secrecy
	SC-AKE [41]	745	PRF	SUF-CMA	IND-CCA	OTP	Strong Secrecy & Authentication
		Proving post-quantum soundness of Squirrel case studies [5]
	Basic Hash [22]	100	PRF				Authentication & Unlinkability
	Hash Lock [43]	130	PRF				Authentication & Unlinkability
	LAK (with pairs) [42]	250	PRF				Authentication & Unlinkability
	MW [52]	300	PRF			OTP	Authentication & Unlinkability
	Feldhofer [36]	270			ENC-KP INT-CTXT		Authentication & Unlinkability
	Private Authentication [7]	100			ENC-KP IND-CCA		Anonymity

  A measurement allows obtaining probabilistically classical state from a quantum state, where the measurement of x a x × |x will yield state |x with probability |a x | 2 . Given separate systems H 1 , H 2 , we describe the joint systems with the tensor product H 1 ⊗ H 2

	Every pure state can thus be written
	as:
	|φ =

x a x × |x where x |a x | 2 = 1.

  sk P 1 ,P 2 pk(•),enc(_[dec(_,•)],_,pk(•)) C, t, s n P 1 ,P 2 enc(•,•,pk(•)) C, t, s n P 1 ,P 2 C, t, s senc-rand P 1 ,P 2

	NM2	.
	∅ t(n)	. = t(n ) Γ,	{x} r pk(sk) ∈s	s	. = {x} r pk(sk) , C(dec(s, sk))
					sk

. = t(n) φ Γ, C(dec(s, sk)) . = t(n) φ

PQ-BC: A Post-Quantum BC logicIn this section we first provide the core of the formal definition of the PQ-BC logic: its term interpretation that is suitable for post-quantum attackers, as well as the consistency and monotonicity conditions needed to ensure the stability and locality of the logic. This interpretation allows to consider a single interactive attacker, rather than a set of single-one shot attackers. We then prove the computational soundness of the logic with the new interpretation. This implies that the logic can be used to obtained computational guarantees against quantum attackers. Second, we provide the structural rules of the logic, as well as the balance condition needed to prove the rules sound in the post-quantum setting. Finally, we discuss which cryptographic axioms -and thus which corresponding BC axioms -can be used inside the logic to get post-quantum soundness of a protocol analysis.While we directly refer to a quantum attacker in definitions and proofs, we actually design a logic with an interpretation and rules that are computationally sound for any interactive black-box attacker. The attacker can be instantiated as a Polynomial Time attacker, or a Quantum Polynomial Time attacker, or even an unbounded Turing machine attacker. It is only the cryptographic assumptions used inside a given proof that restrict the attacker's computational power.4.1 Syntax and SemanticsWe use terms to model random samplings, public function computations by honest parties, and black-box attacker computations. For random samplings, the BC logic inherits some conventions from the Pi calculus: notably, fresh values (such as nonces) are called names (and have nothing to do with identities); by convention, variables called n, n , . . . are names and hence freshly generated values. In Example 1 r, r , and sk would also be modeled as names. Let N be a set of names. Names can be seen as fixed identifiers, where each is a pointer to a uniformly sampled bitstring. Let Σ be a set of function symbols, the set used for public functions and primitives. Let {att i | i ∈ N} be a set of function symbols such that att i is of arity i for each i ∈ N. Definition 1. We consider terms built according to the syntax: t ::= n ∈ N name (fresh value) | f (t 1 , . . . , t k ) function symbol f ∈ Σ | att i (t 1 , . . . , t i ) i-th attacker call

we only separate the two for clarity, but it could be encoded into a single quantum state

Acknowledgments. We thank Hubert Comon for many interesting discussions.

Proof. Most of the proofs are transpositions of proofs from [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF][START_REF] Koutsos | Preuves symboliques de propriétés d'indistinguabilité calculatoire[END_REF], where we additionally rely on Lemma 7 to show the additional information given to the distinguisher B through the state φ u A of the interactive attacker A does not allow it to distinguish the terms.

• REFL The distributions are exactly the same on both sides.

• TRANS The result is direct by triangle inequality over the three advantages.

• PERM We easily obtain a simulator by mixing the inputs.

• FRESH As the names are fresh, there distribution is independent of the other terms. And taken in isolation, an attacker as a null advantage to distinguish two uniform distributions.

• SYM The definition of the interpretation of ∼ is symmetric.

• α-equ Names are all pointers to independent uniform distributions, so applying an injective mapping over them does not change the distribution of the terms.

• FA Applying a deterministic function to the attacker input strictly decreases its advantage. (intuitively, the deterministic function can only reduce the quantity of information available to the attacker)

• RESTR We are given a model with attacker A and distinguisher B against u ∼ v. Similarly to Lemma 7,we set A as the attacker that drops all queries bigger than Max att ( u) and forwards the others to A, and set is final state as the final one of A. As we have Max att ( u) ≤ Max att ( u, s), we have by Lemma 7 that

A . • EQU As it is slightly longer, we push this proof in Lemma 8.

• IFT In the positive branch of the conditional, we are replacing two terms that have exactly the same distribution with overwhelming probability. Note that this crucially rely on the locality property.

• CS We assume the premices. With s = w, if b then u else v and t = w , if b then u else v , let A and B be attackers against s ∼ t. We let p l,t , p l,f , p r,t , p r,f be the following quantities:

We define the attacker B t against w, b, u ∼ w, b , u :

. With this, and based on the definition of B t , we can conclude that:

1. In the example of Fig. 11, we can see that as soon as we finished interpreting st att ( u), the rest of the computation becomes completely independent of the attacker. Thus, the set of the attacker after

, else, u, v would not satisfy the consistency property. We conclude with (1).

By construction of A .

This Lemma directly allows us to link oblivious and non-oblivious indistinguishability.

Lemma 8. For any terms s, t and any sequence of terms u such that Max att ( u, s) = Max att ( u, t), we have that:

Proof. The left-hand side of the implication directly implies that Pr ρs,A {[[s

, and we also have that

ρs is negligible, we can apply the same function to both and still have a negligible distance, we thus now that the following is negligible for any B.

We now look at the final state of the attacker A. As s .

= t, u, s and u, t are all well-formed, we also have that u, s, u, t is well-formed. Thus, as Max att ( u, s) = Max att ( u, t), we have by Lemma 7 that φ u,t A = φ u,s A . We can thus conclude that the following is negligible

And thus, we do have that u, s ∼ u, t.

Cryptographic assumptions in PQ-BC

In Section 2.4 we discussed how BC encodes cryptographic assumptions, such as PRF, IND-CCA, EUF-CMA, ENC-KP, INT-CTXT, OTP, and DDH. The original proofs of soundness of these encodings in [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF][START_REF] Koutsos | Preuves symboliques de propriétés d'indistinguabilité calculatoire[END_REF] were aimed at a classical attacker. We revisited all these proofs, and due to their direct black-box nature, it turns out these proofs also directly apply against a post-quantum attacker: if there exist an instantiating that satisfies the assumption against a quantum attacker, then the corresponding BC axiom is post-quantum sound. However, knowing that a BC rule is post-quantum sound w.r.t. the cryptographic assumption does not mean that we know an instantiation (i.e., a concrete scheme) that is secure with respect to a quantum attacker. While we know instantiations for most of the above assumptions with respect to a classical attacker, at this moment we do not know of a post-quantum secure instantiation of the DDH assumption. In the future, a candidate for post-quantum DDH could be the CSI-DDH [START_REF] Kawashima | An efficient authenticated key exchange from random self-reducibility on CSIDH[END_REF] assumption, based on the CSIDH assumption [START_REF] Castryck | CSIDH: An efficient post-quantum commutative group action[END_REF]. Their concrete security is however the subject of discussions [START_REF] Daniel J Bernstein | Quantum circuits for the CSIDH: optimizing quantum evaluation of isogenies[END_REF][START_REF] Biasse | A note on the security of CSIDH[END_REF][START_REF] Bonnetain | Quantum security analysis of CSIDH[END_REF][START_REF] Peikert | He gives C-sieves on the CSIDH[END_REF]. We therefore omit this for now from list of allowed cryptographic assumptions for PQ-BC.

This yields the following list of currently usable PQ-BC axioms for post-quantum proofs: PRF, IND-CCA, EUF-CMA, ENC-KP, INT-CTXT, and OTP. Concretely, this means that a proof in

and HFresh k (t; u

D Global tactics

Most of the meta-logic rules are local, in the sense that they apply to a term in one position, and not to the full protocol at once. This can be cumbersome, even on some simple examples. Let us consider for instance the following protocol:

! i (out(hash(n(i), k)|(out(hash(n(i), k)

Intuitively, when the hash function satisfy the PRF assumption, this protocol should be indistinguishable from:

To prove it, we need to replace in two different output the same hash by the same random value. However, the existing tactic for PRF in Squirrel intuitively allow to prove the following: frame@pre(τ ), hash(n(i), k) frame@pre(τ ), if Cond then r(i) else hash(n(i), k)

Where Cond is a formula dedicated to this instance, that asks that the hashed message was not hashed before in the frame. It essentially allows to replace a hash by a random name only the first time this given hash is computed.

We provide three new tactics, which instead of reasoning only over the explicit terms of the current frame we are investigating, also allow performing protocol wide transformations.

D.1 Extended PRF

We first recall the existing PRF rules for the base and the meta-logic in Fig. 14.

We provide a new base logic rule, that can be derived from the previous one. We let G-PRF be the axiom such that, for all sequences u and term t, we have u σ ∼ u when

• σ is the substitution such that for all H(m, k) ∈ st( u ),

Lemma 11. The axiom G-PRF is sound in all models where H is a PRF.

Proof. We assume that n ∈ st( u , t) and k H(_,•) ( u , t), First, note that the original rule directly implies u σ PRF ∼ u where σ 1 maps H(t, k) to if HFresh k (t; u , t)thennelseH(t, k) with HFresh k (t; u

Using this variant of the rule, we proceed in two steps. First, we consider σ 1 the substitution such that for all H(m, k) ∈ st( u ), We are only introducing a trivial if then else, so we do have that u σ 1 ∼ u . We can then go once step further, and highlight the fact that in the else branch, m <> t, with σ 2 the substitution such that for all H(m, k) ∈ st( u ),

Once again, the interpretation of the conditional is such that u σ 2 ∼ u σ 1 . Let us now apply the PRF axiom over u σ 2 for H(t, k). It yields that u σ 2 ∼ u σ 3 with σ 3 the substitution such that for all H(m, k) ∈ st( u ),

Now, we actually have for any H(m, k) ∈ st( u σ 2 ) \ {H(t, k)} that m <> t, as such m are all of the form if m = t then m else 0.

So in fact, we get that HFresh k (t; u σ 2 , t) is equivalent to true. And thus, that u σ 3 ∼ u σ 4 with σ 4 the substitution such that for all H(m, k) ∈ st( u ),

We directly conclude by reverting if m = t then m else 0 to m and by transitivity.

Note that we made a proof based on the previous rule, but it could have also been made directly as a reduction from the cryptographic axiom.

D.1.1 Meta logic rule

We now introduce the meta logic rule. We recall that ∆ P1,P2 u ∼ v is used to denote that the macros are expanded on the left-hand side according to the protocol P 1 and on the right according to P 2 .

Lemma 12. G-PRF is sound in all model where H satisfies the PRF assumption.

Proof. Recall that to prove the soundness of a meta logic rules, we only have to show that for all possible expansions of the terms, the rule correspond to some valid implication in the base logic.

Our rule is in fact directly a multiple application of the G-PRF rule, one for each copy of t and of k. This is because the tryfind construct is expanded as follows, in a simple case where l is an integer and the key and message only depend on a single index:

With this expansion, it becomes clear that the rule is obtained by apply the base logic rule G-PRF first to H(t [START_REF]The Squirrel Prover repository[END_REF], k [START_REF]The Squirrel Prover repository[END_REF]), then H(t [START_REF] Almeida | A Machine-Checked Proof of Security for AWS Key Management Service[END_REF], k [START_REF] Almeida | A Machine-Checked Proof of Security for AWS Key Management Service[END_REF]), . . . . This rule when used with messages that depend on the attacker may appear counter-intuitive. Let us for instance consider the protocol:

By applying G-PRF to H(x l , k), we get

Here, the else branch would never be taken, and if for instance the attacker performs the inputs x 0 = 0, x 1 = 1, x 3 = 0, the frame would be n[0], n [START_REF]The Squirrel Prover repository[END_REF], n[0].

D.2 Global rewritings

We also introduce two very basic tactics, to help reason globally over some systems. They are both direct consequences of rules of the base logic, that are simply lifted to protocols.

D.2.1 Renaming

For any renaming of a name n into a fresh name n , we have that ∆ P1,P1σ u ∼ u σ.

D.2.2 Equal

We may sometimes do the proof of an indistinguishability by instead proving that all the terms inside the protocols are in fact equal with overwhelming probability.

Recall that in the meta-logic, we define a set of action names A, and a concrete action for a ∈ A is given by a(φ, o) where φ and o are terms. A protocol P 1 is then a set of concrete actions, and we denote by A P1 the set of actions of a protocol.

G-PRF

∅ a(φ1,o1)∈P1,a(φ2,o2)∈P2 for a∈A P 1

Recall that ∆ P1,P2 u ∼ u is not a trivial goal, as we can for instance have u := frame@τ .

D.3 Extended IND-CCA 2

We also provide a generalized version of the IND-CCA 2 predicate. We let G-CCA be the axiom such that, for all sequences u , term t and name r, we have u σ ∼ u when

• σ is the substitution such that:

We define the G-CCA experiment in the classical computational game-based setting as follows:

Recall the IND-CCA 2 description of Appendix C. We actually prove in the computational model that the security of IND-CCA 2 implies the one of G-CCA. The soundness of the G-CCA BC axiom naturally follows as it is a completely direct translation.