Cédric Fournet
email: fournet@microsoft.com

Markulf Kohlweiss
email: markulf@microsoft.com

Pierre-Yves Strub
email: pierre-yves@strub.nu

Modular Code-Based Cryptographic Verification

Keywords: K.6.m [Security and Protection]: Security; F.3.1 [Specifying and Verifying and Reasoning about Programs]: Specification techniques Security, Verification, Languages Cryptography, refinement types, security protocols. 1. TYPECHECKING CRYPTOGRAPHY

Type systems are effective tools for verifying the security of cryptographic programs. They provide automation, modularity and scalability, and have been applied to large security protocols. However, they traditionally rely on abstract assumptions on the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions using lower level, computational models that precisely account for the complexity and success probability of attacks. These models are more realistic, but they are harder to formalize and automate.

We present the first modular automated program verification method based on standard cryptographic assumptions. We show how to verify ideal functionalities and protocols written in ML by typing them against new cryptographic interfaces using F7, a refinement type checker coupled with an SMT-solver. We develop a probabilistic core calculus for F7 and formalize its type safety in COQ.

We build typed module and interfaces for MACs, signatures, and encryptions, and establish their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces. We illustrate our method on a series of protocol implementations.

One long-standing challenge for reliably building secure software is to integrate cryptographic expertise with general-purpose program verification.

Several research tools provide automated security analysis of code that uses cryptography; they can deal with sample protocol implementations written in C [START_REF] Goubault-Larrecq | Cryptographic protocol analysis on real C code[END_REF][START_REF] Chaki | ASPIER: An automated framework for verifying security protocol implementations[END_REF][START_REF] Dupressoir | Guiding a general-purpose C verifier to prove cryptographic protocols[END_REF] or in ML [START_REF] Bhargavan | Verified implementations of the Information Card federated identity-management protocol[END_REF][START_REF] Bhargavan | Cryptographically verified implementations for TLS[END_REF][START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF][START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF]. These tools can verify complex properties and reveal logical flaws in protocol designs and implementations. On the other hand, they rely on strong, symbolic assumptions on the underlying cryptographic primitives, treated as black boxes, as initially proposed by Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF]. They formally restrict the power of the attacker, and are often at odds with weaker guarantees considered by the cryptographers who actually design and implement these primitives. In symbolic models, for instance, each primitive constructs syntactically-distinct symbolic terms, each subject to distinct rewrite rules, which makes it difficult to reflect attacks where the same bitstring may be successfully decrypted and parsed using different keys and message formats. Similarly, brute-force attacks on concrete bitstrings used as keys or passwords, or side-channel attacks on binary formats are difficult to reflect symbolically.

Formal Computational Cryptography

The semantics of computational models are more complex, as they must account for adversaries with bounded computational capabilities and for small probabilities of failure, even with correct primitives and protocols. More fundamentally, computational models reason about partial specifications of cryptographic primitives. Instead of giving, for instance, rewrite rules that completely define their behavior, cryptographers provide minimal positive functional guarantees: what the protocol requires to run as intended, e.g. decryption of a correctly encrypted plaintext with the correct key will succeed; and minimal negative security assumptions: what a computationallybounded adversary cannot achieve, except with a negligible probability, e.g. distinguish between encryptions of two different plaintexts. Thus, computational proofs must apply parametrically, for any concrete primitives that meet those functional and security hypotheses.

Direct vs Indirect Approaches

