K Amrit

P.-A Fouque

T Genet

M Tibouchi

Proofs as Cryptography: a new interpretation of the Curry-Howard isomorphism for software certificates

The objective of the study is to provide a way to delegate a proof of a property to a possibly untrusted agent and have a small certificate guaranteeing that the proof has been done by this (untrusted) agent. The key principle is to see a property as an encryption key and its proof as the related decryption key. The protocol then only consists of sending a nonce ciphered by the property. If the untrusted agent can prove the property then he has the corresponding proof term (λ-term) and is thus able to decrypt the nonce in clear. By sending it back, he proves that the property has been proven without showing the proof. Expected benefits include small certificates to be exchanged and the zero-knowledge proof schema which allows the proof term to remain secret. External agents can only check whether a proof exists without having any information about it. It can be of interest if the proof contains some critical information about the code structure for instance.

Introduction

The objective of this study is to provide a mechanism by which a host system can determine with certainty that it is safe to execute a program supplied by a source. For this to be possible, the code producer might need to convince the consumer that the source code or the program satisfies certain required properties. These properties can very well be the requirement that the program preserves certain invariants. One way to achieve the goal is to make use of Proof-Carrying Code technique aka PCC [START_REF] Necula | Proof carrying code[END_REF]: the code producer supplies with the code a safety proof that attests to the code's adherence to a previously defined safety policy. The code consumer can then easily and quickly validate the proof. This technique doesn't rely on any cryptographic system.

An alternative way to achieve the goal could be to provide a way to delegate the proof of a property to a possibly untrusted agent and have a small certificate guaranteeing that the proof has been done by the agent. This technique is useful in cases where no predefined safety policy is required and the code producer doesn't have to prove the property on his own and hence speeds up the process at the code producer's end. 5Being in the same setting as the PCC, the code producer and the code consumer could agree on a predefined policy (property) and the code producer after writing the program proves the property but it doesn't send it along with the native source code. Another very important aspect of this mechanism is that it provides a new interpretation of the Curry-Howard isomorphism for software certificates. In both the mechanisms we rely on the analogy between proofs (safety proofs) and types. The analogy carries over to proof validation and type checking.

This technique relies on cryptographic mechanisms and implements a zero-knowledge proof of the fact that the proof in the hand of the prover is a correct proof of the property in question. The property to be proven is seen as an encryption key while the proof-term is the corresponding secret key. Compared to PCC technique which eventually is more of a code consumer friendly mechanism, the one that we have studied is more of a code producer friendly technique as he doesn't need to send the proof which could be of enormous size.

This internship report starts with an introduction to propositional logic and a discussion on Curry-Howard isomorphism and then it makes a detour from Proof Carrying Code technique to our technique as an improved alternative to PCC. As a proof is done in the framework of typed SKI combinatorial calculus which is different from the one considered in the discussion of PCC, a complete section is devoted on its presentation. Last but not least, a considerable amount of time was spent searching the appropriate cryptographic system and hence a treatment of Functional encryption (initially thought to be useful) is left in appendix.

Propositional logic

In mathematical logic, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true propositions. The series of formulas which is constructed within such a system is called a derivation and the last formula of the series is a theorem, whose derivation may be interpreted as a proof of the truth of the proposition represented by the theorem. Truth-functional propositional logic is a propositional logic whose interpretation limits the truth values of its propositions to two, usually true and false. Truth-functional propositional logic and systems isomorphic to it are considered to be zeroth-order logic.

Background

Every logic comprises a (formal) language for making statements about objects and reasoning about properties of these objects. This view of logic is very general and actually we restrict our attention to mathematical objects, programs, and data structures in particular. Statements in logical language are constructed according to a predefined set of formation rules (depending on the language) called syntax rules.

A logical language can be used in different ways. For instance, a language can be used as a deduction system (or a proof system); that is, to construct proofs or refutations. This use of a logical language is called proof theory. In this case, a set of facts called axioms and a set of deduction rules (inference rules) are given, and the object is to determine which facts follow from the axioms and the rules of inference. While using logic as a proof system, one is not concerned with the meaning of the statements that are manipulated, but with the arrangement of these statements, and specially, whether proofs or refutations can be constructed. In this sense, statements in the language are viewed as cold facts and the manipulations involved are purely mechanical, to the point that they could be carried out by a computer. This does not mean that finding a proof for a statement does not require creativity, but that the interpretation of the statements is irrelevant.

However, the statements expressed in a logical language often have an intended meaning. The second use of a formal language is for expressing statements that receive a meaning when they are given what is called an interpretation. In this case, the language of logic is used to formalize properties of structures, and determine when a statement is true of a structure. This use of logical language is called model theory.

One of the interesting aspects of model theory is that it forces us to have a precise and rigorous definition of the concept of truth in a structure. Depending on the interpretation that one has in mind, truth may have quite a different meaning. For instance, whether a statement is true or false may depend on parameters. A statement true under all interpretations of the parameters is said to be valid. A useful (and quite reasonable) mathematical assumption is that the truth of a statement can be obtained from the truth (or falsity) of its parts (sub-statements). From a technical point of view, this means that the truth of a statement is defined by recursion on the syntactical structure of the statement.

The two aspects of logic described above are actually not independent, and it is the interaction between the model theory and proof theory that makes logic an interesting and effective tool. One might say that model theory and proof theory form a couple in which the individuals complement each other. To summarize, a logical language has a certain syntax, and the meaning or semantics of statements expressed in this language is given by an interpretation in a structure. Given a logical language and its semantics, one usually has one or more proof systems for this logical system.

A proof system is acceptable only if every provable formula is indeed valid. In this case, we say that the proof system is sound. Then, one tries to prove that the proof system is complete. A proof system is complete if every valid formula is provable. Depending on the complexity of the semantics of a given logic, it is not always possible to find a complete proof system for that logic. This is the case, for instance, for second-order logic. However, there are complete proof systems for propositional logic and first-order logic. In the first-order case, this only means that a procedure can be found such that, if the input formula is valid, the procedure will halt and produce a proof. But this does not provide a decision procedure for validity. Indeed, as a consequence of a theorem of Church, there is no procedure that will halt for every input formula and decide whether or not a formula is valid.

There are many ways of proving the completeness of a proof system. Oddly, most proofs establishing completeness only show that if a formula A is valid, then there exists a proof of A. However, such arguments do not actually yield a method for constructing a proof of A (in the formal system). Only the existence of a proof is shown.

Propositional logic is the system of logic with the simplest semantics. Yet, many of the concepts and techniques used for studying propositional logic generalize to first-order logic.

Generic Description

In general terms, a calculus is a formal system that consists of a set of syntactic expressions (well-formed formulas), a distinguished subset of these expressions (axioms), plus a set of formal rules that define a specific binary relation, intended to be interpreted as logical equivalence on the space of expressions. A propositional calculus is a formal system L = L(A, Ω, Z, I) where :

-The set of alphabet A is a finite set of elements called propositional symbols or propositional variables. Syntactically speaking, these are the most basic elements of the formal language L otherwise referred to as atomic formulas or terminal elements. -Ω is the set of a finite number of logical connectives. The set Ω is partitioned into disjoint subsets as :

Ω = Ω 0 ∪ Ω 1 . . . ∪ Ω j . . . ∪ Ω n
The set Ω j is the set of all operators of arity j. In the more familiar propositional calculi Ω is typically partitioned as follows:

Ω 0 = {⊥, } Ω 1 = {¬} Ω 2 = {∨, ∧, →}
-The set Z is a finite set of transformation rules that are called inference rules when they acquire logical applications. -The set I is the set of axioms in this language.

A Simplified Axiom System

We consider a propositional calculus L = L(A, Ω, Z, I) where :

-We consider the set A to be large enough that would suffice the needs of our discussion. For example A = {p, q, r, s, t, u, v}. -We take : Ω 1 = {¬} and Ω 2 = {→}.

-The set Z is taken to be singleton, the rule being : if p and p → q are true then we can infer that q is also true. -The set I is the set of axioms in this language and consists precisely of the following ones:

-

(p → (q → p)) -((p → (q → r)) → ((p → q) → (p → r))) -((¬p → ¬q) → (q → p))

Natural Deduction System

We consider a propositional calculus L = L(A, Ω, Z, I) where :