The relation between symbolic and computational models for cryptography has been an active subject of research for the last ten years [see e.g. [START_REF] Laud | Semantics and program analysis of computationally secure information flow[END_REF][START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF][START_REF] Backes | The reactive simulatability (RSIM) framework for asynchronous systems[END_REF]. Despite impressive results, computational soundness holds only for a fraction of the primitives and patterns supported by symbolic verification tools; it also restricts their usage (for instance demanding tags to disambiguate parsing) and requires non-standard assumptions [e.g. type-n security, 3]. Thus, to tackle the details of existing protocol designs and implementations, with their own choice of cryptographic primitives and properties, one usually cannot first verify them symbolically then apply a generic computational soundness theorem. As advocated by Halevi [START_REF] Halevi | A plausible approach to computer-aided cryptographic proofs[END_REF], Datta et al. [START_REF] Datta | Probabilistic polynomial-time semantics for a protocol security logic[END_REF], Blanchet [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF], Barthe et al. [START_REF] Barthe | Formal certification of ElGamal encryption[END_REF][START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF], we follow a more direct approach: we design and adapt automated verification techniques for computational cryptography, rather than hypothetical symbolic abstractions.

Typing Cryptographic Primitives Types naturally capture partial cryptographic specifications. In the context of communications security, protocol code can be typechecked against abstract interfaces for their primitives, then linked to any implementation that meets this interface, with guaranteed security for the resulting executable. For example, Laud [START_REF] Laud | Secrecy types for a simulatable cryptographic library[END_REF][START_REF] Laud | On the computational soundness of cryptographicallymasked flows[END_REF] adapt type systems for symbolic security and establish their computational soundness with relatively minor changes to the typing rules.

Symbolic Typechecking with F7 (Review) Bengtson et al. [START_REF] Bengtson | Refinement types for secure implementations[END_REF] develop a general-purpose refinement type system and a prototype typechecker (F7) for verifying the code of protocols and applications written in F#, a dialect of ML for the .NET platform. Bhargavan et al. [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF] extend their method by designing symbolic libraries for a wide range of cryptographic primitives and patterns and evaluating the performance of typechecking versus global verification by ProVerif, a leading protocol verifier [START_REF] Abadi | Analyzing security protocols with secrecy types and logic programs[END_REF]. Their approach relies on dual implementations for cryptography: a concrete implementation links to systems libraries and is used for running the protocol; another symbolic implementation defines cryptography in terms of programming-language abstractions such as seals [START_REF] Morris | Protection in programming languages[END_REF] and algebraic data types. Formally, security holds only within the symbolic model. Following Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF], concrete security also depends on a careful assessment of the presumed capabilities of adversaries versus those enabled by the symbolic libraries.

Cryptographic Verification with F7 In this paper, we introduce a modular method for programming and verifying cryptographic systems. Using F# and F7, we build computationally sound libraries for sample functionalities, and we use them to program and verify sample protocols. Our method is as follows: for each cryptographic functionality,

• we write a new refinement-typed ideal interface that captures its security guarantees;

• we program and typecheck an ideal implementation for this functionality, thereby verifying its security;

• we show how to substitute concrete cryptographic implementations for the ideal one, while preserving its security for all well-typed programs that use the functionality, under standard assumptions coded as games in ML.

We then automatically verify programs and protocols that use these functionalities by typechecking against their ideal interfaces. Although these interfaces differ from those used for symbolic verification, the F7 verification framework still applies; we can in particular re-typecheck existing code against our new interfaces, and thus verify their security in the computational model without modifying their specification. Our contributions are as follows:

(1) We adopt the "code-based game-playing" approach advocated by Bellare and Rogaway [START_REF] Bellare | The security of triple encryption and a framework for code-based game-playing proofs[END_REF] for writing precise cryptographic proofs: we reason on cryptography using ML programs (rather than Turing machines) and conduct our security proofs by programming, typechecking, and reasoning on ML code ( §2 to §6).

(2) We develop a probabilistic variant of RCF, the core typed calculus for F7. We have formalized our calculus and most of its metatheory in COQ [START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8[END_REF], including all the key typing lemmas such as type safety and parametricity ( §2).

(3) We program typed ideal functionalities for MACs and signatures, and establish their soundness for authenticity, assuming CMA security ( §3).

(4) We define a notion of perfect secrecy and show how to automatically verify it by typing using parametricity ( §4).

(5) We program parametrically typed ideal functionalities for CPA and CCA2 secure encryption, and establish that they are indistinguishable from concrete encryption ( §5).

(6) We evaluate our method on cryptographic constructions, such as hybrid encryption and encrypt-then-MAC, and security protocols, including large implementations previously verified using symbolic models. To our knowledge, these are the largest protocols verified in the standard model ( §6).

Our approach is modular, since the existence of ideal interfaces and implementations can be established separately for each cryptographic functionality, and since their composition preserves security. (Symbolic verification lacks this form of modularity, as it relies on a single definition of symbolic terms.) Our ideal implementations correspond to ideal functionalities in the universal composability model [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]; as required, concrete and ideal implementations are indistinguishable for all well-typed environments. Similarly, our use of refinement typed interfaces for ideal functionalities may be seen as a form of conditional simulatability [START_REF] Backes | Conditional reactive simulatability[END_REF].

The code fragments and interfaces listed in this paper are part of typed, executable programs. The source files, the formal COQ development, and a companion paper with additional details and proofs are available online. Related Work We discuss only closely related work on cryptographic type systems, computational soundness for symbolic cryptography, and verification tools for computational cryptography. As regards perfect secrecy, our definitions and proof techniques rely on parametricity, a classic approach for symbolic security [see e.g. [START_REF] Morris | Protection in programming languages[END_REF][START_REF] Abadi | Secrecy by typing in security protocols[END_REF][START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF].

We adapt an existing type system and its implementation, but do not attempt to design a new one for reasoning about probability distributions or polynomial-time complexity. Many type systems have been developed specifically for computational cryptography, notably in the context of information flow security [e.g. [START_REF] Laud | Secrecy types for a simulatable cryptographic library[END_REF][START_REF] Laud | On the computational soundness of cryptographicallymasked flows[END_REF]. Beyond type systems, other verification techniques also rely on logical properties of protocols, using domain-specific axioms [START_REF] Durgin | A compositional logic for proving security properties of protocols[END_REF][START_REF] Datta | Protocol composition logic (PCL)[END_REF].

CertiCrypt [START_REF] Barthe | Formal certification of ElGamal encryption[END_REF] and EasyCrypt [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF] provide a framework and a tool to derive COQ proofs for cryptographic constructions. Cryp-toVerif [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF] can verify the security of protocols under asymptotic assumptions, both expressed in a domain-specific pi calculus. It searches for a sequence of games, until it reaches a 'final game' such that the target security properties can be checked. Bhargavan et al. [START_REF] Bhargavan | Cryptographically verified implementations for TLS[END_REF] build a model extractor from ML to CryptoVerif, and apply it to verify the cryptographic core of their TLS implementation. Their tools rely on global program transformations that do not scale well to large programs. Our approach is scalable and modular, but does require type annotations.

Our work can be seen as a typed variant of simulation-based security [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF][START_REF] Backes | The reactive simulatability (RSIM) framework for asynchronous systems[END_REF][START_REF] Küsters | Simulation-based security with inexhaustible interactive Turing machines[END_REF]. Using types to express constraints on environments, we achieve fine-grained modularity, giving for example an ideal functionality for CPA encryption.

Backes et al. [START_REF] Backes | Computational sound verification of source code[END_REF] establish the asymptotic soundness of symbolic trace properties in RCF, the core calculus of F7, by translation to CoSP [START_REF] Backes | CoSP: A general framework for computational soundness proofs[END_REF]. They do not rely on types; instead, they relate the sealbased symbolic cryptography of Bengtson et al. [START_REF] Bengtson | Refinement types for secure implementations[END_REF] to an algebraic Dolev-Yao model, then apply a general computational-soundness theorem. Our method seems more direct and compositional, and also applies to observational equivalences, such as indistinguishability.

COMPUTATIONAL RCF

We define a variant of RCF, with mutable references and probabilistic sampling, but without non-determinism: we need sampling to model cryptographic algorithms and probabilistic adversaries; we exclude non-determinism because it would yield too much power to computationally bounded adversaries, essentially giving them access to an NP oracle. Instead, as usual with concrete cryptography, we let the adversary schedule the computation. The resulting calculus has the same expressive power and complexity as probabilistic Turing machines, while retaining the high-level programming syntax and tools of ML. We stay as close as possible to the calculus of Bengtson et al. [START_REF] Bengtson | Refinement types for secure implementations[END_REF]. We adapt their type system and use F7, their typechecker, for all our experiments. Core Syntax We give below our syntax for RCF, a formal core of F# with support for sampling and references. This syntax is a simplification of the concrete ML syntax supported by F# and F7; the technical report provides encodings and syntactic sugar showing how to support the ML code presented in the next sections.

= expression M value M N application let x = A in B let (scope of x is B) let (x, y) = M in A pair split (scope of x, y is A) match M with constructor match h x → A else B (scope of x is A) assume φ assumption of formula φ assert φ assertion of formula φ sample fair coin toss ref M reference creation true △ = inl () false △ = inr ()
The syntax includes standard functional constructors, values, and expressions. It also has two expressions for specification purposes: assume and assert both take a formula φ as parameter. Informally, assume φ records φ as a new hypothesis, whereas assert φ records φ as a proof obligation, which should logically follow from the hypotheses recorded so far. Operationally, these expressions do not affect the rest of the computation. The formulas φ range over first-order logic with predicates on F# values; we omit their standard syntax.

Our first addition to RCF is the expression sample, which reduces to either true or false with probability 1 2 . This expression models a perfect source of random bits.

Instead of communications and concurrency, our calculus features references à la ML, via the presence of references creators, readers and writers. We use these imperative references for programming schedulers, communications, and stateful oracles. Formally, references are pairs of functions that read and write on a memory location. Each evaluation of ref allocates a fresh label a, and returns a pair (read a , write a ) for resp. reading and writing at location a. Following the syntax of ML, we write !M and M:=N for reference reading and writing, defined as

get c △ = let (x 1 , x 2 ) = c in x 1 () set c v △ = let (x 1 , x 2 ) = c in x 2 v
Conversely, our calculus does not include primitive comparison on arbitrary values (M = N), present in RCF. This restriction mat-ters for modelling secrecy in §4, where we need to exclude comparisons on values with abstract types. (Comparisons on constructed values such as Booleans, pairs, and bitstrings are still enabled using match, so this restriction does not affect the expressive power of protocols and adversaries that exchange only first-order values.) Probabilistic semantics We define a probabilistic reduction semantics. We write [X, L, A] → p [X ′ , L ′ , B] when expression A reduces in one step to B, from store X to store X ′ , under logical assumptions (i.e. sequence of formulas) L to L ′ , with probability p (0 < p ≤ 1); this relation is defined in the full paper. Stores are finite maps from labels to values and keep track of references creations and assignments in the usual way. We write

[X, L, A] → n p [X ′ , L ′ , B] when [X, L, A] → p 1 • • • → p n [X ′ , L ′ , B] in n steps and p is the prod- uct p 1 • • • p n , and write [X, L, A] → * p [X ′ , L ′ , B] when [X, L, A] → n p [X ′ , L ′ , B]
for some n ≥ 0. Our reduction rules coincide with those of RCF, except for the presence of probability indices, the rules for references and assumption logging:

[X, L, ref M] → 1 [X ⊎ {a → M}, L, (read a , write a )] [X ⊎ {a → M}, L, read a ()] → 1 [X ⊎ {a → M}, L, M] [X ⊎ {a → M}, L, write a N] → 1 [X ⊎ {a → N}, L, ()] [X, L, assume φ ] → 1 [X, L ∪ {φ }, ()]
the sampling rules sample → 1 2 true, sample → 1 2 false and the stuttering rule on values [X, L, M] → 1 [X, L, M] which guarantees that every closed configuration performs a reduction step with total probability 1. For example, let x 0 = sample in . . . let x n-1 = sample in (x 0 , . . ., x n-1 ) reduces in 2n steps to each binary n-word with probability 1 2 n and may model a uniform random bitstring generator. Runtime Safety A close expression A is safe if and only if, in all evaluations of A, all assertions succeed, that is, each time an assert is evaluated, its formula logically follows from the previously assumed formulas. More generally, we define a probabilistic notion of safety. Let P be a predicate over monotonic trace properties. The probability that P(A) holds in n ≥ 0 steps is defined as

q n △ = ∑ A→ p 1 A 1 ...→ pn A n |P (p 1 . . . p n )
where the sum ranges over distinct configurations A 1 , . . . , A n up to relabeling. (A i represent configurations with main expression A i , and an expression A is treated as the configuration with an empty store and an empty log.) The series (q n ) n≥0 is positive, increasing, and bounded by 1, so it has a limit q ∈ [0, 1] = lim n→∞ q n . We let Pr[A ⇓ M] be q when M is a closed value and P is "A n has expression M". We similarly define the probability that A terminates, letting P be "A n 's expression is a value", and that A fails, letting P be "some A i is a failing assert" (i.e. A i = [X i , L i , E[assert φ ]] for some evaluation context E and formula φ that does not follow from L i ). Hence, A is safe if and only if it fails with probability 0. Type Safety We type expressions using dependent types, with the syntax below. The main addition to F# types are refinement types: an expression has type x:T {φ } when its values M (if any) have type T and, moreover, are such that formula φ {M/x} follows from prior assumptions. Dependent functions and dependent pairs bind a value variable x in the formulas within the types of the function result and the second element of the pair, respectively.

The main typing judgment is of the form I ⊢ A : T , stating that expression A has type T in environment I. Following Bhargavan et al. [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF], we do not rely on kinding (formally, we do not have the subtyping rule (Public Tainted)) and we use an auxiliary typing judgment I ⊢ B ❀ I ′ stating that B is a module that is well-typed in environment I and that exports the typed interface I ′ . Formally, if we have I ⊢ B ❀ I ′ and I ′ ⊢ A : T , then also I ⊢ B • A : T where B • A represents the composition of the F# modules B and A. We refer to the full paper for auxiliary definitions and the RCF typing rules.

Syntax of Types

T,U,V ::= type α type variable unit unit type x:T →U dependent function type (scope of x is U) x:T * U dependent pair type (scope of x is U) T +U disjoint sum type µα.T recursive type (scope of α is T ) x:T {φ } refinement type (scope of x is φ ) bool △ = unit + unit ref T △ = (() → T ) * (T → ())
We obtain a safety theorem for probabilistic RCF:

THEOREM 1 (SAFETY). If ∅ ⊢ A : T then A is safe.
Concretely, to establish I ⊢ B ❀ I ′ , the F7 typechecker takes as input a series of interface definition files (with .fs7 suffixes) instead of typed environments I and I ′ plus an F# implementation file (with an .fs suffix) instead of the expression B. After typechecking with F7, all formulas can be erased to yield ordinary F# interfaces and implementations.

Security By Typing We use safety to model the security of protocols and their implementations, as follows. The protocol and its libraries are written as F# modules (say C PR ), using assume and assert to specify their security properties, whereas the adversary is their main programs (say A). The capabilities of the adversary are specified as a typed adversary interface I PR : we let A range over arbitrary programs well-typed against this interface (I PR ⊢ A : T ) that do not use assume and assert.

Since the assume and assert specify what is actually verified by typing, one must carefully review them before interpreting formal safety as a meaningful security property. In this paper, we suppose in particular that, for all runs of our systems, the assumptions recorded in the global log are logically consistent, in the sense that we cannot derive false from them. Bhargavan et al. [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF] rely on a similar logical-consistency hypothesis and provide simple syntactic conditions on assumed formulas to guarantee consistency. In comparison, our code uses only basic assumptions (e.g. to record runtime events) and their consistency is straightforward.

For protocols, we write the adversary interface I PR so that all its functions operate on plain, unrefined types such as concrete bytes. Thus, our condition I PR ⊢ A : T expresses that the adversary can interact with the protocol only by calling these functions, using any concrete bytes that it can compute, and its formal typability does not exclude any such attack. For instance, I PR may export functions to control the network, generate keys, and trigger runs of the protocol with various parameters, but keep some of the protocol keys private. Thus, by quantifying over all probabilistic runs of all resulting systems C PR • A, we account for the potential behavior of C PR when controlled by any active network attackers. To automatically verify the protocol, we let F7 check that it is a well-typed implementation of the interface I PR , that is, ∅ ⊢ C PR ❀ I PR . Then, by composing the two typing hypotheses on C PR and A, we have ∅ ⊢ C PR • A : T , and by Theorem 1, we conclude that C PR • A is safe for all active network attackers.

For cryptographic functionalities, the main focus in this paper, we write more precise typed interfaces, using refinement types to express (and typecheck) obligations that protocol designers need to comply with when using these functionalities. Our typed cryptographic interfaces enable us to treat protocols and adversaries as a single program when reasoning on cryptographic libraries. These interfaces may not directly correspond to a class of untyped adversaries. As illustrated for the RPC protocol at the end of §3, they complement more traditional bytes-only adversary interface: given a system composed of cryptographic libraries and protocol code, one can automatically verify by typing that the system exports this particular adversary interface. (See also the full paper for an extended discussion of adversary typability.)

Computational Complexity We finally define notions of termination and complexity. Asymptotic security is expressed for algorithms, protocols, and adversaries parameterized by a global security parameter η ≥ 0, intuitively the length of the cryptographic materials in use. In this paper, we treat η as a symbolic integer constant in expressions and we often keep its instantiation implicit, writing for instance A instead of (A η ) η≥0 for the series of expressions obtained by instantiating η with 0, 1, . . . .

• A series of probabilities (q η ) η≥0 is negligible when, for any polynomial p, we have lim η→∞ (q η * p(η)) = 0; it is overwhelming when 1q η is negligible. • A closed expression A is asymptotically safe when its series of probabilities of failing is negligible. • Closed expressions A 0 and A 1 are asymptotically indistinguishable, written

A 0 ≈ ε A 1 , when |Pr[A 0 ⇓ M] -Pr[A 1 ⇓ M]
is negligible for all closed values M. • A closed expression A has probabilistic polynomial-time complexity, or is p.p.t. for short, when there exists a polynomial p such that, for all η ≥ 0, A η terminates with probability 1 in at most p(η) steps.

We extend our notions of polynomial-time complexity to typed, modular systems with first-order interfaces, that is, interfaces declaring values of base type and n-ary functions on such values. (In our F# programs, we treat curried functions as n-ary functions.)

(1) A closed first-order functional value is p.p.t. when its runtime is bounded by a polynomial in the size of its parameters.

In For functions on bitstrings, our definitions coincide with those used for Turing machines. Our definition for modules is similar to inexhaustible Turing machines [START_REF] Küsters | Simulation-based security with inexhaustible interactive Turing machines[END_REF] and reactive polynomialtime [START_REF] Hofheinz | Polynomial runtime and composability[END_REF]. We leave as future work a more general treatment of complexity for higher-order modules; see for instance Kapron and Cook [START_REF] Kapron | A new characterization of type 2 feasibility[END_REF] for second-order functions, or Danielsson [START_REF] Danielsson | Lightweight semiformal time complexity analysis for purely functional data structures[END_REF] for typebased verification of complexity.

AUTHENTICITY USING MACS

Message authentication codes (MACs) provide integrity protection based on keyed cryptographic hashes. We consider the properties of an F# module that implements this functionality. We begin with its plain F# programming interface: The interface declares types for keys, texts, and MACs. The type for keys is abstract, whereas those for texts and MACs are just type aliases for 'bytes', the type of concrete byte arrays, used for clarity in other declarations. The interface also declares symbolic constants for the sizes (in bytes) of MACs and keys, and four functions: to generate a fresh key; to produce a MAC given a key and a text; to verify whether a MAC is valid given a key and a text; and to serialize a key into bytes. This function is named LEAK since it will be used to model key compromise. (The full paper also discusses a converse function COERCE to turn bytes into keys.) Concrete implementation (C) We give below a sample implementation of that interface based on the .NET cryptographic libraries, which we use for running our protocols. (For brevity, we often omit repeated declarations in code excerpts, such as type text = bytes; the complete source files are available online.) This F# code sets sizes for keys and MACs, uses concrete random bytes as keys, and just performs system calls to standard algorithms [START_REF] Krawczyk | HMAC: Keyed-hashing for message authentication[END_REF]. As with all practically deployed symmetric primitives, there is no formal security guarantee and the choice of algorithms is expected to evolve over time. Ideal Interface (I) To capture the intended properties of MACs, we rely on another, refined ideal interface for the same module, written I, as follows:

type mac = b:bytes{Length(b) = macsize} predicate val Msg: key * text → bool val GEN: unit → key val MAC: k:key → t:text{Msg(k,t)} → mac val VERIFY: k:key → t:text → m:mac → v:bool{v=true ⇒ Msg(k,t)} val LEAK: k:key{!t. Msg(k,t)} → b:bytes {Length(b) = keysize}
This refined interface is designed for protocol verification and is similar to those used for typing symbolic cryptography [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF]. It declares the type of keys as abstract, thus preventing accidental key leakage in data sent on a public network or passed to MAC.

To support authentication properties, the interface introduces a logical predicate on keys and texts, Msg(k,t), to indicate that t is an authentic message MACed with key k. This predicate occurs in the types of MAC and VERIFY, as a pre-condition for MACing and as a post-condition of successful MAC verification. The interpretation of Msg(k,t) is protocol-dependent: as illustrated at the end of this section, each protocol defines Msg according to the properties it wishes to authenticate using MACs, possibly giving a different interpretations to each key. In order to be safe for any logical definition of Msg, calls to VERIFY may succeed at most for texts previously passed as arguments to MAC with matching keys (until the key is leaked), thereby excluding the possibility of forging a MAC for any other text.

The pre-condition of LEAK accounts for dynamic key compromise: the protocol may call LEAK to access the actual key bytes, while other parts of the protocol still rely on the post-condition of VERIFY. To preserve safety, the precondition !t, Msg(k,t) demands that, before leaking the key, Msg(k,t) holds for all texts. (In F7 syntax, !t is logical universal quantification on t.) The function LEAK can be used to model the potential corruption of principals by leaking their keys to the adversary; see Bhargavan et al. [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF][START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF] and §6 for protocols verified by typing despite partial key compromise. (The function COERCE would have a similar pre-condition, so that any key supplied by the adversary is treated as compromised. Independently, the adversary may include its own copy of the concrete implementation C, and thus use any bytes as keys.)

In contrast with symbolic models, our texts and MACs are just concrete byte arrays. Taking advantage of refinements, the interface also enforces the consistency of sizes for MACs and key bytes. (In F7, Length is a logical library function.) Thus, for instance, typechecking would catch parsing errors leading to a call to VERIFY with a truncated MAC, as its argument would not match the refined type mac.

Intuitively, the ideal interface is too good to be true: a simple information-theoretic argument shows that any implementation such that (1) MACs are shorter than texts and (2) MAC and VERIFY communicate only through MACs must be unsafe. In particular, we do not have ⊢ C ❀ I. Next, we show how we can establish its weaker, asymptotic safety under cryptographic assumptions. Security (CMA) Common assumptions on MACs are functional correctness and security. The correctness assumption, as well as other expected functional properties of our concrete implementation, are expressed using another refined concrete interface that declares

type mac = b:bytes{Length(b) = macsize} predicate val GENerated: key → bool predicate val MACed: key * text * mac → bool val GEN: unit → k:key {GENerated(k)} val MAC: k:key → t:text → m:mac {MACed(k,t,m)} val VERIFY: k:key → t:text → m:mac → v:bool{ GENerated(k) ∧ MACed(k,t,m) ⇒ v = true } val LEAK: k:key → b:bytes{Length(b) = keysize} assume !k,t,m0,m1. GENerated(k) ∧ MACed(k,t,m0) ∧ MACed(k,t,m1) ⇒ m0 = m1
In this interface, written I C in the following, two auxiliary predicates GENerated and MACed keep track of the results returned by GEN and MAC; the final assumption states that MAC is a deterministic function. These properties are easily met by any implementation that just recomputes the MAC for verification, as our concrete implementation does: to typecheck against I C , it suffices to add events at the end of GEN and MAC to record their result.

The security assumption is expressed as a game. We adopt a standard notion, resistance against existential Chosen Message forgery Attacks (CMA), introduced by Goldwasser et al. [START_REF] Goldwasser | A digital signature scheme secure against adaptive chosen-message attack[END_REF] for signatures; we follow the presentation of Bellare et al. [START_REF] Bellare | Keying hash functions for message authentication[END_REF]. In this game, an adversary attempts to forge a valid MAC; to this end, it can adaptively call two oracles for computing and verifying MACs on a single, hidden key; the adversary wins if it can produce a text and a MAC such that verification succeeds but the text has not been passed to the MAC oracle. We set up this game using an F# module, written CMA and defined as follows:

let k = GEN() let log = ref [] let mac t = log := t::!log; MAC k t let verify t m = let v = VERIFY k t m in assert(not v || List.mem t !log); v
This code generates a key, implements the two oracles as functions using that key, and maintains a log of all texts passed as arguments to the mac function. We intend to run this code with an adversary given access to mac and verify, but not k or log. The verification oracle also tests whether any verified pair wins the game: the assert claims that this does not happen: either v is false, or t is in the log. (In the asserted formula, || is logical disjunction.) DEFINITION 1. C is CMA-secure when, for all p.p.t. expressions A with no assume or assert such that mac: text → mac, verify: text → mac → bool ⊢ A: unit, the expression C • CMA • A is asymptotically safe.

We establish asymptotic safety for programs well-typed against the ideal interface of a CMA-secure MAC. THEOREM 2 (ASYMPTOTIC SAFETY FOR MAC). Let C be p.p.t. CMA-secure and such that ⊢ C ❀ I C . Let A be p.p.t. such that I ⊢ A : unit. The expression C • A is asymptotically safe.

As illustrated at the end of this section, Theorem 2 usefully applies to expressions A composed of a fixed protocol and any adversaries typed against its protocol interface.

To prove Theorem 2, our main tool is an intermediate, well-typed functionality, written F and defined below, such that C • F implements the ideal interface I. We call C •F an ideal MAC implementation. Our next theorem states that the concrete and ideal implementations are indistinguishable; it can be used in compositional proofs relying on F. For example, §6 in the full paper uses it to show that encrypt-then-MAC implements authenticated encryption. (In terms of universal composability, C emulates F, with C as a simulator.) THEOREM 3 (IDEAL FUNCTIONALITY FOR MAC). Let C be p.p.t. CMA-secure such that ⊢ C ❀ I C . Let A be p.p.t. such that

I ⊢ A. We have C • A ≈ ε C • F• A.
Ideal Functionality (F) Our ideal functionality re-defines the type for keys, now represented as integer indexes, and re-defines the functions GEN, MAC, VERIFY, and LEAK using those provided by any implementation of the refined concrete interface I C . It maintains a global, private association table ks that maps each key index to some internal state, consisting of a concrete MAC key (kv), a list of previously-MACed texts (log), and a Boolean flag (leaked) indicating whether the key has been leaked or not. In the code below, qualified names such as Mac.GEN refer to entries from the concrete interface I C , while names such as GEN refer to their re-definition. Our ideal functionality F is: GEN allocates a key with index k (the number of keys allocated so far), generates a concrete key, and records its initial state, with an empty log and a flag set to false. When called with a key, the three other functions first perform a table lookup to retrieve its state (kv,log,leaked). MAC computes the MAC using the concrete key kv and adds the MACed text to the log. VERIFY performs the concrete MAC verification, then it corrects its result from true to false when (i) the concrete verification succeeds; but (ii) the text has not been MACed, as recorded in log; and (iii) the key has not been leaked, as recorded by leaked. LEAK returns the concrete key bytes, and sets the leaked flag to true.

let ks = ref [] ( *
The module C • F obtained by composing the concrete MAC implementation with F is a well-typed implementation of the ideal interface, as F corrects any unsafe verification of C, but it is unrealistic, as F relies on global shared state.

LEMMA 1 (TYPING). I C ⊢ F ❀ I .

This lemma is proved by letting F7 typecheck F. Intuitively, it holds because the result of the verification function is always consistent with the log and the flag, whose refinement types record enough facts Msg(k,t) to establish the post-condition of VERIFY.

We provide a brief outline of the proof for Theorems 3 and Theorem 2, but refer to the full paper for the details. Classically, we rely on an "up to bad" lemma of [START_REF] Bellare | The security of triple encryption and a framework for code-based game-playing proofs[END_REF], stating that C • F and C have exactly the same behaviour until F corrects a verification; when this happens, a related adversary wins against CMA. We use two main reductions, to account for dynamic key leakage, then for the use of multiple keys in F. To complete the proof of Theorem 2, we use Lemma 1 and the typing hypotheses of C and A to conclude from Theorem 1 that C • F • A is perfectly safe.

Sample Protocol: An Authenticated RPC To illustrate the use of our MAC library for verification, we include the code of a sample protocol for remote procedure calls (RPC) adapted from Bhargavan et al. [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF]. In the protocol, a client and a server exchange requests s and responses t coded as strings. To authenticate and correlate these strings, they use MACs computed from a shared key k: We omit the formatting functions, request and response, that compute the bytes actually MACed as tagged concatenations of their arguments. For simplicity we only consider the single key setting. Fournet et al. [START_REF] Fournet | Cryptographic verification of protocol implementations by typechecking[END_REF] show how to verify a variant of the protocol with multiple keys shared between pairs of principals using our MAC functionality; the details are available online. Security is modelled as safety when running with an active adversary that calls the functions client and server (to trigger parallel sessions) and controls the network. To this end, these two functions include matching assume and assert for each message sent and accepted by the protocol, respectively. With this specification, type-safety entails two correspondence properties between these events, of the form "whenever the server accepts a request s, the client must have sent that request before" and similarly for responses. The protocol uses a single key, so its security depends on MACing unambiguous texts (formatted by request and response).

let k = GEN() let client s = assume (Request(s)); send (concat (utf8 s) (MAC k (request s))); recv (fun msg → let (v,m ′ ) = split macsize msg in let t = iutf8 v in if VERIFY k (response s t) m ′ then assert(Response(s,t));()) let server () = recv (fun msg → let (v,m) = split macsize msg in let s = iutf8 v in if VERIFY k (request
Let Net range over modules implementing the network and the scheduler, informally controlled by the adversary, with the following interface for the protocol:

I Net △ = send: bytes → unit, recv: (bytes → unit)→ unit
In addition, Net may export an arbitrary interface I ′ NET for the adversary. Let C RPC be the sample protocol code above, after inlining its other (trusted) library functions, with the following interface for the adversary: (Technically, we state our p.p.t. assumption on Net composed with C RPC because Net has a second-order interface.) For each concrete definition of Net, we obtain a computational safety theorem against adversaries A with access to the network and the protocol, guaranteeing that the two correspondence properties discussed above hold with overwhelming probability.

I RPC △ = client: string → unit
The proof of Theorem 4 roughly consists of letting F7 typecheck I NET , I ⊢ C RPC ❀ I RPC . As a sanity check, we outline a broken (non-typable) variant C • RPC and a sample adversary A that breaks response authentication (with probability 1). Suppose that the formatting functions request and response simply concatenate their arguments-without tagging. Any valid MAC for a request will also be accepted as a valid MAC for the empty response to that request. The adversary A below meets the conditions of Theorem 4, and tries this simple reflection attack by triggering a request, intercepting it, and sending back a fake response with the same MAC:

client "hello"; let msg = recv'() in let (v,mac) = split macsize msg in send' (concat (utf8 "") mac)
where send' and recv' are part of the attacker interface I ′ NET . The expression C • Net •C • RPC • A reduces to a configuration of the form [X, {Request("hello")}, E[assert(Response("hello",""))]], with a failing assertion as the the client accepts the fake response. As can be expected, the protocol C • RPC does not typecheck, since the precondition for calling MAC would have to imply Response(s,"").

Bhargavan et al. [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF] verify similar code by typing against symbolic cryptographic interfaces. Although we now rely on computational assumptions, our protocol code still typechecks essentially for the same reasons. In comparison with their symbolic theorem, ours is also simpler-we do not need to give our adversary access to the cryptographic library, since the adversary may include its own implementation of MAC algorithms.

Experimentally, we also test that our protocol code runs correctly, at least when compiled with a Net library and an adversary that implements a reliable network and a simple test. The rest of the code is available online, including a sample (harmless) adversary that correctly schedules clients and servers for testing, and another adversary that tries the attack described above.

Public-Key Signatures

We have also applied our verification method to public-key signature schemes, under similar assumptions, using RSA as sample implementation. The main differences are that we have distinct types for public and private keys, and that we give the protocol (and the adversary) unconditional access to the bytes of public keys. See the full paper for the resulting ideal functionality.

PERFECT SECRECY BY TYPING

In this section and the next, we focus on a simple notion of perfect secrecy and on indistinguishability, its cryptographic counterpart. We let ≈ represent probabilistic equivalence between closed terminating expressions: two expressions are equivalent when they return values with identical probabilities. Our notion of secrecy concerns values given an abstract type, written α in this section. With encryptions, α will be the type of plaintexts. Intuitively, protocols given values of type α cannot directly operate on them [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF]; we use this parametricity property to establish equivalences between implementations of α. (Roy et al. [START_REF] Roy | Inductive trace properties for computational security[END_REF] similarly restrict protocols, using a notion of secretive traces for protecting nonces.) DEFINITION 2. For a fixed type variable α, let secret types be of the form T α ::= α | T → T α where T ranges over base types. Let secret interfaces be of the form I α = α, x 1 : T α,1 , . . . , x n : T α,n for some n ≥ 0. Let P α range over modules that define let x i = v i for some pure total values v i for i = 1..n, such that ⊢ P α ❀ I α .

THEOREM 5 (SECRECY BY TYPING). Let A such that I α ⊢ A : bool. For all P 0 α and P 1 α , we have

P 0 α • A ≈ P 1 α • A.
The proof relies on a variant of the subject reduction lemma, which we verified in COQ. Experimentally, we use F7 to automatically check the typing condition of Theorem 5.

For example, consider a protocol C that operates on a secret string s (formally a free variable of C) using operations defined in library P (including a definition of s), and an adversary A that tries to gain information on s by interacting with the protocol using interface I C . We are thus interested in systems of the form P •C • A with ⊢ P • C ❀ I C and I C ⊢ A : bool. To prove that P • C does not leak any information on s, it suffices to verify that P defines only pure values, to write a secret interface of the form I α = α, s : α, . . . for P, and to typecheck that ⊢ P ❀ I α and I α ⊢ C ❀ I C . Theorem 5 then applies to C • A and any two variants P 0 α and P 1 α of P that differ only in their definition of s, and thus the probability Pr[P •C • A ⇓ b] does not depend on the value of s.

A Module for Plaintexts In preparation to encryption in §5, we introduce a sample module for plaintexts, written P, with two interfaces: a secret interface I PLAIN with abstract type α=plain; and another, concrete interface I C PLAIN that reveals the representation of plain. We begin with the latter: The constant plainsize and the type repr define a fixed-length, concrete representation of plain values. (We need to bound the length of plaintexts, as otherwise encryption would necessarily leak some information about plaintexts.)

We let I PLAIN be I C PLAIN with the abstract type declaration type plain substituted for the type alias type plain = repr. The interface I PLAIN is secret, and such that ⊢ P ❀ I C PLAIN implies ⊢ P ❀ I PLAIN . (It does not strictly match Definition 2 because of the integer constant plainsize; however Theorem 5 applies after inlining plainsize in P.) In both interfaces, the functions plain and respond stand for any code that operates concretely on secrets, for instance respond may compute responses to secret requests in an RPC protocol; this code may be hoisted to P in order to apply Theorem 5. The function plain (implemented as the identity function) maps representations to plaintexts; it is useful, for instance, to let the adversary provide chosen values for plaintexts. Conversely, a function repr from plaintexts to concrete representations, necessary for instance to marshal plaintexts before their concrete encryption, would break secrecy. As explained in the next section, however, the secret interface I PLAIN still enables ideal encryption.

SECRECY USING ENCRYPTION

We consider the secrecy guarantees provided by encryption, We begin with public-key encryption, then briefly discuss symmetric encryption. As for MACs in §3, we have a basic F# interface and a more precise concrete F7 interface (written I C ENC ) that expresses functional correctness and enforces consistent bytes lengths for encryption. We let C ENC range over p.p.t. implementations of I C ENC . The full paper gives these interfaces and a sample implementation based on RSA-OAEP.

Our ideal interface for public-key encryption (I ENC ), parameterized by the plaintext type of I PLAIN , is as follows: The interface sets sizes for public keys and ciphertexts, and declares three algorithms: GEN generates keys, ENC encrypts using the public key, and DEC decrypts using the secret key. Secret keys skey are abstract and, in contrast with §3, the interface does not support their dynamic compromise, as this would lead to a well-known commitment problem [see e.g. 4]. Public keys pkey are concrete, fixed-length bytes; these keys may be passed to the adversary, who can then encrypt using its own implementation of ENC, or to other parties, who can authenticate them then encrypt their secrets. The refinement PKey(pk) tracks the public keys generated by GEN and prevents the use of untrusted keys. Security of Encryption (CCA2) We use a standard notion of security, named indistinguishability under chosen-ciphertext attacks (CCA2) [START_REF] Rackoff | Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack[END_REF]. We follow the presentation of Bellare and Rogaway [START_REF] Bellare | Introduction to modern cryptography[END_REF], allowing the adversary to perform multiple oracle encryptions. We formalize this notion as a game in F#, using two modules CCA b for b = 0, 1 obtained from the code below by replacing select x 0 x 1 with x 0 and x 1 , respectively.

let pk, sk = GEN () let log = empty_log pk let enc x 0 x 1 = let x = select x 0 x 1 in let v = ENC pk x in log := cons pk (v,x) !log; v let dec v = match assoc pk v !log with | Some(x) → zero | None → DEC sk v
These modules generate a keypair then define oracles for encryption and decryption: the adversary is given access to enc, dec and pk, but not to the private decryption key sk. This is enforced by the interface

P •C ENC •CCA 0 • A ≈ ε P •C ENC •CCA 1 • A.
A first encryption theorem yields secrecy by typing for protocols whose plaintexts can be given a secret interface.

P 0 •C ENC • A ≈ ε P 1 •C ENC • A.
A second, more general theorem states the soundness of a welltyped ideal functionality for encryption F ENC , defined below.

• A ≈ ε P •C ENC • F ENC • A.
In contrast with Theorem 6, Theorem 7 does not require that A be well-typed using secret plaintexts; instead, it says that, irrespective of I C PLAIN 's implementation, the use of encryption does not leak additional information about plaintexts. As illustrated in the rest of the paper, Theorem 7 is convenient for composing cryptographic modules, for instance with plaintexts carrying cryptographic materials such as short term keys. Ideal Functionality (F ENC ) We let F ENC be the module: Our ideal functionality (for abstract plaintexts) calls a concrete public-key encryption module PKEnc (for plaintexts of type repr). It stores all concrete secret keys in a private association table ks indexed by public keys, together with a log of all ciphertext-plaintexts pairs for this key. It implements the type of secret keys as SK of pkey, also used to index the table. The refinement PKey(pk) of I ENC ensures that all table lookups in ks succeed. To ideally encrypt x, F ENC concretely encrypts zero (some constant plainsize bytes), and adds (c, x) to the log of the public key. To ideally decrypt c, F ENC first searches for some (c, x) in the log; otherwise it concretely decrypts c and uses the function plain to turn the resulting repr into an abstract plain. Thus, F ENC treats plaintexts parametrically, and can be typed using the secret interface I PLAIN : we have I PLAIN , I C ENC ⊢ F ENC ❀ I ENC and this enables us to prove Theorem 6 from Theorems 5 and 7. CPA Encryption and Authenticated Encryption We outline variants of our ideal interface for two other notions of security: resistance to chosen plaintext attacks (CPA) and authenticated encryption. We refer to the full paper and the code for the corresponding security definitions and variants of Theorems 6 and 7. We focus on symmetric encryptions, for simplicity and because authenticated encryption does not have a direct public-key analogue. (See also Küsters and Tuengerthal [38] for ideal functionalities for symmetric encryption with support for corruption.)

CPA Secure Encryption is an assumption weaker than CCA2, obtained by removing the decryption oracle, and meant to be used with authenticated ciphertexts.

Accordingly where the predicate Msg plays the same role as in §3. The precondition on DEC has disappeared, and DEC now returns an option: either some authentic plaintext, or None to report decryption error. Sample Construction Hybrid encryption [START_REF] Bellare | Introduction to modern cryptography[END_REF] supports public-key encryption for large plaintexts by encrypting them under a fresh symmetric key itself encrypted under the public key. To illustrate our method, we program hybrid encryption given a pair of publickey and symmetric-key encryptions and we show that, if both these encryptions are CPA, then hybrid encryption is also CPA. Our code defines:

let ENC pk t = let k = SEnc.GEN() in concat (PKEnc.ENC pk k) (SEnc.ENC k t) let DEC sk c = let c0,c1 = split SEnc.ciphersize c in SEnc.DEC(PKEnc.DEC sk c0) c1
The code (C Hyb ) uses two encryption modules named SEnc and PKEnc (written C SENC and C ENC below), each parameterized by its own plaintext module (P and P k ): large, fixed-sized bytes for symmetric encryption and the resulting hybrid encryption, and symmetric keys for public-key encryption. Using F7, we verify that C Hyb implements an interface (I cpa,hyb ENC , listed below) that includes a public key ideal interface for CPA and defines its ENCrypted predicate as a logical specification of hybrid encryption: We outline a proof of our two encryption theorems for hybrid encryption. To prove the ideal-functionality theorem, we apply ideal-functionality theorems first to public-key encryption, then to symmetric-key encryption. Let P and A be the plaintext module and main expression (as in Theorem 7). Let P k define symmetric keys as public-key encryptions plaintexts. Starting with our concrete implementation

C △ = C SENC • P k •C ENC •C Hyb , we have P •C • A ≈ ε P •C SENC • P k •C ENC • F ENC •C Hyb • A ≈ ε P •C SENC • F SENC • P k •C ENC • F ENC •C Hyb • A.
To apply the ideal public-key and symmetric-key theorems, we let F7 verify their two typing hypotheses:

I C,ENC PLAIN , I ENC ⊢ P •C SENC •C Hyb ❀ I cpa,hyb ENC I C,SENC PLAIN , I SENC ⊢ P k •C ENC • F ENC •C Hyb ❀ I cpa,hyb
ENC . and we conclude with ideal functionality

F △ = C SENC • F SENC • P k • C ENC • F ENC •C Hyb .
To prove the asymptotic secrecy theorem (with hypotheses similar to those of Theorem 6), we use our new idealfunctionality theorem twice and Theorem 5:

P 0 •C • A ≈ ε P 0 • F • A Thm 5 ≈ ε P 1 • F • A ≈ ε P 1 •C • A
To apply Theorem 5, we let F7 verify I PLAIN ⊢ F ❀ I cpa,hyb ENC . The full paper also describes a broken, non-typable variant of hybrid encryption that "forgets" to encrypt its symmetric keys, a sample protocol that encrypts a secret, and a sample passive adversary that breaks asymptotic secrecy using its own concrete implementation of the decryption algorithm.

APPLICATIONS

We show how to compose the typed interfaces and functionalities given in §3 and §5 to verify larger programs.

Multiple Instances of Cryptographic Libraries Formally, a single protocol can use several copies of the same functionality, with distinct copies of their ideal interface and distinct abstract types to protect their keys. Asymptotic security then follows from repeatedly applying our authenticity and secrecy theorems. This enables us, for instance, to verify protocols that use both MACs and signatures, or protocols that encrypt values with different concrete types. The full paper illustrates this approach, showing for instance how to encrypt the keys of another functionality, and how to verify variants of our RPC protocol with authenticated encryption.

Sample Construction: Encrypt-then-MAC We realize authenticated encryption [START_REF] Bellare | Authenticated encryption: Relations among notions and analysis of the generic composition paradigm[END_REF] We also use F7 to verify that F implements the ideal authenticated encryption interface of §5, that is, I PLAIN ⊢ F ❀ I ae SENC . Sample Implementation: Secure Multiparty Sessions We outline the application of our method to larger existing protocols, and consider the cryptographic implementations of secure multiparty sessions of Bhargavan et al. [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF], excluding their fixed key distribution sub-protocol.

Multiparty sessions are global, structured communication protocols. Sessions are specified using a declarative language that indicates who can send which messages, when, and what those messages can contain. From this high-level specification, one can infer generalized correspondence properties, named session integrity, that account for parallel runs of sessions and the compromise of some of their principals, and then generate custom cryptographic protocols that realize all these properties. To this end, Bhargavan et al. developed a verifying protocol compiler that generates both the protocol code (in F#) and detailed type annotations (in F7) embedding the multiparty session logic and the refinements for each of the MAC keys of the protocol-essentially a large definition of the predicate Msg presented in §3. The compiled code is independently verified by F7. Some of their sample protocols involve up to six roles and hundreds of different cryptographic messages formats, handled by more than 5 000 lines of ML protocol code and 4 000 lines of F7 declarations.

Nonetheless, the refined interface for MACs used for typechecking their protocols is almost identical to the ideal interface I MAC of §3, thanks to its support for dynamic key generation and key compromise. Thus, we directly benefit from their symbolic verification effort: for each protocol implementation that they generate and typecheck against their cryptographic library interfaces, Theorem 2 applies and, assuming that their MAC algorithm is CMA-secure, the generated protocol is also asymptotically safe, and their notion of session integrity holds with overwhelming probability.

CONCLUSIONS AND FUTURE WORK

We have shown how to express and verify the computational security of sample cryptographic functionalities (once and for all) using ideal refinement-typed interfaces.

(1) The cryptographic proofs of these functionalities are independent and relatively simple; they mostly rely on programming and typechecking.

(2) The security proofs for protocols using these cryptographic functionalities entirely rely on automated typechecking, much as in prior work on symbolic verification.

(3) Their verified security properties are directly expressed as (asymptotic variants of) safety and perfect secrecy on the protocol code.

This yields an effective, modular method for specifying and verifying protocol code under standard assumptions. Although we conducted our experiments using F# and F7, we would like to carry over our approach to protocols coded in lowerlevel languages such as C and C++. Refinement types are a convenient way to implement point (2) above, but any general-purpose static verification tool that can prove that a program conforms with our ideal interfaces will do.

  type key type text = bytes type mac = bytes val macsize: int val keysize: int val GEN: unit → key val MAC: key → text → mac val VERIFY: key → text → mac → bool val LEAK: key → bytes

open

  System.Security.Cryptography let keysize = 16 ( * 128 bits * ) let macsize = 20 ( * 160 bits * ) type key = bytes let GEN () = randomBytes keysize let MAC k (t:text) = (new HMACSHA1(k)).ComputeHash t let VERIFY k t sv = (MAC k t = sv) let LEAK (k:key) = k

  val plainsize: int type repr = b:bytes {Length(b) = plainsize} type plain = repr val plain: repr → plain val respond: plain → plain

  predicate val PKey: bytes → bool type pkey = pk:bytes{Length(pk)=pksize ∧ PKey(pk)} type cipher = b:bytes {Length(b)=ciphersize} type skey val GEN: unit → pkey * skey val ENC: pkey → plain → cipher val DEC: skey → cipher → plain

=

  pk: pkey, enc: plain → cipher, dec: cipher → plain using the types of I C PLAIN and I C ENC . The oracle-encryption function enc, also known as a left-or-right oracle, encrypts either x 0 or x 1 , depending on b; it also logs the pair (v, x) where v is the resulting ciphertext. The oracle-decryption function dec first checks whether its argument v is the result of an oracle encryption, and then returns a constant (zero), otherwise it performs the decryption. In the end, the adversary wins if it can guess b.DEFINITION 3. C ENC is CCA2 secure when, for all p.p.t. modules P with ⊢ P ❀ I C PLAIN and A with I C PLAIN , I cca ⊢ A : bool, we have

  let ks = ref [] ( * state for all keypairs generated so far * ) let zero = zeroCreate plainsize let GEN () = let pk, sk = PKEnc.GEN () ks := (pk,(sk, empty_log pk))::!ks; (pk,SK(pk)) let ENC pk x = let (sk,log) = assoc pk !ks in let c = PKEnc.ENC pk zero in log := cons pk (c,x) !log; c let DEC (SK(pk)) c = let (sk,log) = assoc pk !ks in match assocc pk c !log with | Some(x) → x | None → plain (PKEnc.DEC sk c)

  definition !pk,p,c. ENCrypted(pk,p,c) ⇔ ∃c0,c1,k. (c = c0|c1 ∧ Length(k)=SEnc.keysize ∧ PKEnc.ENCrypted(pk,k,c0) ∧ Length(c0)=PKEnc.ciphersize ∧ SEnc.ENCrypted(k,p,c1) ∧ Length(c1)=SEnc.ciphersize) val GEN: unit → pk:pkey * sk:skey {pk=PK(sk)} val ENC: pk:pkey → p:plain → c:cipher {ENCrypted(pk,p,c)} val DEC: sk:skey → c:cipher {∃p. ENCrypted(PK(sk),p,c)} → p:plain{ENCrypted(PK(sk),p,c)}

  using Encrypt-then-MAC. Given a CMAsecure MAC C MAC and a CPA-secure encryption C SENC , we build a module C EtM such thatC △ = C SENC •C MAC •C EtM implements authenticated encryption, with ideal functionality F △ = C SENC •F cpa SENC • C MAC • F MAC • C EtM .Using the theorems of §3 and §5, we show that, for any plaintext module P such that ⊢ P ❀ I C PLAIN and every p.p.t. A such that I C PLAIN , I ae SENC ⊢ A, we have P •C • A ≈ ε P • F • A.

  , server: unit → unit We arrive at the following computational safety theorem: THEOREM 4 (RPC SAFETY). Let C be a CMA-secure p.p.t. module with ⊢ C ❀ I C . Let Net be a module with ⊢ Net ❀ I NET , ⊢ Net ❀ I ′ NET , and Net •C RPC is p.p.t. Let A be a p.p.t. expression with I ′ NET , I RPC ⊢ A : unit. The expression C • Net •C RPC • A is asymptotically safe.

  THEOREM 6 (ASYMPTOTIC SECRECY). Let C ENC be a p.p.t. CCA2-secure module with I C PLAIN ⊢ C ENC ❀ I C ENC . Let A be a p.p.t. expression with I PLAIN , I ENC ⊢ A : bool. For any two pure p.p.t. implementations P b of I PLAIN , we have

  THEOREM 7 (IDEAL FUNCTIONALITY). Let C ENC be a p.p.t. CCA2-secure module with I C PLAIN ⊢ C ENC ❀ I C ENC , P a p.p.t. module with ⊢ P ❀ I C PLAIN , and A a p.p.t. expression with I C PLAIN , I ENC ⊢ A. We have P •C ENC

  ENCrypted(k,p,c)} → p:plainwhere the predicate ENCrypted(k,p,c) in the refinements ensures that a well-typed program never attempts to decrypt a ciphertext not produced by ENC. The interface also includes a logical assumption, stating that a ciphertext is the correct encryption of at most one plaintext for a given key.Authenticated Encryption is a stronger notion that provides both secrecy and authenticity. Accordingly, our ideal interface I ae

	declares	SENC
	predicate val Msg: key * plain → bool
	val ENC: k:key → p:plain {Msg(k,p)}→ c:cipher
	val DEC: k:key → c:cipher → (p:plain {Msg(k,p)}) option

, our ideal CPA interface I cpa SENC declares predicate val ENCrypted: key * plain * cipher → bool val ENC: k:key → p:plain → c:cipher {ENCrypted(k,p,c)} val DEC: k:key → c:cipher {∃p.

Acknowledgments Many thanks to Martín Abadi, Aslan Askarov, Karthik Bhargavan, Avik Chaudhuri, Andy Gordon, Gurvan le Guernic, James Margetson, Tamara Rezk, Nikhil Swamy, Dimitrios Vytiniotis and the anonymous reviewers for their help.


Laurent Sagart

teaching and research institutions in France or abroad, or from public or private research centers.


Gohar M Kyureghyan
email: gohar.kyureghyan@ovgu.de

Ferruh Özbudak
email: ozbudak@metu.edu.tr

Planar products of linearized polynomials

Keywords: planar mapping, quadratic mapping, Dembowski-Ostrom polynomial, linearized polynomial, directions defined by linear functions

Let L1(x) and L2(x) be linearized polynomials over Fqn . We determine conditions when the product L1(x) • L2(x) is a planar mapping on Fqn . For a linearized polynomial L over Fqn , let M(L) = {α ∈ Fqn : L(x) + α • x is bijective on Fqn }. We show that the planarity of the product L1(x) • L2(x) is linked with the set M(L) of a suitable linearized polynomial L. We use this relation to describe some families of such planar mappings and we give some nonexistence results.

Introduction

Let p be an odd prime number and q a power of p. Given a mapping f : F q n → F q n and a nonzero element a ∈ F q n , we call D f,a : F q n → F q n , x → f (x + a) -f (x) -f (a) the difference mapping of f defined by a. A mapping f : F q n → F q n is called planar (or perfect nonlinear) if all its difference mappings are bijective. Planar mappings were introduced in [START_REF] Dembowski | Planes of order n with collineation groups of order n 2[END_REF] as a tool to construct projective spaces. In Cryptology planar mappings are called perfectly nonlinear, and they provide the optimal resistance to differential attacks [START_REF] Nyberg | Differentially uniform mappings for cryptography[END_REF]. In [START_REF] Ding | Signal sets from functions with optimum nonlinearity[END_REF], [START_REF] Ding | A family of optimal constant-composition codes[END_REF], planar mappings are used to construct optimal constant-composition codes and signal sets. Planar mappings do not exist in finite fields of even characteristic. A mapping f : F 2 n → F 2 n is called almost perfect nonlinear (APN) if every difference mapping of it has an image set of the maximal possible cardinality 2 n-1 .

The q-weight of a nonnegative integer m is the sum of the digits in its q-adic representation, i.e. if m = i b i q i then the q-ary weight of m is i b i ∈ Z. Recall, that any mapping of F q n can be represented by a polynomial over F q n of degree less than q n . Moreover, different such polynomials define different mappings. This allows us to identify the set of mappings of F q n with the set of polynomials over F q n with degree less than q n . We use the notation F (X) to denote a polynomial, while F (x) is used for the mapping induced by F (X). The algebraic q-degree of a polynomial over F q n is the maximal q-weight of the exponents in its terms. We use briefly the term algebraic degree, since q is fixed all over the paper.

The F q -linear mappings L : F q n → F q n are represented by the polynomials of algebraic degree 1 with the zero constant term, that is

L(x) = n-1 i=0 c i x q i , c i ∈ F q n .
Such polynomials are called linearized or q-polynomials. The affine mappings are given by the polynomials of algebraic degree 1.

Two mappings F, G :

F q n → F q n are called extended affine equivalent (EA- equivalent), if G = A 1 • F • A 2 + A
for some affine permutations A 1 , A 2 and an affine mapping A. EA-equivalent non-constant mappings have the same algebraic degree. It is easy to see that EA-equivalence preserves the planarity of mappings.

A mapping is called quadratic if it is represented by a polynomial of algebraic degree 2. The polynomials of algebraic degree 2 with no terms of algebraic degree 1, n-1 i,j=0 a i,j x q i +q j , a i,j ∈ F q n , are called Dembowski-Ostrom polynomials in [START_REF] Coulter | Planar functions and planes of Lenz-Barlotti class II[END_REF]. Observe that any quadratic mapping is EA-equivalent to a one represented by a Dembowski-Ostrom polynomial. Dembowski-Ostrom planar polynomials describe finite commutative semifields and vice-versa [START_REF] Dembowski | Planes of order n with collineation groups of order n 2[END_REF][START_REF] Coulter | Commutative presemifields and semifields[END_REF].

In this paper we continue the study of products of linearized polynomials. To our knowledge such polynomials were first considered in [START_REF] Blokhuis | Permutations amongst the Dembowski-Ostrom polynomials[END_REF]. In [START_REF] Blokhuis | Permutations amongst the Dembowski-Ostrom polynomials[END_REF][START_REF] Laigle-Chapuy | A note on a class of quadratic permutations over F2n[END_REF] bijectivness of these polynomials is studied. APN products of linearized polynomials are considered in [START_REF] Th | On almost perfect nonlinear functions over F n 2[END_REF], where it is shown that if X • L(X) is APN with a linearized polynomial L(X) then L(X) must be a monomial. In this paper we investigate the planar products of linearized polynomials. In particular we observe that to contrary to the APN case there are planar polynomials X • L(X) with a nonmonomial linearized polynomial L(X). [START_REF] Kyureghyan | Some Theorems on Planar Mappings[END_REF][START_REF] Weng | Pseudo-Paley graphs and skew Hadamard sets from presemifields[END_REF] it is shown that the only zero of a planar Dembowski-Ostrom polynomial is X = 0, which yields the statement.

Planar products of linearized polynomials

Proposition 1. Let L 1 , L 2 ∈ F q n [X] be linearized polynomials. If the mapping L 1 • L 2 : F q n → F q n is planar, then necessarily the mappings L 1 and L 2 are bijective on F q n . Proof. Observe that L 1 (X) • L 2 (X) is a Dembowski-Ostrom polynomial. In

⊓ ⊔

The next proposition shows that the study of planar polynomials of shape L 1 (X) • L 2 (X) can be reduced to the one of shape X • L(X).

Proposition 2. Let L 1 , L 2 : F q n → F q n be F q -linear. Then L 1 (x) • L 2 (x) is planar on F q n if and only if x • L 1 (L -1 2 (x)) is planar on F q n , where L -1 2 (x) is the inverse mapping of L 2 . Proof. The mappings L 1 (x) • L 2 (x) is EA-equivalent to x • L 1 (L -1 2 (x)), since (L 1 (x) • L 2 (x)) • L -1 2 (x) = L 1 (L -1 2 (x)) • L 2 (L -1 2 (x)) = L 1 (L -1 2 (x)) • x. ⊓ ⊔
For any linearized polynomial L(X) over F q n we define the polynomial Q L by

Q L (X) := L(X) X . Lemma 1. Let L(X) ∈ F q n [
X] be a linearized permutation polynomial. The mapping x • L(x) is planar on F q n if and only if, for any non-zero β ∈ F q n , at most one of β or -β belongs to the set {Q L (x) :

x ∈ F * q n }. Proof. Consider D a (x) = (x + a)L(x + a) -xL(x) -aL(a) = aL(x) + xL(a).
Since D a (x) is a linear mapping, it is bijective if and only if it has a trivial kernel. It remains to note that the condition aL(x) + xL(a) = 0 if and only if

x = 0 is equivalent to L(x) x = - L(a) a for any non-zero a, x ∈ F q n . ⊓ ⊔
Further we show that the planarity of X • L(X) is linked with the set

M(L) = {α ∈ F q n : L(x) + α • x is bijective on F q n }.
Theorem 1. Let L(X) ∈ F q n [X] be linearized. The mapping x • L(x) is planar on F q n if and only if 0 ∈ M(L) and at least one of β or -β belongs to the set M(L) for any non-zero β ∈ F q n . Proof. The condition 0 ∈ M(L) states that L(x) is bijective on F q n . Using Lemma 1, for any non-zero β ∈ F q n it must hold that either β or -β is not contained in {Q L (x) : x ∈ F * q n }. The proof now follows from the observation that β ∈ {Q L (x) :

x ∈ F * q n } if and only if L(x) -β • x is bijective on F q n . ⊓ ⊔
Note that the monomial planar mappings x 2 and x q i +1 on F q n with n/ gcd(n, i) odd are covered by Theorem 1. The conditions of Theorem 1 are trivially fulfilled for x 2 . In the case x • x q i it is easy to see, that there is no β such that both x q i + βx and x q i -βx are not bijective on F q n if and only if -1 is not a (q i -1)th power in F q n , or equivalently n/ gcd(n, i) odd.

In [START_REF] Th | On almost perfect nonlinear functions over F n 2[END_REF] it is shown that if X • L(X) is APN with a linearized polynomial L(X) then L(X) must be a monomial. Does a similar result hold for planar products X • L(X)? The answer is negative as the following observation shows. Proposition 3. Let 1 ≤ k ≤ n -1 with n/ gcd(n, k) odd and let u ∈ F q n be not a (q k -1)st power in F q n . Then the mapping F (x) = x • (x q n-k -ux q k ) is planar on F q n . Proof. We show that F (x) is EA-equivalent to the planar monomial x q k +1 . Indeed,

F (x) = x q n-k +1 -u x q k +1 = (x q n-k -u x) • x q k +1 ,
and the assumtions on k and u ensure that x q n-k -u x is bijective and x q k +1 is planar.

Our next goal is to describe further families of planar products X • L(X) using Theorem 1. To our knowledge the only linearized polynomials L for which the sets M(L) are known are X, X q k -uX, T r(X) = X + X q + . . . + X q n-1 or some natural transformations of these polynomials.

Open Problem. Find new families of linearized permutation polynomials L with |{β, -β} ∩ M(L)| ≥ 1 for any β ∈ F q n . The next result was proved in [START_REF] Helleseth | On a family of perfect nonlinear binomials[END_REF][START_REF] Hou | On certain diagonal equations over finite fields[END_REF] by different approaches. In [START_REF] Helleseth | On a family of perfect nonlinear binomials[END_REF] it is shown that the mappings of Theorem 2 can be obtained from the mapping x → x 2 via EA-equivalence. We show that this result can be proved by using Theorem 1 as well.

Theorem 2. Let u ∈ F q 2 . The mapping F (x) = x 2 + ux q+1 is planar on F q 2 if and only if 1 -u q+1 is a square in the subfield F q .
Proof. The statement is true for u = 0, so let u = 0. By Proposition 1 if F (x) is planar then x + ux q is bijective on F q 2 , which is equivalent to u q+1 = 1. Further we apply Theorem 1 with L(x) = x + ux q . Let β ∈ F q 2 be such that both L(x) + βx = ux q + (1 + β)x and L(x) -βx = ux q + (1 -β)x are not bijective on F q 2 . This is the case if and only if the elements -(1 + β)/u and -(1 -β)/u are (q -1)st powers in F q 2 , or equivalently if it holds:

β + 1 u q+1 = β -1 u q+1 = 1.
In particular, it must hold (β + 1) q+1 = (β -1) q+1 , which implies

β q = -β. Hence, β + 1 u q+1 = -β 2 -β + β + 1 u q+1 = 1, which yields β 2 = -u q+1 + 1.
Note that 1 -u q+1 is an element in the subfield F q . Moreover β ∈ F q , since β = -β q . Hence, F (x) is planar on F q 2 only if 1 -u q+1 is a square in F q . Finally, we show that this condition is necessary as well. Indeed, let 1 -u q+1 = 0 be a non-square in F q . Suppose, β ∈ F q 2 \ F q satisfies β 2 = -u q+1 + 1. Then necessarily β q = -β, since β and -β are the zeros of the irreducible polynomial X 2 -(1-u q+1 ) in F q 2 and therefor -β is the conjugate of β over F q . To complete the proof it remains to note that for this β it holds

β + 1 u q+1 = β -1 u q+1 = 1.

⊓ ⊔

In the remaining part of the paper we consider the case L(X) = T r(X), where T r(X) is the polynomial describing the trace mapping from F q n onto F q .

Proposition 4. [START_REF] Blokhuis | The number of directions determined by a function f on a finite field[END_REF][START_REF] Kyureghyan | Constructing permutations of finite fields via linear translators[END_REF] For the trace mapping T r from

F q n onto F q it holds M(T r) = {γ ∈ F * q n : T r(γ -1 ) = -1}. Theorem 3. Let a ∈ F * q n with T r (2a) -1 = -1. Then F (X) = X • (T r(X) + aX) is planar on F q n if
and only if there is no z ∈ F q n such that T r(z -1 ) = -1 and T r((z -2a) -1 ) = 1.

Proof. By Proposition 4 it holds

M := M(T r(x) + ax) = {α ∈ F q n : α = -a and T r((a + α) -1 ) = -1}.
By Theorem 1, F (x) is planar if and only if at least one of β or -β belongs to M for any non-zero β ∈ F q n . First we consider the case that β ∈ {-a, a}. Note that a ∈ M as a = -a and T r (2a) -1 = -1. Hence if β ∈ {-a, a}, then either β or -β is contained in M. It remains to show that if β ∈ F q n \ {0, -a, a}, then either β or -β is contained in M. Assume the contrary and hence we have β ∈ F q n \ {0, -a, a} with T r (a + β) -1 = -1 and T r (a -β) -1 = -1. Putting z = a + β we obtain z ∈ F q n with a -β = -(z -2a), T r z -1 = -1 and T r (z -2a) -1 = -T r (a -β) -1 = 1. Using the condition in the statement we complete the proof.

⊓ ⊔ Remark 1. If a = 0 in Theorem 3, then F (x) = x•(T r(x)) is not planar by Proposition 1, since T r(x) is not bijective. Further let a ∈ F * q n with T r (2a) -1 = -1. Then a ∈ M(T r(x) + ax) and -a ∈ M(T r(x) + ax). Hence also for such an a the mapping F (x) = x • (T r(x) + ax) is not planar (see Theorem 1).

Corollaries 1 and 2 show, that the conditions of Theorem 3 are satisfied for n = 3 and a = -1, -2.

Corollary 1. The mapping F (x) = x q 2 +1 +x q+1 is planar on F q 3 . Equivalently, there is no z ∈ F q 3 satisfying T r 1 z = -1 and T r 1 z+2 = 1.

Proof. The statement follows from Proposition 3 and Theorem 3 ⊓ ⊔ Corollary 2. The mapping G(x) = x q 2 +1 + x q+1 -x 2 is planar on F q 3 . Proof. Note that G(x) = x(T r(x) -2x) and hence we can use Theorem 3 with a = -2. Suppose there is z ∈ F q 3 with T r

1 z = -1 and T r 1 z + 4 = 1. (1)
Observe that then z ∈ F q . Indeed, for z ∈ F q condition (1)

T r

1 z = 3 z = -1 and T r 1 z + 4 = 3 z + 4 = 1.
reduces to z = -3 and z = -1, which cannot be satisfied. Let z ∈ F q 3 \ F q which satisfies (1). As in the proof of Corollary 1 already shown the minimal polynomial of z over F q is of the following shape

M z (X) = X 3 + a 2 X 2 + bX + b.
The minimal polynomial of z + 4 is M z+4 (X) = M z (X -4), and hence

M z+4 (X) = (X -4) 3 + a 2 (X -4) 2 + b(X -4) + b = X 3 + (a 2 -12)X 2 + (48 -8a 2 + b)X -64 + 16a 2 -3b.
To ensure T r((z + 4) -1 ) = 1 it must hold 48 -8a 2 + b = 64 -16a 2 + 3b, and hence b = 4a 2 -8. Substituting this value of b in M z (X), we get M z (X) = X 3 + a 2 X 2 + (4a 2 -8)X + 4a 2 -8, a contradiction, since X = -2 is a zero of the latter polynomial. ⊓ ⊔ Remark 2. Observe that the planar mappings described in Corollaries 1 and 2 are EA-equivalent to the monomial planar mapping x q+1 . Indeed, for F (x) this follows from the proof of Proposition 3, and in the case of G(x) from the following equality x q 2 + x q -x q+1 = -x q 2 + x q + x • G(x).

In the following theorem we show that if n is sufficiently large, then there is no a ∈ F q n such that F (X) = X • (T r(X) + aX) is planar on F q n . This is a result obtained using Theorem 3 and Remark 1, which is in the oppositive direction of the existence results given above.

Theorem 4. Let a ∈ F q n and F (X) = X • (T r(X) + aX). If one the following conditions hold, then F (X) is not planar on F q n : -q ≥ 23 and n ≥ 12, -q ∈ {11, 13, 17, 19} and n ≥ 13,

Acknowledgments

The authors thank anonymous reviewers for their useful comments. A part of this paper was written while the second named author was visiting Department of Mathematics, Otto-von-Guericke University of Magdeburg with a research fellowship from Alexander von Humboldt Foundation. He thanks Ottovon-Guericke University of Magdeburg for hospitality. The second named author is partially supported T ÜB İTAK under Grant No. TBAG-109T672.

q = 9 and n ≥ 14, -q = 7 and n ≥ 15.

q = 5 and n ≥ 16.

q = 3 and n ≥ 19.

Proof. Using Remark 1, we can assume that a = 0. Let f 1 (z) and f 2 (z) be the rational functions in F q n (z) given by

We use Theorem 1.1 from [START_REF] Cohen | Finite field elements with specified order and traces[END_REF]. Let p be the characteristic of F q n . Recall that the set {f 1 (z), f 2 (z)} is strongly linearly independent over F q (cf. [START_REF] Cohen | Finite field elements with specified order and traces[END_REF]) if there is no a 1 , a 2 , ǫ ∈ F q n and h(z) ∈ F q n (z) such that (a 1 , a 2 ) = (0, 0) and

We use some simple facts from the theory of algebraic function fields (cf. [START_REF] Stichtenoth | Algebraic Function Fields and Codes[END_REF] or [START_REF] Niederreiter | Rational Points on Curves over Finite Fields: Theory and Applications[END_REF]). Let P 1 be the place of F q n (z) corresponding to the zero of z and let ν P1 denote the normalized discrete valuation corresponding to P 1 . Assume that a 1 = 0. Then

Hence ν P1 (h(z)) < 0, indeed otherwise, using the triangle inequality of valuations (cf. [17, Definition 1.1.9]) we get

which is a contradiction to (2). As ν P1 (h(z)) < 0, we have ν P1 (ǫ) > ν P1 (h(z)) > ν P1 (h(z) p ). Then using the strict triangle inequality of valuations (cf. [START_REF] Stichtenoth | Algebraic Function Fields and Codes[END_REF]Lemma 1.1.11]) we obtain that ν P1 (h(z) p -h(z) + ǫ) = pν P1 (h(z)) = pℓ, where ℓ = ν P1 (h(z)) is a negative integer. This is again a contradiction to (2). Therefore we get that a 1 = 0. Similarly we show that a 2 = 0. This proves that the set {f 1 (z), f 2 (z)} is strongly linearly independent over F q . Under the notation of [4, Theorem 1.1] we have r = 2, deg f

Then there exists a primitive element γ ∈ F q n such that T r(γ -1 ) = -1 and T r((γ -2a)

where log q is the logarithm with respect to base q. It is easy to check the ( 3) is satisfied if one of the conditions in the statement of the theorem holds. For example if q ≥ 23, then 4(2 + log q (9.8 • 2)) ≤ 4(2 + log 23 (9.8 • 2)) = 11.7959 . . . . This completes the proof. ⊓ ⊔