-The set A is supposed to be large enough that would suffice the needs. For example A = {p, q, r, s, t, u, v}.

-We consider : Ω 0 = {⊥, }, Ω 1 = {¬} and Ω 2 = {∨, ∧, →}.

-The set Z is a defined in Figure 1, the transformation rules are intended to be interpreted as the inference rules of so called natural deduction system. -The system presented here has just one axiom that says p → p.

Here we use the sequent notation A 1 , A 2 , . . . , A n B to represent judgements in natural deduction. The standard semantics of a judgement in natural deduction is that it asserts that whenever A 1 , A 2 . . . , A n are all true, B will also be true. We can define two other logical frameworks depending on the presence or absence of certain rules. To be precise we are interested in Minimal and Intuitionistic logic. Defined in [START_REF] Meredith | Seperating minimal, intuitionist and classical logic[END_REF] and developed by Ingebrigt Johansson, minimal logic is a sub-logic of intuitionistic logic which means that set of provable propositions in minimal logic is a proper subset of the corresponding set in intuitionistic logic.

-intro

Γ Γ A Γ B ∧-intro Γ A ∧ B Γ A ∨-intro Γ A ∨ B Γ B ∨-intro Γ A ∨ B Γ A → B Γ A →-elim Γ B Γ A Γ ¬A ¬-elim Γ ⊥
In all the three logics we have two rules corresponding to negation:

-Elimination of negation : If we can prove a proposition A and its negation ¬A, then we have a contradiction noted ⊥. -Introduction of negation : If a proposition A leads to a contradiction then ¬A is valid. The rule can even be formulated as the definition of negation : ¬A := A → ⊥.

The three logics differ on the consequence drawn by a contradiction.

-Classical logic uses reductio ad absurdum and deduces from ¬A → ⊥ that A is valid. This is in fact the elimination rule for double negation because ¬A → ⊥ is the synonym of ¬¬A. -Intuitionistic logic deduces any proposition from a contradiction: ⊥ → B which is the rule ex falso quodlibet aka the principle of explosion. -Minimal logic treats ⊥ as any other proposition and hence has no particular significance.

Examples from Minimal Logic

Example 1:

(¬A ∧ ¬B ↔ ¬(A ∨ B))
We suppose that we have ¬A ∧ ¬B and prove that ¬(A ∨ B) i.e. the hypothesis A ∨ B leads to a contradiction. We have two cases : if A is valid then it is in contradiction with the hypothesis ¬A similarly for B. So, in any case, we have a contradiction.

Conversely, we suppose that we have ¬(A ∨ B) and we prove ¬A i.e. A leads to contradiction. But if A is valid then A ∨ B is valid which contradicts the hypothesis. Similarly for B. However, we only have

(¬A ∨ ¬B ↔ ¬(A ∧ B)). The converse is valid only in classical logic.
Example 2: A → ¬¬A We suppose A then the supplementary hypothesis ¬A results in a contradiction. Hence we have the result. The converse is not valid in minimal logic and neither in intuitionistic logic. However we have ¬¬¬A → ¬A.

Example 3: We can show that in minimal logic ¬¬(A → B) → (¬¬A → ¬¬B) . But the converse is valid both in intuitionistic and classical logic but not in minimal logic.

Example 4: For the contra-positive argument : we can show that in minimal logic we have

(A → B) → (¬B → ¬A), (A → ¬B) → (B → ¬A) and (¬A → ¬B) → (B → ¬¬A) but we don't have (¬A → ¬B) → (B → A) which is a variant of reductio ad absurdum.

Curry-Howard Isomorphism

In programming language theory and proof theory, the Curry-Howard isomorphism is the direct relationship between computer programs and proofs. It is a generalization of a syntactic analogy between systems of formal logic and computational calculi. The Curry-Howard isomorphism is the observation that two families of formalisms-namely, the proof systems on one hand, and the models of computations on the other-are in fact structurally the same kind of objects. In other words, a proof is a program, the formula it proves is a type for the program.

In its more general formulation, the Curry-Howard isomorphism is a correspondence between formal proof calculi and type systems for models of computations. In particular, it splits into two correspondences. One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs which, this time, is specific to the particular choice of proof system and model of computation considered.

At the level of formulas and types, the correspondence says that implication behaves as a function type, conjunction as a product type (this may be called a tuple, a struct, a list, or some other term depending on the language), disjunction as a sum type (this may be called a union), a false formula as the empty type and a true formula as the singleton type (whose sole member is the null object). Quantifiers correspond to dependent function space or products (as appropriate). The following table summarizes

Correspondence between Hilbert-style Deduction Systems and Combinatory Logic

According to Curry: the simplest types for the basic combinators K and S of combinatory logic surprisingly correspond to the respective axiom schemes α → (β → α) and (α 2 used in Hilbert-style deduction systems. A complete section is devoted on this calculus as it is used to express formulas or properties of a program in our technique. We obtain a similar correspondence where both the columns are in one-to-one correspondence.

→ (β → γ)) → ((α → β) → (α → γ)) noted φ in Figure

Hilbert-style implication logic

α ∈ Γ assumption Γ α axiom K Γ α → (β → α) axiom S Γ φ Γ α → β Γ α modus ponens Γ β Simply typed combinatory logic x : α ∈ Γ Γ x : α Γ K : α → (β → α) Γ S : φ Γ E 1 : α → β Γ E 2 : α Γ E 1 E 2 : β

Logic side

Programming side assumption variable axioms combinators modus ponens application

Proof as program : applications

As seen above proofs act as programs and that a proof π of a property φ is equivalent to saying that the type of the λ-term associated with the proof is φ. This equivalence is useful in proof validation where one has to validate a proof π of a property (or a formula) φ. This is useful in applications where users need to be convinced that a free software developed by an untrusted agent satisfies a certain property. This trust problem is specific for free software because : they are not always developed by well-known companies (that users may trust), such software developments rely on a large community of authors for development/ proofs or these developers cannot afford code signing by a certifying authority. Now the question that stands is how exactly a user can be convinced that a software (or a program) is safe to use without relying on reputation or any certifying authority. There are several possibilities :

-using the Proof-Carrying Code framework [START_REF] Necula | Proof carrying code[END_REF] -probabilistic checking of the proof [START_REF] Arora | Probabilistic checking of proofs : A new characterization of NP[END_REF] -checking that the poof has been constructed using zero-knowledge protocols and Curry-Howard isomorphism.

SKI Combinatorial Calculus

The logical framework in which we are working is not the same as the one used in the PCC [START_REF] Necula | Proof carrying code[END_REF]. Our framework is that of a propositional calculus with a simplified axiomatic system. In the literature this logic is called SKI(SK) Combinatorial Calculus. The following sections present the features of this logical framework.

Presentation

We use the definition presented in subsection 2.2 to define SKI calculus as an example of propositional logic and in fact as the implicational fragment of any intuitionistic logic.

Definition

SKI calculus is obtained for the following instance of the sets: -A = {p, q, r, s, t, u, v} or any such finite set. Another way of defining the alphabet would be to take A = {S, K, I, (, )} -Ω 2 = {→}.

-The rule of modus ponens : if p and p → q are true then we can infer that q is also true.

-The set I being the set containing:

S: (p → (q → p)) K: ((p → (q → r)) → ((p → q) → (p → r))) I: (p → p)

Terms and Derivations

The set T of terms is defined recursively as follows:

1. S,K,I are terms.

2. If τ 1 and τ 2 are terms, then (τ 1 τ 2 ) is also a term.

3. Nothing is a term unless required to be by the rules 1 and 2.

A derivation is a finite sequence of terms satisfying the following rules:

1. If ∆ is a derivation ending in the term α((Kβ)γ)ζ, then ∆ followed by αβζ is also a derivation.

2. If ∆ is a derivation ending in the term α(Iβ)ζ, then ∆ followed by αβζ is also a derivation.

3. If ∆ is a derivation ending in the term α(((Sβ)γ)δ)ζ, then ∆ followed by α((βδ)(γδ)) is also a derivation.

Properties

The ceremony above captures much of the conventional style in which logicians present the combinator calculus. But the conventional ceremony describing the combinator calculus does not match the natural binary structure of the formal system. It is much more natural to understand the calculus as operating on binary tree-structured terms with the symbols S,K, I at the leaves. The parentheses are in some sense only there to indicate the tree structure, and shouldn't be regarded as part of the abstract alphabet.

Informally, and using programming language jargon, a tree (xy) can be thought of as a "function" x applied to an "argument" y. When "evaluated", the tree "returns a value" , i.e. transforms into another tree. Of course, all three of the "function", the "argument" and the "value" are either combinators, or binary trees, and if they are binary trees they too may be thought of as functions whenever the need arises. The evaluation operation is defined as follows :

I returns its argument : Ix = x K when applied to any argument x, yields a one-argument constant function Kx, which, when applied to any argument, returns x. Kxy = x S is a substitution operator. It takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third. More clearly :

Sxyz = (xz)(yz)

Computations

Example 1: SKSK evaluates to KK(SK) by the S-rule. Then if we evaluate KK(SK), we get K by the K-rule. As no further rule can be applied, the computation halts there.

Example 2: For all trees α and β, SKαβ will always evaluate to β in two steps, Kβ(αβ) = β, so the ultimate result of evaluating SKαβ will always equal the result of evaluating β. We say that SKα and I are "functionally" equivalent because they always yield the same result when applied to any β.

Example 3: Self-application SII is an expression that takes an argument and applies that argument to itself:

SIIα = Iα(Iα) = αα
Example 4: Recursion We can write a function that applies something to the self application of something else:

(S(Kα)(SII))β = Kαβ(SIIβ) = α(SIIβ) = α(ββ)
This function can be used to achieve recursion. If β is the function that applies to the self application of something else, then self-applying β performs α recursively on ββ. More clearly, if β = S(Kα)(SII) then :

SIIβ = ββ = α(ββ) = α(α(ββ)) = . . .

Example 5: Reverser S(K(SI))K reverses the terms in αβ: S(K(SI))Kαβ → K(SI)α(Kα)β → SI(Kα)β → Iβ(Kαβ) → Iβα → βα

Using example 2 it can be shown that SKI calculus is not the minimum system that can fully perform the computations of lambda calculus, as all occurrences of I in any expression can be replaced by SKK or SKS or SK and the resulting expression will yield the same result. So, I is merely syntactic sugar.

Universal Qualities of SKI

The combinator calculus was designed precisely to be universal in the sense that it can accomplish every conceivable rearrangement of sub-terms just by means of applying terms to them. That is, given a rule for rearranging n symbols into the shape of a term (allowing copying and deleting of individual symbols), there is a term that can be applied to each choice of n symbols so that several derivation steps will accomplish that rearrangement. The examples of SII as a repeater and S(K(SI))K as a reverser suggest how this works. This particular quality of a formal system is called combinatory completeness. Every formal system that contains something acting like S and something like K is combinatorialy complete.

Rearrangement arise in formal systems whenever we substitute symbols with variables. The combinator calculus was designed specifically to show that substitution for variables can be reduced to more primitive looking operations.

By accident, the combinator calculus turns out to be universal in a much more powerful sense than combinatory completeness. The combinator calculus is a universal programming system-its derivation can accomplish everything than can be accomplished by computation. That is, terms can be understood as programs, and every program that we can write in every programming language can be written also as a term in the combinator calculus. Since formal systems are the same thing as computing systems, every formal system can be described as an interpretation of the terms in the combinator calculus. In short, the combinator calculus is Turing complete. Last but not least, SKI calculus generates the implication fragment of intuitionistic logic.

As seen above the combinators S, K, I are functions and hence as the lambda calculus terms they are equivalent to :

-S:= λx.λy.λz.(xz)(yz) -K:= λx.λy.x -I := λx.x Using the typing rules defined in Figure 2 we can talk about typed SKI calculus. We observe that not all the terms in the calculus are typable. One of the example is the term in the example 3 of 4.2.1. From now on, SKI calculus refers to the typed SKI calculus.

Proofs as Cryptography

This section presents our alternative to the PCC technique where we use cryptographic techniques to implement a zero-knowledge proof of the validity of a proof of a given property. We should note that we have not been able to make the technique completely functional. Part of this section presents the goal and the steps that we have taken to tackle the different problems that we have faced and highlights some of these which remain unresolved.

There are several ways to present the communication model between the user and the developer, hitherto called consumer and producer respectively. This change in nomenclature is in consonance with the different possible models. One of the possible model implementing this technique could be: instead of proving a property of a program on the developer's side, we delegate the proof to an untrusted agent and we receive a small certificate guaranteeing that the proof has been done by this agent. We can even generalize this mechanism where the communication is done on a broadcast communication network, where terminals on the other end are provers and the user is the verifier. Upon receiving a program, the user might need to verify if a property holds for the program and so he gets in touch with provers (in broadcast network) and verifies if any of the provers has a valid proof.

We can even have a model where the user and the developer have no prior communication on the property and the user upon receiving a program (written by a certain developer) wants to verify the validity of a certain property on the program. He then looks for a zero-knowledge proof of the validity of the proof.

Another possible model could follow the same route as the PCC technique where the user and the developer agree on a property and then after writing the program the developer proves the property on the program and then sends the program (not the proof) to the user. The user then verifies the validity of the proof and ultimately forwards it to the waiting process. The following subsection discusses the latter one which remains in tune with the PCC except the fact that the proof term (λ-term) corresponding to the proof is not sent along with the program.

Communication Protocol

In fact, the protocol can be conceived in the following way and a schematic representation is given by Figure 3. The user and the developer agree on a property φ that a program must satisfy. The developer writes a program P , proves the property φ on P and sends it to the user. The user then uses cryptographic means to verify the validity of the proof. The property gives the encryption key while a proof term π (λ-term corresponding to the proof) gives a secret key. He then encrypts a nonce using the property and sends it to the developer, if the developer has a valid proof, he has a decryption algorithm (eventually depending on the λ-term corresponding to the proof) which can decrypt the nonce and the developer then sends the decrypted nonce to the user. The user verifies the exactitude of the nonce sent and the nonce received. This zero-knowledge proof conception makes our principle far more simpler and efficient compared to PCC.

Encryption

The predefined property φ is expressed in the (typed) SKI combinatorial calculus discussed in section 4. We give a recursive definition to the way a nonce {n} is encrypted under a property (a formula) φ. For that we define or initialize keys for each atomic terms like p, q, r used to define the alphabet A, and we denote

• • φ • • P • • {n} φ • • Dec π ({n} φ )
User (P, φ) Developer (P, φ)

Figure 3: Communication Protocol them by K p , K q , K r . We then define the key K p→q as {K q } Kp to be read as the key K q encrypted under the key K p . Finally, encryption of a nonce {n} under any formula

A → B is the set {K A , {n} K B }.
The following examples encrypt a nonce {n} under the axioms of the SKI calculus.

Example I:

We encrypt a nonce {n} under I as {n} p→p which is the set K p , {n} Kp .

Example S: {n} under S is {n} (p→(q→p)) which is the set {K p , {n} q→p } and which eventually is the set {K p , K q , {n} Kp } Example K: {n} under K is {n} ((p→(q→r))→((p→q)→(p→r))) which is:

{K (p→(q→r)) , {n} (p→q)→(p→r) } = {{K q→r } Kp , K p→q , {n} p→r } = {{{K r } Kq } Kp , {K q } Kp , K p , {n} Kr }

Provable-Decryptable Equivalence

Loosely speaking, decryption of a nonce {n} encrypted under a formula F is actually an algorithm that (at each instant) makes a choice from the available keys and a key encrypted under this key or eventually the nonce under the chosen key. If the property is provable in the SKI calculus, the process terminates with the decrypted nonce. Before delving in the problem of proving the fact that having a proof is equivalent to having a decryption algorithm, we can see that the examples taken in the previous subsection proves the fact that the encryption process has the soundness property. The Provable-Decryptable equivalence can even be expressed by saying that one cannot decrypt a nonce encrypted under a formula that is not provable in the SKI calculus.

Decryptable implies Provable

The only operator in our logic is implication →, two rules of natural deduction that correspond to introduction and elimination of → are :

Γ, A B (→) introduction Γ A → B Γ A Γ A → B (→) elimination Γ B
The introduction rule corresponds to the axiom I while the elimination rule corresponds to the inference rule of modus ponens in our logic. 6 We observe that the encryption algorithm implements a recursive → elimination which is to ascend upwards in the (→) introduction rule and that at any stage of the derivation tree (corresponding to the proof) and for any sequent A 1 , A 2 , . . . , A n B the encryption at this stage gives {K A1 , K A2 , . . . , K An , {n} B }. Thus the antecedent correspond to the keys while the succedent gives the encryption of the nonce under the key corresponding to it. The process terminates when the succedent is an atomic term (a formula devoid of the operator →).

The decryption process starts by searching the key corresponding to the atomic term under which the nonce is encrypted or any available encryption of the key. The decryption of this key might require decryption of other keys. Each decryption (of either a key or eventually the nonce) mirrors into the application of (→) elimination rule. For instance, {K p , {K q } Kp , {n} Kq } corresponds to the encryption using the sequent p, (p → q) q, which is precisely the (→) elimination. In general if K Γ decrypts {n} K A then Γ A. Decryptability implies the existence of a function π such that π(K Γ ) = K A . The function π in fact implements a recursive application of modus ponens and hence implements (→) elimination rule. So, if encryption is ascending upwards (away from the root) 7 in the derivation tree, decryption is descending downwards (towards the root) in the derivation tree and hence is equivalent to building the proof tree. This proves that decryptable implies provable.

Provable implies Decryptable

This part of the implication is non-trivial and hence requires careful observation via examples.

Example 1 p → ((p → q) → q) Encryption of a nonce n under the formula gives :

{n} p→((p→q)→q) = {K p , {n} ((p→q)→q) } = {K p , K p→q , {n} Kq } = {K p , {K q } Kp , {n} Kq } p, (p → q) p p, (p → q) (p → q) p, (p → q) q Encryption termination step p (p → q) → q p → ((p → q) → q)
Proof 1: Proof tree

We use the available key K p to retrieve K q and ultimately n. To be more formal we can use the proof-term corresponding to Proof 1 to decrypt the nonce. The proof-term corresponding to the above formula is : λx.λf.f x and captures the idea of typing rules: if x is of type p and f is of type p → q then f x is of type q.

The corresponding decryption algorithm would be λx.λf.λc.c(f x) and works in the following way :

λx.λf.λc.c(f x){n} p→((p→q)→q) = λx.λf.λc.c(f x)K p {K q } Kp {n} Kq = {n} Kq ({K q } Kp K p ) = {n} Kq K q = n 6.
Using the soundness of → wrt : if Γ → A, then Γ A, and completeness of → wrt : if Γ A, then Γ → A. 7. root being the formula to be proven

Example 2 ((p → q) → q) → p {n} ((p→q)→q)→p = {K (p→q)→q , {n} Kp } = {{K q } {{Kq} Kp } , {n} Kp }

As no free key is available it seems we cannot decrypt n and this is exactly what we expect (if we hope that provability implies decryptability) because the above formula is not provable in our logic. We can check different formulations of contra-positive argument :

Example 3.1 (p → q) → ((q → r) → (p → r)) {n} (p→q)→((q→r)→(p→r)) = {{K q } Kp , {K r } Kq , K p , {n} Kr } Example 3.2 (p → (q → r)) → (q → (p → r)) {n} (p→(q→r))→(q→(p→r)) = {{{K r } Kq } Kp , K q , K p , {n} Kr } Example 3.3 ((p → r) → (q → r)) → (q → ((p → r) → r)) {n} ((p→r)→(q→r))→(q→((p→r)→r)) = {{{K r } Kq } {{Kr} Kp } , K q , {K r } Kp , {n} Kr } Example 3.4 ((p → r) → (q → r)) → (q → p) {n} ((p→r)→(q→r))→(q→p) = {{K r } Kq } {{Kr} Kp } , K q , {n} Kp
The first three decryptions are obvious and follow the same pattern as in the first example. But the fourth encryption cannot be reversed and again the reason should be the fact that the last formula is not provable in our logic (subsection 2.4).

Example 4 ((p → q) → r) → (q → r) Encryption of a nonce n gives {n} ((p→q)→r)→(q→r) = {{K r } {{Kq} Kp } , K q , {n} Kr } At the first sight the above nonce does not seem to be decryptable but here we note that the formula is provable and a derivation tree is given in Proof 2. p, q, (p → q) → r q q, (p → q) → r (p → q) q, (p → q) → r (p → q) → r q, (p → q) → r r Encryption termination step (p → q) → r (q → r)

((p → q) → r) → (q → r)
Proof 2: Proof tree A careful observation would reveal that to decrypt the nonce the developer either needs the key K p or {K q } Kp while knowing K q . The second case is realizable because the developer can ask the user to encrypt K q under the key K p (that he doesn't have). A number of questions on security might arise but it seems to be a legitimate demand on the part of developer. And if we permit such queries the decryption is automatic.

From the perspective of the proof term :

λH.λH 0 .H (λ x Kp . H 0 Kq ) Kp→q if
x is of type p, H 0 of type q and H of type (p → q) → r, then the type of the initial formula is given by the λ-term given above. In terms of encryption keys, the decryption algorithm substitutes x by K p , H 0 by K q and so λx.H 0 by K p→q . So, a decryption algorithm would indeed need the key K p→q = {K q } Kp in order to decrypt the nonce. We observe that in the proof term H is applied to a λ-term which is not the case in the previous examples.

Example 5.1 (((p → r) → r) → ((q → r) → r)) → (((p → q) → r) → r) A nonce n encrypts to : {n} (((p→r)→r)→((q→r)→r))→(((p→q)→r)→r) = K (((p→r)→r)→((q→r)→r)) , {n} ((p→q)→r)→r

= {K (q→r)→r } K (p→r)→r , {K r } Kp→q , {n} Kr = {{K r } {{Kr} Kq } } {{Kr} {{Kr } Kp } } , {K r } {{Kq} Kp } , {n} Kr
Once again formula not being provable implies that the nonce cannot be retrieved. Before analyzing an encrypted nonce under this formula which is the converse of the implication in the previous example, we observe that a proof does exist and is given by the derivation tree in Proof 3.

Example 5.2 (((p → q) → r) → r) → (((p → r) → r) → ((q → r) → r)) A nonce n
If we have a look at the proof term

λH.λH 0 .λH 1 .H(λH 2 .H 0 (λH 3 .H 1 ( H 2 Kp→q H 3 Kp ))) it says that if : H is of type ((p → q) → r) → r , H 0 is of type (p → r) → r
and H 1 of type q → r then : the type of the initial formula is given by the λ-term. Here the types of H 3 and H 2 are p and p → q respectively. In the decryption algorithm, they should be substituted by keys K p and K p→q which are not available to the developer. Here again we observe that H applies on a λ-term as in Example 4.

The above example seems to be a threat to the proposition Provability implies Decryptability and remains unresolved.

p, q p Γ 2 , p p Γ 2 p → q Γ 2 , p q Γ 2 , p q → r Γ 2 , p r Γ 2 p → r Γ 2 (p → r) → r Γ2 Γ 1 , (p → q) r Γ 1 (p → q) → r Γ 1 ((p → q) → r) → r Γ1 ((p → r) → r), ((p → q) → r) → r, q → r r Encryption termination step (p → r) → r, ((p → q) → r) → r (q → r) → r ((p → q) → r) → r ((p → r) → r) → ((q → r) → r) (((p → q) → r) → r) → (((p → r) → r) → ((q → r) → r))
Proof 3: Proof tree A quick observation of the encryption process leads us to remark that the encryption algorithm is precisely moving upwards in the proof-tree and the algorithm terminates when the succedent at the indicated step becomes an atomic term which is ⊥ in Proof 3, r in Proof 2 and q in Proof 1. So, encryption is not exactly building the proof itself though in some cases, they might precisely be the same; for example this happens for the property q → (p → p), Proof 4. In the worst case, the size of the encrypted nonce can be linear in the size of the proof.

Remarks

We consider the two deduction rules (and the only ones in fact) taken from sequent calculus that act on implications.

Γ, A B Γ A → B

This rule says that if one can decrypt {n} A→B using the key K Γ then one is able to decrypt {n} K B if one has the keys K A and K Γ and vice-versa. This is true because by definition {n} A→B = {{n} K B , K A } and the nonce can be decrypted iff K Γ and K A yield K B and this suffices to decrypt {n} K B as well.

Γ A, C Γ, B C Γ, A → B C
In the same tune, the above rule says if keys K Γ and K A→B = {K B } K A can decrypt {n} K C then K Γ must be able to decrypt {n} K A and K Γ , K B must be able to decrypt {n} K C and vice-versa. To be precise K Γ must yield K A (neglecting the trivial case where it yields K C ). For this we might suppose to have a function f that serve this purpose.

If we have some way to define such a function then the problem would be solved and then encryption under a formula is equivalent to applying the first rule and terminate at the point where the succedent is an atomic term. The decryption would be to apply the second rule or the first one to build the complete tree if possible.

Applications

As suggested in the paper [START_REF] Necula | Proof carrying code[END_REF], PCC technique can be used to implement "safe network packet filters". It remains in the experimental stage. Many modern operating systems provide a facility for allowing application programs to receive packets directly from the network device. Typically, an application is not interested in receiving every packet from the network, but only a small fraction that exhibit a specific property (e.g. an application might want only TCP packets destined for a Telnet port. In such cases, it is highly profitable to allow application program to specify a boolean function on network packets, and then have this filter run within kernel's address space. The kernel can then avoid delivering uninteresting packets to the application, thereby saving the cost of many unnecessary context switches. Our technique can prove to be an alternative to PCC for such applications ( if our technique could provide a sufficient condition i.e. provable implies decryptable).

Another possible application could be in the implementation of a program checker. A user upon receiving a program wants to verify whether the terminal executing the program has properly evaluated the program on a particular input. Another possible variant could be that : we suppose that an independent software vendor publishes a program with a signature and a user wants to execute the program on an input (possibly via an agent) and wants some sort of a proof or a signature derived from the original one that attests to the fact that it was exactly the same program that was evaluated on the input.

Conclusion and Future work

Until now, proofs have been seen as programs, the following table explains this with an example :

Property

Proof Type φ λ-term π : φ φ = (A → (A → B)) → B π = λx.λf.f x We observe that from any proof π A of A, we can construct a proof π A→B of A → B and using π we can construct a proof π B of B.

ππ A π A→B = (λx.λf.λf x)π A π A→B = π A→B π A = π B
With the help of the technique presented in this report we try to see proofs as cryptography and try to extend the Curry-Howard isomorphism to cryptography though we are successful in only one direction (i.e. a decryption algorithm π for a nonce encrypted under a property φ gives a proof of the property).

Property

Proof Type φ λ-term π : φ Encryption key φ Decryption algorithm π Use of cryptography to implement zero-knowledge proof makes the implementation more efficient compared to that of PCC and hence the user is no longer forced to send the proof with the code which might contain informations that the user should not have access to. In the PCC framework, the VC predicate is computed twice : once to prove it and the other time to verify it. This might be a waste of time. The other point to note is that the verification process might be long and difficult; in our case it is just a string comparison of the nonce sent and the nonce received. In all these contexts, our technique proves to provide an upper hand to both the user and the developer.

The Proof-Carrying Code is considered to be intrinsically safe: most attempts to tamper with either code or the proof results in a validation error. In the few cases, when the code and the proof are modified such that validation still succeeds, the new code is also safe. But, in this case, the modified program might not be the one that the consumer is waiting for. Our technique rejects the result of any possible tamper either with the property or with the program and this is made possible by the intrinsic cryptographic system.

A further observation reveals that the encryption of a nonce under a property is building a part of the proof tree (in the worst case building it completely) and decryption is to finish the rest of the tree. The future work would be to prove that Provability implies Decryptability which might require a complete shift from the encryption algorithm. And then we could try to extend the logical framework and search for an efficient encryption scheme that can be implemented in first-order constructive logic (such that it deals with the quantifiers) and reduces the size of the encrypted nonce (which is sending a nonce under an atomic formula with several keys). Another line of work would be to make empirical tests on the application of this technique while reducing the size of the information passed to the developer.

Figure 1 :

 1 Figure 1: Inference rules of natural deduction

Figure 2 :

 2 Figure 2: Typed combinatory logic

  encrypted under the formula is given as : {n} (((p→q)→r)→r)→(((p→r)→r)→((q→r)→r)) = {K ((p→q)→r)→r , {n} (((p→r)→r)→((q→r)→r)) } = {K ((p→q)→r)→r , K (p→r)→r , {n} (q→r)→r } = {{K r } {{Kr} {{Kq } Kp } } , {K r } {{Kr} Kp } , {n} (q→r)→r } = {{K r } {{Kr} {{Kq } Kp } } , {K r } {{Kr} Kp } , {K r } Kq , {n} Kr }

We suppose that the producer and the consumer have no prior communication and the consumer upon receiving a program (written by a certain producer) wants to verify the validity of a certain property on the program.

2.3 Classical, Intuitionistic & Minimal LogicThe logics presented above are classical logic and in general they are characterized by a number of equivalent axioms :Proof by contradiction

Γ, A B →-intro Γ A → B Γ, A ⊥ ¬-intro Γ ¬A excluded middle Γ A ∨ ¬A Γ ⊥ ⊥-elim Γ A

Γ A ∧ B ∧ -elim Γ B Γ A ∨ B Γ, A C Γ, B C ∨ -elim Γ C

Encryption termination step{n} q→(p→p) = {K q , K p , {n} Kp } q (p → p) q → (p → p) Proof 4: Proof tree


Thomas Dedieu

Fabio Perroni

Fritz Grunewald

THE FUNDAMENTAL GROUP OF QUOTIENTS OF A PRODUCT OF CURVES

Keywords: Mathematics Subject Classification. 32Q55, 14H30, 20F34. 1

We prove a structure theorem for the fundamental group of the quotient X of a product of curves by the action of a finite group G, hence for that of any resolution of the singularities of X.

Introduction

The study of varieties isogenous to a product of curves was initiated by Catanese in [START_REF] Catanese | Fibred surfaces, varieties isogenous to a product and related moduli spaces[END_REF], inspired by a construction of Beauville. These varieties are quotients of a product of smooth projective curves C 1 × • • • × C n by the free action of a finite group G.

Much of the work in this area has been focused in the n = 2 case. Surfaces isogenous to a product of curves provide a wide class of surfaces quite manageable to work with, since they are determined by discrete combinatorial data. They were used successfully to address various questions (see e.g. the survey paper [START_REF] Bauer | Complex surfaces of general type: some recent progress[END_REF]), and in particular to obtain substantial information about various moduli spaces of surfaces of general type (see e.g. [START_REF] Bauer | Some new surfaces with pg = q = 0[END_REF][START_REF] Bauer | The classification of surfaces with pg = q = 0 isogenous to a product of curves[END_REF][START_REF] Bauer | Quotients of products of curves, new surfaces with pg = 0 and their fundamental groups[END_REF]).

In the case of a variety isogenous to a product, the action of G is free, and X := (C 1 × • • • × C n )/G is smooth. Furthermore, we have the following natural description of the fundamental group of X.

Proposition 1.1. [START_REF] Catanese | Fibred surfaces, varieties isogenous to a product and related moduli spaces[END_REF] If X := (C 1 × • • • × C n )/G is the quotient of a product of curves by the free action of a finite group, then the fundamental group of X sits in an exact sequence

1 → Π g1 × • • • × Π gn → π 1 (X) → G → 1, (1.1)
where each Π gi is the fundamental group of C i . This extension, in the unmixed case where each Π gi is a normal subgroup, is determined by the associated maps G → Out (Π gi ) to the respective Teichmüller modular groups.

In the recent paper [START_REF] Bauer | Quotients of products of curves, new surfaces with pg = 0 and their fundamental groups[END_REF], Bauer, Catanese, Grunewald and Pignatelli prove that a similar statement still holds under weaker assumptions.

Theorem 1.2. [BCGP09, Thm. 0.10 and Thm. 4.1] Assume that G acts faithfully on each curve C i as a group of automorphisms, and let X := (C 1 × • • • × C n )/G be the (possibly singular) quotient by the diagonal action of G. Then the fundamental group π 1 (X) has a normal subgroup of finite index isomorphic to the product of n surface groups. We call G ′ the quotient group.

Here, by a surface group we mean a group isomorphic to the fundamental group of a compact Riemann surface. Note that, unlike in Proposition 1.1, the surface groups in Theorem 1.2 above are not necessarily isomorphic to the fundamental groups of the curves C 1 , . . . , C n , and furthermore that the corresponding quotient

G ′ of π 1 (X) is not necessarily isomorphic to G.
The first step of the proof of Theorem 1.2 consists in showing that π 1 (X) is isomorphic to the quotient of the fibre product

T := T 1 × G • • • × G T n of
n orbifold surface groups (see Subsection 2.1) by its torsion subgroup Tors(T). Whereas this first part rests upon geometrical considerations, the rest of the proof relies on an abstract group theoretic argument showing that this quotient necessarily contains a normal subgroup as described in Theorem 1.2. In particular, the relation occurring between the groups G and G ′ is not well understood.

Using a suitable resolution of the singularities of X, Bauer, Catanese, Grunewald and Pignatelli show in addition that the fundamental group of any resolution Y of X is isomorphic to the fundamental group of X, so that the same description holds for π 1 (Y ).

In [START_REF] Bauer | Quotients of products of curves, new surfaces with pg = 0 and their fundamental groups[END_REF], as an important application of Theorem 1.2, many new families of algebraic surfaces S of general type with p g (S) = 0 are constructed, and several new examples of groups are realized as the fundamental group of an algebraic surface S of general type with p g (S) = 0. This increases notably our knowledge on algebraic surfaces. In fact the authors consider and classify all the surfaces whose canonical models arise as quotients X := (C 1 × C 2 ) /G of the product of two curves of genera g(C 1 ), g(C 2 ) ≥ 2 by the action of a finite group G such that p g (X) = q(X) = 0.

In the present paper, we drop the assumption that the actions of G on C 1 , . . . , C n are faithful. We obtain the following expected strengthening of Theorem 1.2. Theorem 1.3. Let C 1 , . . . , C n be smooth projective curves, and let G be a finite group acting on each C i as a group of automorphisms. Then the fundamental group of the quotient X := C 1 × • • • × C n /G by the diagonal action of G has a normal subgroup of finite index that is isomorphic to the product of n surface groups.

This result should allow in the future the realization of interesting groups as fundamental groups of higher dimensional algebraic varieties, following the method developed in [START_REF] Bauer | Quotients of products of curves, new surfaces with pg = 0 and their fundamental groups[END_REF] for surfaces. Notice that, in the case where the G-actions are faithful, X can only have isolated cyclic-quotient singularities, while if the actions are not faithful, then the singular locus of X can have components of positive dimension, and the singularities are abelian-quotient singularities.

Again, one shows that any desingularization of the quotient X has a fundamental group isomorphic to that of X. This time however, we have to rely on a strong result of Kollár [K93].

The proof follows then closely the one of Theorem 1.2 of [START_REF] Bauer | Quotients of products of curves, new surfaces with pg = 0 and their fundamental groups[END_REF]. The main new difficulty one has to overcome is to find a natural counterpart to the fibered product

T 1 × G • • • × G T n ,
acting discontinuously on the product C1 × • • • × Cn of the universal covers of C 1 , . . . , C n . After that similar group theoretic arguments work with some slight modifications.

It has already been observed in [START_REF] Catanese | Fibred surfaces, varieties isogenous to a product and related moduli spaces[END_REF] that Theorem 1.3 follows directly from Theorem 1.2 when n = 2, by performing the quotient (C 1 × C 2 ) /G in successive steps. For n > 2 however, this procedure does not apply.

The paper is organized as follows. In Section 2, we fix notations and collect some basic facts about group actions on compact Riemann surfaces. Section 3 is devoted to the proof of Theorem 1.3: the proof itself is given in Subsection 3.1, using intermediate results proven in Subsections 3.2 and 3.3.

Acknowledgements. We are indebted to Prof. Ingrid Bauer for suggesting this problem to us and for many useful conversations. We express our thanks to Profs. Fabrizio Catanese and Keiji Oguiso for their interest and warm encouragement. In particular, we thank Prof. Oguiso for bringing the paper [K93] to our attention. We also wish to thank Wenfei Liu and Matteo Penegini for worthy conversations on the subject.

This work started as the first-named author held a post-doctoral position at the Universität Bayreuth, supported by the DFG-Forschergruppe 790 "Classification of Algebraic Surfaces and Compact Complex Manifolds". He is grateful to this institution for providing excellent working conditions.

Notations and basic results

2.1. Notations. We work over the field of complex numbers C.

Let G be a group, and consider a subset

H ⊂ G. We write H ≤ G when H is a subgroup of G, and H ✂ G when H is a normal subgroup of G. If A ⊂ G is any subset, then A G denotes the normal subgroup of G generated by A.
Let g be a non negative integer. We call Π g the surface group of genus g, defined as

Π g := a 1 , b 1 , . . . , a g , b g g i=1 [a i , b i ] = 1 .
This is the fundamental group of compact Riemann surfaces of genus g. On the other hand, letting in addition m 1 , . . . , m r be positive integers, we denote by T(g; m 1 , . . . , m r ) the orbifold surface group of signature (g; m 1 , . . . , m r ), defined as

T(g; m 1 , . . . , m r ) := a 1 , b 1 , . . . , a g , b g , c 1 , . . . , c r c m1 1 = • • • = c mr r = g i=1 [a i , b i ] • c 1 • • • • • c r = 1 .
It is obtained from the fundamental group of the complement of a set of r distinct points in a compact Riemann surface of genus g, by quotienting by the normal subgroup generated by γ m1 1 , . . . , γ mr r , where each γ i is a simple geometric counterclockwise loop around the i-th removed point.

Let G be a finite group. An appropriate orbifold homomorphism is a surjective homomorphism ϕ : T(g; m 1 , . . . , m r ) → G such that ϕ(c i ) has order m i for i = 1, . . . , r.

The action of a group G as a group of homeomorphisms on a topological space X is said to be discontinuous if the following two conditions are satisfied: (i) the stabilizer of each point of X is finite; (ii) each point x ∈ X has a neighbourhood U such that g(U ) ∩ U = ∅, for each g ∈ G such that gx = x.

Basic results. The following result is essentially a reformulation of Riemann's existence theorem (see [BCGP09, Thm. 2.1]).

Theorem 2.1. A finite group G acts faithfully as a group of automorphisms on a compact Riemann surface of genus g if and only if there are natural numbers g ′ , m 1 , . . . , m r and an appropriate orbifold homomorphism ϕ : T(g ′ ; m 1 , . . . , m r ) → G such that the Riemann-Hurwitz relation holds:

2g -2 = |G| 2g ′ -2 + r i=1 1 - 1 m i .
Remark 2.2. As already remarked in [START_REF] Bauer | Quotients of products of curves, new surfaces with pg = 0 and their fundamental groups[END_REF], under the above hypotheses, g ′ is the geometric genus of

C ′ := C/G,
:= p -1 (C ′ • ).
In particular, ϕ(c i ) generates the stabilizer of the corresponding ramification point. Furthermore, the kernel of ϕ is isomorphic to the fundamental group π 1 (C), and the action of π 1 (C) on the universal cover C of C extends to a discontinuous action of T := T(g ′ ; m 1 , . . . , m r ). Let u : C → C be the covering map. It is ϕ-equivariant, and C/G ∼ = C/T .

We now give two elementary facts that will be used in the following. (ii) Let t ∈ St x . Then t is conjugated to c m i , for some i ∈ {1, . . . , r} and m ∈ N. Proof. The π 1 (C)-action on C is free, so π 1 (C)∩St x = {1}. This yields (i), because π 1 (C) is the kernel of ϕ.

To prove (ii), let y = u(x). If t = 1, then the result is clear. Else, there exists an integer i ∈ {1, . . . , m} and a point x ′ ∈ u -1 (y) that is fixed by c i . It then follows from (i) that St x ′ = c i , hence that t is conjugated to a power of c i .

Main Theorem

The main result of the paper is the following Theorem 3.1. Let C 1 , . . . , C n be compact Riemann surfaces, and let G be a finite group that acts as a group of automorphisms on each C i . We consider the quotient of the product C 1 × • • • × C n by the diagonal action of G. Then there is a normal subgroup of finite index Π in the fundamental group

π 1 C 1 × • • • × C n G ,
such that Π is isomorphic to the product of n surface groups.

Notice that, according to notations 2.1, a surface group is a group isomorphic to the fundamental group of a compact Riemann surface of genus a non negative integer g, in particular we admit also the "degenerate cases" where g = 0, 1.

The proof of this theorem follows closely that of [BCGP09, Thm. 4.1], and is given in the next subsections. Before we move on to this proof, let us give the following important consequence of Theorem 3.1.

Corollary 3.2. Let C 1 , . . . , C n and G be as in the statement of Theorem 3.1, and let Y be a resolution of the singularities of

X := (C 1 × • • • × C n )/G.
Then, the fundamental group of Y is isomorphic to the fundamental group of X, and moreover it has a normal subgroup of finite index isomorphic to the product of n surface groups.

Proof. The natural morphism

f * : π 1 (Y ) -→ π 1 (X)
induced by the resolution f : Y → X is an isomorphism. This follows directly from [K93, Sec. 7]: since X is normal and only has quotient singularities, Y is locally simply connected by [K93, Thm. 7.2], hence f * is an isomorphism by [K93, Lem. 7.2]. The second claim is now a direct consequence of Theorem 3.1.

3.1. Proof of the main theorem. For i = 1, . . . , n, we let

K i = ker (G → Aut(C i )) and H i = G/K i ,
where G → Aut(C i ) is the morphism associated to the action of G on C i . We call p i the projection G → H i . Now H i acts faithfully on C i , so we have (see Remark 2.2) a short exact sequence

1 → π 1 (C i ) → T i ϕi -→ H i → 1, (3.1)
where T i is an orbifold surface group, and ϕ i is an appropriate orbifold homomorphism. Let Σ i := G × Hi T i be the fibered product corresponding to the Cartesian

diagram Σ i ψi G G ✷ T i ϕi G pi G G H i .
We call ψ i : Σ i → G the projection on the first factor. Pulling-back (3.1) by p i : G → H i , we obtain a short exact sequence

1 → π 1 (C i ) → Σ i ψi -→ G → 1, (3.2)
where the left-hand side map is

γ ∈ π 1 (C i ) → (1, γ) ∈ Σ i . Next, we define G := Σ 1 × G • • • × G Σ n as the fibered product correponding to the Cartesian diagram below. G x x p p p p p p p p p Ð Ð Ò Ò Ò Ò Ò 2 2 f f f f f @ @ Σ 1 9 9 x x x x x x x x x Σ 2 0 0 b b b b b . . . Σ n-1 } } { { { { { Σ n v v m m m m m m m m m m m m G Let ∆ : G → G × • • • × G be the diagonal morphism. Then G can also be seen as the fibered product G × (Gו••×G) (Σ 1 × • • • × Σ n ) → G
with respect to the two morphisms ∆ and (ψ 1 , . . . , ψ n ). Therefore, the pull-back by ∆ of the product of the n exact sequences (3.2) for i = 1, . . . , n is a short exact sequence

1 → n i=1 π 1 (C i ) → G Ψ -→ G → 1, (3.3) where Ψ is the first projection G × (Gו••×G) (Σ 1 × • • • × Σ n ) → G.
Now we have the following, coming from the fact that G acts discontinuously on the universal cover of

C 1 × • • • × C n .
Proposition 3.3. Let G′ ✂ G be the normal subgroup of G generated by those elements which have non-empty fixed-point set. Then

π 1 C 1 × • • • × C n G ∼ = G G′ .
Proof. For i = 1, . . . , n, the action of T i on the universal covering Ci of C i (see Remark 2.2) induces an action of Σ i on Ci via the projection of Σ i on its second factor T i . We obtain in this way an action of G on the product C1 × • • • × Cn . This action is discontinuous: let St x be the stabilizer of a point x ∈ C1 × • • • × Cn with respect to the action of G. Then the same argument as that in the proof of Lemma 2.3 shows that Ψ |Stx is injective, from which it follows that St x is finite because G is finite. On the other hand, condition (ii) in the definition of a discontinuous action is a consequence of the fact that the T i -actions are themselves discontinuous.

Then, the main theorem in [START_REF] Armstrong | The fundamental group of the orbit space of a discontinuous group[END_REF] applies to our situation, and gives a group isomorphism

π 1 C1 × • • • × Cn G ∼ = G G′ .
Eventually, since the universal covering

U : C1 × • • • × Cn → C 1 × • • • × C n is Ψ- equivariant, we have an isomorphism C 1 × • • • × C n G ∼ = C1 × • • • × Cn G ,
and the proposition follows.

Remark 3.4. The elements of G which have fixed-points are precisely those elements of finite order. Therefore G′ is the torsion subgroup of G.

Now the proof of Theorem 3.1 relies on the following result, the proof of which we postpone to Subsection 3.3.

Proposition 3.5. The quotient G/ G′ is an extension

1 → E → G/ G′ θ -→ T → 1
of a finite group E by a group T that is a finite-index subgroup of a product of n orbifold surface groups.

Using the results of [START_REF] Grunewald | Cohomological goodness and the profinite completion of Bianchi groups[END_REF], the latter fact enables one to show that there is a finite index normal subgroup Γ ✂ G/ G′ that injects in T : Lemma 3.6. Let S be a group sitting in an exact sequence

1 → E → S → T → 1,
where E is a finite group, and T is a finite index subgroup of a product of n orbifold surface groups. Then S is residually finite. In particular, there exists a finite index normal subgroup Γ ✂ S such that Γ ∩ E = {1}.

Proof. By [GJZ08, Prop. 6.1], an extension of a finite group by a group that is residually finite and good in the sense of [START_REF] Serre | Cohomologie galoisienne[END_REF] is residually finite. It therefore suffices to show that T enjoys the two aforementioned properties.

An orbifold surface group is residually finite. Therefore T is itself residually finite, being a finite index subgroup of a product of orbifold surface groups.

By [GJZ08, Lem. 3.2], it is enough to show that a product of orbifold surface groups is good to prove that T is good. But [GJZ08, Prop. 3.7] tells us that an orbifold surface group is good, and [GJZ08, Prop. 3.4] that a product of good groups is good.

We are now in a position to complete the proof of our main theorem:

Proof of Theorem 3.1. Let T 1 × • • • × T n
be a product of n orbifold surface groups containing T as a finite index subgroup, and let us consider Γ ✂ G/ G′ a normal subgroup of finite index such that

E ∩ Γ = {1}. Then θ(Γ) ≤ T 1 × • • • × T n has finite index.
Now every orbifold surface group contains a surface group as a finite index subgroup (see e.g. [START_REF] Beardon | The geometry of discrete groups[END_REF]), so let Π i be a finite index surface group in T i for each i = 1, . . . , n.

For each i, we consider

θ(Γ) i := θ(Γ) ∩ ({1} × • • • × T i × • • • × {1})
as a subgroup θ(Γ) i ≤ T i , and set

Π ′ i := g∈Ti g (θ(Γ) i ∩ Π i ) g -1 ,
the biggest normal subgroup of T i contained in θ(Γ) i ∩ Π i . Then Π ′ i has finite index in Π i , and thus is itself a surface group. Eventually, Π :

= Π ′ 1 × • • • × Π ′
n is a subgroup of θ(Γ), which is normal and of finite index in T . Therefore, θ -1 (Π) ∩ Γ is a normal subgroup of G/ G′ , with finite index, and isomorphic to Π.

3.2.

Results in group theory. In this subsection, we prove some technical results that are needed for the proof of Proposition 3.5.

Let Σ be any group, R ✂ Σ be a normal subgroup, and L ⊂ Σ be a subset. We define We call R and L the images of R and L respectively by the projection Σ → Σ.

N (R, L) := {hkh -1 k -1 | h ∈ L , k ∈ R} Σ (3.
There is an isomorphism: Σ/ L Σ ∼ = Σ/ L Σ . Notice also that N (R, L) ✂ R and N (R, L) ✂ L Σ , which implies that R is a normal subgroup of Σ.

Lemma 3.7. If R ✂ Σ has finite index, and if L ⊂ Σ is a finite subset consisting of elements of finite order, then L Σ is finite.

Proof. The subgroup L Σ is the image of L Σ under the projection Σ → Σ. Since R has finite index in Σ, and L is finite, it follows that L Σ is generated by finitely many elements which are conjugated to those of L. Since the elements of L have finite order, these generators have finite order as well.

The center Z L Σ of L Σ contains R ∩ L Σ, and hence has finite index in L . Now, by [BCGP09, Lem. 4.6], if a group S is generated by finitely many elements of finite order, and if its centre has finite index in S, then S is finite. From this we conclude that L Σ is finite.

We now consider the particular case when Σ is a group constructed as in Subsection 3.1: Σ = G × H T, where G is a finite group, H is a quotient of G, and T is any group coming with a surjective morphism ϕ : T → H.

Lemma 3.8. The projection on the second factor q : Σ → T induces a morphism

q : Σ L Σ → T q(L) T (3.6)
in a natural way. It is surjective, and has finite kernel.

Proof. We have q ( L Σ ) = q(L) T . The map q is therefore induced by the composition Σ q -→ T → T/ q(L) T , which is clearly surjective. To prove the finiteness of its kernel, notice that for any (g, t) ∈ q -1 ( q(L) T ), there exists h ∈ G with (h, t) ∈ L Σ , hence gh -1 ∈ K := ker(G → H). It follows that q -1 ( q(L) T ) = K L Σ , where K is seen as a subgroup in Σ via the injection k ∈ K → (k, 1) ∈ Σ. Eventually, ker(q) ∼ = K ⊂ G, which is finite.

3.3.

Realization of the fundamental group as a suitable extension. In this subsection, we give a full proof of Proposition 3.5. We use the basic results in group theory established in Subsection 3.2 above.

For i = 1, . . . , n, we fix the following presentation for the orbifold groups T i in (3.1):

T i = a i1 , b i1 , . . . , a igi , b igi , c i1 , . . . , c iri c mi1 i1 = • • • = c mir i iri = gi j=1 [a ij , b ij ] • c i1 • • • • • c iri = 1 ,
and set R i = π 1 (C i ). We write the elements of G as (g, z 1 , . . . , z n ), with (g, z i ) ∈ Σ i for i = 1, . . . , n. Then we have:

Lemma 3.9. For each i = 1, . . . , n, there exists a finite subset N i ⊂ G, such that

N i G = G′ ,
and whose elements are of the form (g, z 1 d ℓ1 1 z -1 1 , . . . , d ℓi i , . . . , z n d ℓn n z -1 n ) for some g ∈ G, some d j ∈ {c j1 , . . . , c jrj } and ℓ j ∈ N for j = 1, . . . , n, and some z j ∈ T j for j = i. and the fact that N i G = G′ .

For i = 1, . . . , n, we let L i ⊂ Σ i be the image of N i by the projection G → Σ i . The first projection ψ i : Σ i → G then induces an epimorphism ψi : Σi := Σi (R i , L i ) → G (see Subsection 3.2 for a definition of Σi ).

Eventually, we let Ĝ be the fibered product

Σ1 × G • • • × G Σn ∼ = G × (Gו••×G) ( Σ1 × • • • × Σn ), (3.8)
and we define a map Φ : Ĝ → G/ G′ by the formula

Φ ([s 1 ], . . . , [s n ]) = [(s 1 , . . . , s n )] , (3.9)
where s i ∈ Σ i for each i (here we see Ĝ as contained in Σ1 × • • • × Σn , using its description by the left-hand side of (3.8) rather than by its right-hand side, and similarly we see G as contained in Σ

1 × • • • × Σ n ).
It is a consequence of Lemma 3.11 that Φ is well-defined by (3.9). Now we have:

Lemma 3.12. The morphism Φ is surjective, and has finite kernel.

Proof. The surjectivity follows at once from (3.9). On the other hand, an element ([s 1 ], . . . , [s n ]) ∈ Ĝ lies in ker Φ if and only if (s 1 , . . . , s n ) ∈ G′ . This implies for i = 1, . . . , n that s i ∈ L i Σi , because G′ = N i G. We thus see that ker Φ, seen as contained in Σ1 × Notice that Ĝ has finite index in n i=1 Σi because G is finite, and therefore that T has finite index in n i=1 T i / q i (L i ) . We have a short exact sequence

• • • × Σn , is contained in L1 Σ1 × • • • × Ln Σn
1 → E 1 → Ĝ Θ| Ĝ ---→ T → 1.
(3.12)

Clearly, ker Φ ⊂ E 1 . Therefore, setting E := E 1 / ker Φ, we obtain the following commutative diagram

1 1 1 G G ker Φ = G G ker Φ G G 1 1 G G E 1 G G Ĝ Φ Θ| Ĝ G G T = G G 1 1 G G E G G G/ G′ θ G G T G G 1 1 1 1 (3.13)
where θ is the morphism induced by Θ| Ĝ which makes the diagram commutative.

We then claim that the lower row of the diagram (3.13) is the short exact sequence we are looking for: exactness follows from an easy diagram chase; the finiteness of E follows from that of E 1 ; eventually, each T i / q i (L i ) is an orbifold surface group, because q i (L i ) consists of finite order elements (see e.g. [BCGP09, Lem. 4.7]), so that T is a finite index subgroup in a product of orbifold surface groups. This concludes the proof of Proposition 3.5.

  Lemma 2.3. (i) Let x ∈ C. Then the restriction of ϕ to the stabilizer St x of x (with respect to the action of T on C) is injective.

  4) and Σ := Σ(R, L) := Σ/N (R, L). (3.5)

  3.2: the left-hand side map in (3.10) is the product of the projec-tions Σi → Σi / Li Σi ∼ = Σ i / L i Σi ,and the qi 's are induced by the second projections q i : Σ i → T i as in Lemma 3.8. We haveker Φ ⊂ L1 Σ1 × • • • × L1 Σn ⊂ ker Θ, (3.11)and ker Θ is finite by both Lemmas 3.7 and 3.8. Let us set T := Θ( Ĝ).

  and m 1 , . . . , m r are the branching indices at the branching points of the G-cover p : C → C ′ . The appropriate orbifold homomorphism ϕ is induced by the monodromy of the Galois étale G-covering p

• : C • → C ′ • induced by p, where C ′ • is the Riemann surface obtained from C ′ by removing the branch points of p, and C •

Remark 3.10. As a direct consequence of Lemma 3.9, if (g, z 1 d ℓ1 1 z -1 1 , . . . , d ℓi i , . . . , z n d ℓn n z -1 n ) ∈ N i for some i, then for any j = i, there exists (h, y 1 , . . . , y j , . . . , y

(where a hat means that the corresponding factor is omitted), such that

Proof of Lemma 3.9. Let s ∈ G be an element with non empty fixed-point set, and let us fix i ∈ {1, . . . , n}. By Lemma 2.3 (ii), s writes

, with notations as in the statement of the Lemma. Obviously, one can find h ∈ G, and

Now we claim that there exists finite sets A j ⊂ T j , j = 1, . . . , i, . . . , n, such that each element of G as in (3.7) is conjugated in G to some

Then it is clear that one can build N i as required.

To prove our claim, first note that if (g,

corresponds to an element of the fibered product G if and only if for each j = i, ϕ j (z -1 j ζ j ) belongs to the centralizer C Hj (ϕ j (d ℓj j )) of ϕ j (d ℓj j ) in H j . Second, note that if k j ∈ R j for some j = i, then (1, 1, . . . , k j , . . . , 1) ∈ G, and therefore any element (g, . . . , z j d ℓj j z -1 j , . . .) ∈ G is conjugated to (g, . . . , (k j z j )d ℓj j (k j z j ) -1 , . . .) ∈ G.

Then our claim follows from the fact that for each j = i, R j ✂ ϕ -1 j C Hj (ϕ j (d ℓj j )) has finite index.

From now on, we let N 1 , . . . , N n be as in Lemma 3.9. Lemma 3.11. For i = 1, . . . , n, if

Then ki := (1, 1, . . . , k i , . . . , 1) ∈ G, and our result follows from the equality (1, 1, . . . , d ℓi i k i d -ℓi i k -1 i , . . . , 1) = (g, z 1 d ℓ1 1 z -1 1 , . . . , d ℓi i , . . . , z n d ℓn n z -1 n ) ki (g, z 1 d ℓ1 1 z -1 1 , . . . , d ℓi i , . . . , z n d ℓn n z -1 n ) -1 k-1 i ,