The dissertation is divided into two main parts. The first part defines the concept of dynamic visual proof and is placed in the context of proving in mathematics as a subject of science and in mathematics as a subject taught at school. The digital component of the dissertation is a collection of 19 applets with dynamic visual proofs created in the GeoGebra program and arranged in thematic chapters in the so-called GeoGebra-Book, available on-line on geogebra.org. In the second part of the work the research focused on the use of dynamic visual proofs in secondary school mathematics lessons and their influence on fulfilment of educational objectives is described. This a qualitative research where a case study focused on the detailed study of a mathematics teacher who uses dynamic visual proofs in her class. To identify educational objectives, a revised Bloom's taxonomy was chosen.

Made available in DSpace on 2016-04-27T16:58:28Z (GMT). No. of bitstreams: 1 Fernando Tavares da Silva.pdf: 4680921 bytes, checksum: 745c13dd17b022406b1dfc18f8f102f2 (MD5) Previous issue date: 2007-10-25 / The objective of this research is to investigate the approach used in proofs and demonstrations of the logarithmic mathematical object, in a collection of textbooks adopted in the Brazilian Secondary School; as well as to conceive and apply a didactic sequence to introduce the student into the deductive mathematical thought. The research intends to answer the following questions: (1) How does the author of the textbooks approach the process of proving, regarding the subject logarithms in his work? Are the readers stimulated to find out proofs in the suggested activities? (2) Which difficulties do first grade students of the Brazilian Secondary School present during a process of proving? In order to answer the first question, we have analysed the collection Matemática for Secondary School by Luiz Roberto Dante, making use of the criteria of the National Book Catalogue for Secondary School (CNLEM). For the second question, we have used some elements of the didactic engineering methodology , making use of the types of proofs by Balacheff. The results of our analysis bring forward that the author of the collection is always concerned about presenting some kind of justification or demonstration for each element introduced. However, there are few activities that stimulate the reader to produce proofs. Regarding the didactic sequence, the research presents some difficulties observed in the process of production of proofs. Furthermore, it shows that the sequence provided the students development from empiric validations to deductive validations / O objetivo desta pesquisa é investigar a abordagem conferida a provas e demonstrações do objeto matemático logaritmo, numa coleção de livros didáticos para o Ensino Médio, bem como conceber e aplicar uma seqüência didática para introduzir o aluno da primeira série do Ensino Médio ao pensamento matemático dedutivo. A pesquisa procura responder às seguintes questões de pesquisa: (1) Como o autor de livros didáticos aborda o processo de prova em relação ao tema logaritmo na sua coleção? Os alunos leitores são estimulados a realizar provas em atividades propostas? (2) Quais dificuldades os alunos da primeira série do Ensino Médio apresentam durante um processo de produção de provas? Para responder à primeira questão analisamos a coleção Matemática do Ensino Médio de autoria de Luiz Roberto Dante utilizando para isso os critérios do Catálogo Nacional do livro para o Ensino Médio (CNLEM). Para a segunda questão, adotamos alguns elementos da metodologia engenharia didática. Empregamos para essa análise a tipologia de provas de Balacheff. Os resultados das nossas análises aduzem que o autor da coleção se preocupa em oferecer sempre algum tipo de justificativa ou demonstração para cada elemento novo apresentado. Entretanto, há poucas atividades que estimulam o leitor a produzir provas. No tocante à seqüência didática, a pesquisa aponta algumas dificuldades verificadas no processo de produção de provas e mostra que apesar disso, a seqüência permitiu um avanço por parte dos alunos de validações empíricas para as validações dedutivas

Made available in DSpace on 2016-04-27T16:58:28Z (GMT). No. of bitstreams: 1 Marcelo Eduardo Pereira.pdf: 4788851 bytes, checksum: f240246d61aa2e0ffdb09fe10593ffca (MD5) Previous issue date: 2007-10-19 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The purpose of this research is to analyze learning situations concerning argumentations and mathematical proofs combined with a computational tool and had been developed into the AprovaME project - Argumentação e Prova na Matemática Escolar (Argumentation and Proof in School Mathematics), particularly during the second phase. We are founded by researches that explore the assuming functions of proof as well as evaluate them in the school context, underneath various aspects and generality levels. Guided by the main results of this studies and the survey of proof conceptions made by the teenager students that had been accomplished during the first phase of the project, we prepared a sequence of activities intending to engage them throughout the stages of proving and to argue about the conditions of transiting between pragmatic and conceptual proofs. We search, into this context, to explore different functions proof, beyond the verification one, and to analyze the role of the Microsoft Excel tool in the students empirical work. The activities were applied in extra classes sessions for three pairs of volunteer students between 15-16 years old from a private school in Santos-SP. As result, it was verified that students interaction with the computer had dynamized the process of surveying conjectures and validating them. Also through the computer experience they were able to notice the manipulated objects properties which developed the production of justifications beyond empirical evidences. Therefore, within this proposal, the students had experienced the moments of proving and presented, by deductive reasoning, argumentations that show clearly the generality involved in the suggested tasks / A proposta deste trabalho é analisar situações de aprendizagem envolvendo argumentações e provas matemáticas, integrando uma ferramenta computacional, tendo sido desenvolvido no âmbito do projeto AProvaME Argumentação e Prova na Matemática Escolar, referindo-se, particularmente, à 2ª Fase deste projeto. Fundamentamo-nos em pesquisas que exploram as funções que uma prova pode assumir e as avaliam, no contexto escolar, sob vários aspectos e níveis de generalidade. À luz dos principais resultados desses estudos e do levantamento das concepções sobre prova de alunos adolescentes, realizado na 1a Fase do Projeto, elaboramos uma seqüência de atividades com o intuito de engajá-los nas várias etapas do processo de prova e discutir as condições de transição das provas pragmáticas para as conceituais. Buscamos, neste contexto, explorar outras funções da prova, além da função de verificação e avaliar o papel da ferramenta Microsoft Excel no trabalho empírico dos alunos. A seqüência foi aplicada, em sessões extraclasse, a três duplas de alunos de 15-16 anos de uma escola particular da cidade de Santos-SP, que participaram voluntariamente da experimentação. Como resultado, verificou-se que a interação dos alunos com o computador dinamizou o processo de produção de conjecturas e de validação experimental destas, bem como a observação de propriedades dos objetos manipulados, favorecendo a elaboração de justificativas que vão além das evidências empíricas. Assim, por meio desta abordagem, os alunos tiveram a oportunidade de vivenciar as etapas do processo de prova, apresentando, por meio de raciocínios dedutivos, argumentos que evidenciam a generalidade envolvida nas tarefas propostas

Made available in DSpace on 2016-04-27T16:58:34Z (GMT). No. of bitstreams: 1 Valdenir Francisco Duarte.pdf: 2275326 bytes, checksum: 64718a9487076854ec47a0150adb082d (MD5) Previous issue date: 2007-12-10 / This work, carried out as part of the research project AprovaME developed at the Pontifical Catholic University of São Paulo, has as its aim to verify the advances and the difficulties presented by students in the elaboration of proofs related to the properties of parallelograms. The research procedures adopted during the study drew from the theories of de Parzysz (2001) concerning formal and empirical proofs; the four dimensions involved in the construction of geometrical thinking perception, representations, construction and conception presented by Machado (1995); the representation of information from the point of view of Duval (1995); and the considerations related to logical sequences in Duval e Egret (1989). Using the methodology Didactical Engineering, a sequence of activities was designed and carried out with two groups of students. One group was composed of 8th grade Middle School students and the second of students from the first year of High School. The activity sequence was planned to involve students in, first, the construction of hypotheses and theses on the basis of empirical explorations and, in term, organise, in a deductive form, their propositions in order to elaborate proofs of various properties of parallelograms. The analysis of the students productions illustrates difficulties experienced in the process of argumentation and proof that can be grouped into three categories: difficulties related to the elaboration of proofs, difficulties associated with the acceptance of empirical arguments and difficulties linked to problems in interpreting the problems proposed. The analysis also suggested that as the activity sequence progressed, certain advances in relation to these difficulties occurred. Some students began to carry out calculations without needing to consider particular cases, others presented complete formal proofs and even those who produced incomplete proofs made use of logical reasoning in attempts to express valid arguments. In addition, a positive factor related to the activity sequence was the engagement of students in the analysis of proofs constructed by others / O presente trabalho, vinculado ao projeto AprovaME, desenvolvido na Pontifícia Universidade Católica de São Paulo, tem por objetivo verificar os avanços e as dificuldades apresentadas pelos alunos na elaboração de provas sobre as propriedades dos paralelogramos. Os procedimentos dessa pesquisa foram fundamentados nas teorias de Parzysz (2001) sobre provas formais e empíricas; Machado (1995) sobre as quatro dimensões da construção do pensamento geométrico: percepção, representação, construção e concepção; Duval (1995) sobre formas de representação de informações; Duval e Egret (1989) sobre seqüências lógicas. Usando a metodologia da Engenharia Didática, foram concebidas e aplicadas a alunos da oitava série do Ensino Fundamental e do primeiro ano do Ensino Médio, uma seqüência de atividades que visaram levá-los, de forma empírica, a construir o conceito de hipótese/tese e, de forma dedutiva, a ordenar proposições de modo a elaborar provas das propriedades dos paralelogramos. A análise das produções dos alunos mostra dificuldades no processo de argumentação e prova que podem ser agrupadas em três categorias: dificuldades ligadas à elaboração de uma prova, dificuldades oriundas da aceitação de provas empíricas e dificuldades ligadas à leitura e interpretação de enunciados. A análise também apontou que houve certos avanços nesse processo. Alunos realizaram cálculos sem o apoio empírico, outros apresentaram algumas provas formais completas, e mesmo aqueles que produziram provas incompletas mostraram um raciocínio lógico até o ponto onde elas foram feitas. Além disso, verificou-se que o fato de dois alunos poderem analisar a prova feita pela outra dupla foi um fator muito positivo na seqüência apresentada

<p>Učenje o načelima postupka je jedno od karakteristika germanske procesualistike, pod čijim uticajem postaje i neodvojivi deo domaće doktrine. U teoriji se veoma rano se za oblast prikupljanja procesnog materijala formiraju dva antipodna načela &ndash; raspravno i istražno. Prvo podrazumeva da su samo stranke ovla&scaron;ćene da unose procesni materijal, odnosno da su samo one odgovorne za to. Drugo stavlja u dužnost sudu pribavljanje procesnog materijala i prebacuje odgovornost sa stranaka na njega.</p><p>Od promena u srpskom parničnom postupku koje su usledile 2004. g. tvrdi se da je raspravno načelo afirmisano, a dono&scaron;enjem Zakona o parničnom postupku iz 2011. g. i da je promenjen koncept parničenja u smislu uloge suda. On je sada pasivan, i gotovo neodgovoran na planu prikupljanja procesnog materijala. Predmet istraživanja u disertaciji je postojanje raspravnog načela u sada&scaron;njem srpskom parničnom postupku.</p><p>Rezultati istraživanja pokazuju da se ne može govoriti o raspravnom načelu kao važećem u srpskom parničnom postupku. Takav zaključak je, pre svega, uslovljen teoretskim određenjem pojma raspravnog načela i njegovog odnosa prema sudijskoj dužnosti pitanja. Raspravno načelo zaista podrazumeva da samo stranke unose procesni materijal u postupak i da u tom pogledu imaju slobodu, odnosno odgovornost. U tom smislu njegova nužna posledica su tri instituta: teret tvrdnje, priznanje tvrdnji koje vezuje sud i subjektivni teret dokazivanja. Međutim, ukoliko uz ova tri instituta postoji i sudijska dužnost pitanja, onda se odgovornost delom prebacuje i na sud, &scaron;to dovodi do postojanja sasvim drugog načela &ndash; ublaženog raspravnog načela.</p><p>Na osnovu rečenog, promene koje su se desile napu&scaron;tanjem načela materijalne istine, i to pre svega ukidanjem ovla&scaron;ćenja suda da izvodi dokaze po službenoj dužnosti, nisu dovele do uspostave raspravnog načela. Sud i dalje ima dužnost da postavljanjem pitanja ukazuje strankama na deficite procesnog materijala; presuda na osnovu tereta tvrdnje, kao i presuđenje uprkos nepredlaganju dokaza može da usledi samo ako sud prethodno ispuni svoju dužnost. Sud je i u srpskom postupku saodgovorni subjekat postupka, i to ne proizilazi samo iz redakcije ZPP, već je takav smisao u skladu sa vrednovanjima slobode i odgovornosti stranaka, sa ciljem postupka, i na kraju sa osnovnim ljudskim procesnim pravima zagarantovanim Ustavom.</p><p>Određenje da raspravno načelo nije važeće, već da je to ublaženo raspravno, utiče na shvatanje niza instituta koji se tiču procesa formiranja činjeničnog stanja,<br />a spram toga se i svi drugi instituti koji se tiču procesa formiranja činjeničnog stanja moraju prosuđivati.</p><p>Veoma važan deo istraživanja, koji je i prethodio zauzimanju stavova, je uporednopravno istraživanje fokusirano na germanski pravni krug &ndash; Nemačku i Austriju. S obzirom da su srpsko procesno pravo i dogmatika gotovo pod isključivim germanskim uticajem, bilo je potrebno da se temeljno istraži pitanje raspravnog načela u ovim sistemima. Rezultati ovog dela su pokazali da je ideja o raspravnom načelu koje podrazumeva pasivan i neodgovoran sud davno prevladana; upravo obratno, moderan germanski model postupka podrazumeva saodgovornost suda i stranaka.</p> / <p>The doctrine of civil litigation principles is one of the key characteristics of the Germanic procedural theory. Under its influence the doctrine of the principles grew into the essential part of the Serbian theory as well. The theory has rather early developed two conflicting principles with regard to responsibility for collecting the facts and and evidence &ndash; the principle of party control of facts and means of proof (Verhandlungsmaxime) and principle of investigation by the court (Untersuchungsmaxime). First one entails that the parties only can provide facts and means of proof in litigation; court can not render its judgment upon facts or proof which are not introduced by the parties. Second one implies a duty of the court to ascertain and clarify the facts; by the same token, court has responsibility to do so.<br />It is the common opinion that principle of party control over facts and means of proof is effectuated in Serbian civil litigation since legislative changes in 2004. Moreover, after the introduction of the new Civil Procedure Act in 2011it is widely accepted that the paradigm of litigation is radically changed so the court is now rather passive and almost without any responsibility for gathering facts and means of proof. The subject matter of this doctoral thesis is the existence of principle of party control of facts and means of proof in current Serbian civil litigation.<br />The results of analysis show that the principle of party control of facts and means of proof does not exists in Serbian civil litigation. This conclusion is first of all determined by dogmatic examination of the principle&rsquo;s notion. Indeed it signifies that only parties produce facts and means of proof, and in that sense that they have disposition and, accordingly, responsibility for that. By the same token, its necessary consequence are three institutes: burden of facts, binding effect of non disputed facts and burden of production of proof. However, if these three institutes exist with the court&rsquo;s parallel duty to provide hints and feedback, then the responsibility is shifted partly to the court, which results in existence of a new principle &ndash; principle of soften party control of facts and means of proof.<br />Regarding to what is said earlier, the changes which resulted in abandoning the principle of seeking of material truth, basically abrogating the court&rsquo;s obligation to take the proofs ex offo, did not lead to the creation of principle of party control of facts and means of proof. The court still has a duty to give hints and feebacks, i. e. to suggest to the parties that they clarify or supplement their pleadings; dismissing the claim or striking defense as insufficient due to the lack of factual pleadings or production of means of proof can take place only if the court previously fulfills its duty. The court is also in Serbian civil litigation jointly responsible procedural subject. That conclusion is not warranted only by interpretation of wording of the Civil Procedure Code&rsquo;s provision, but rather and predominantly by evaluation of party autonomy and responsibility in Serbian civil procedure, purpose of a civil procedure, and last but not least, by basic procedural constitutional rights.<br />The conclusion that the principle of party control of facts and means of proof does not exist and that its place is taken by the principle of softened party control has fundamental consequences on set of institutes which refer to the process of determination of facts. In that sense all these institutes are analyzed by the virtue of existing principle of Serbian civil procedure.<br />Particularly important part of the thesis, which indeed precedes the main part, is a comparative study of the Germanic legal systems &ndash; Germany and Austria. Regarding the fact that Serbian procedural law and doctrine was and still is under almost entirely Germanic influence, it was necessary to conduct a thorough analysis of these systems. Results show that the idea of principle of party control of facts and means of proof, i. e. idea of passive and unliable court is abendoned. Directly opposite, modern Germanic procedural model is distinguished by joint responsibility of court and parties.</p>

Anonymous communications networks help to solve the real and important problem of enabling users to communicate privately over the Internet. However, by doing so, they also introduce an entirely new problem: How can service providers on the Internet---such as websites, IRC networks and mail servers---allow anonymous access while protecting themselves against abuse by misbehaving anonymous users? Recent research efforts have focused on using anonymous blacklisting systems (also known as anonymous revocation systems) to solve this problem. As opposed to revocable anonymity systems, which enable some trusted third party to deanonymize users, anonymous blacklisting systems provide a way for users to authenticate anonymously with a service provider, while enabling the service provider to revoke access from individual misbehaving anonymous users without revealing their identities. The literature contains several anonymous blacklisting systems, many of which are impractical for real-world deployment. In 2006, however, Tsang et al. proposed Nymble, which solves the anonymous blacklisting problem very efficiently using trusted third parties. Nymble has inspired a number of subsequent anonymous blacklisting systems. Some of these use fundamentally different approaches to accomplish what Nymble does without using third parties at all; so far, these proposals have all suffered from serious performance and scalability problems. Other systems build on the Nymble framework to reduce Nymble's trust assumptions while maintaining its highly efficient design. The primary contribution of this thesis is a new anonymous blacklisting system built on the Nymble framework---a nimbler version of Nymble---called Nymbler. We propose several enhancements to the Nymble framework that facilitate the construction of a scheme that minimizes trust in third parties. We then propose a new set of security and privacy properties that anonymous blacklisting systems should possess to protect: 1) users' privacy against malicious service providers and third parties (including other malicious users), and 2) service providers against abuse by malicious users. We also propose a set of performance requirements that anonymous blacklisting systems should meet to maximize their potential for real-world adoption, and formally define some optional features in the anonymous blacklisting systems literature. We then present Nymbler, which improves on existing Nymble-like systems by reducing the level of trust placed in third parties, while simultaneously providing stronger privacy guarantees and some new functionality. It avoids dependence on trusted hardware and unreasonable assumptions about non-collusion between trusted third parties. We have implemented all key components of Nymbler, and our measurements indicate that the system is highly practical. Our system solves several open problems in the anonymous blacklisting systems literature, and makes use of some new cryptographic constructions that are likely to be of independent theoretical interest.

Cette thèse est consacrée à la complexité basée sur le paradigme des preuves interactives. Les classes ainsi définies ont toutes en commun qu’un ou plusieurs prouveurs, infiniment puissants, tentent de convaincre un vérificateur, de puissance bornée, de l’appartenance d’un mot à un langage. Nous abordons ici le modèle classique, où les participants sont des machines de Turing, et le modèle quantique, où ceux-ci sont des circuits quantiques. La revue de littérature que comprend cette thèse s’adresse à un lecteur déjà familier avec la complexité et l’informatique quantique. Cette thèse présente comme résultat la caractérisation de la classe NP par une classe de preuves interactives quantiques de taille logarithmique. Les différentes classes sont présentées dans un ordre permettant d’aborder aussi facilement que possible les classes interactives. Le premier chapitre est consacré aux classes de base de la complexité ; celles-ci seront utiles pour situer les classes subséquemment présentées. Les chapitres deux et trois présentent respectivement les classes à un et à plusieurs prouveurs. La présentation du résultat ci-haut mentionné est l’objet du chapitre quatre. / This thesis is devoted to complexity theory based on the interactive proof paradigm. All classes defined in this way involve one or many infinitely powerful provers attempting to convince a verifier of limited power that a string belongs to a certain language. We will consider the classical model, in which the various participants are Turing machines, as well as the quantum model, in which they are quantum circuits. The literature review included in this thesis assume that the reader is familiar with the basics of complexity theory and quantum computing. This thesis presents the original result that the class NP can be characterized by a class of quantum interactive proofs of logarithmic size. The various classes are presented in an order that facilitates the treatment of interactive classes. The first chapter is devoted to the basic complexity classes; these will be useful points of comparison for classes presented subsequently. Chapters two and three respectively present classes with one and many provers. The presentation of the result mentioned above is the object of chapter four.

Anonymous communications networks help to solve the real and important problem of enabling users to communicate privately over the Internet. However, by doing so, they also introduce an entirely new problem: How can service providers on the Internet---such as websites, IRC networks and mail servers---allow anonymous access while protecting themselves against abuse by misbehaving anonymous users? Recent research efforts have focused on using anonymous blacklisting systems (also known as anonymous revocation systems) to solve this problem. As opposed to revocable anonymity systems, which enable some trusted third party to deanonymize users, anonymous blacklisting systems provide a way for users to authenticate anonymously with a service provider, while enabling the service provider to revoke access from individual misbehaving anonymous users without revealing their identities. The literature contains several anonymous blacklisting systems, many of which are impractical for real-world deployment. In 2006, however, Tsang et al. proposed Nymble, which solves the anonymous blacklisting problem very efficiently using trusted third parties. Nymble has inspired a number of subsequent anonymous blacklisting systems. Some of these use fundamentally different approaches to accomplish what Nymble does without using third parties at all; so far, these proposals have all suffered from serious performance and scalability problems. Other systems build on the Nymble framework to reduce Nymble's trust assumptions while maintaining its highly efficient design. The primary contribution of this thesis is a new anonymous blacklisting system built on the Nymble framework---a nimbler version of Nymble---called Nymbler. We propose several enhancements to the Nymble framework that facilitate the construction of a scheme that minimizes trust in third parties. We then propose a new set of security and privacy properties that anonymous blacklisting systems should possess to protect: 1) users' privacy against malicious service providers and third parties (including other malicious users), and 2) service providers against abuse by malicious users. We also propose a set of performance requirements that anonymous blacklisting systems should meet to maximize their potential for real-world adoption, and formally define some optional features in the anonymous blacklisting systems literature. We then present Nymbler, which improves on existing Nymble-like systems by reducing the level of trust placed in third parties, while simultaneously providing stronger privacy guarantees and some new functionality. It avoids dependence on trusted hardware and unreasonable assumptions about non-collusion between trusted third parties. We have implemented all key components of Nymbler, and our measurements indicate that the system is highly practical. Our system solves several open problems in the anonymous blacklisting systems literature, and makes use of some new cryptographic constructions that are likely to be of independent theoretical interest.

Les langages synchrones sont apparus autour des années quatre-vingt, en réponse à un besoin d’avoir un modèle mathématique simple pour implémenter des systèmes temps réel critiques. Dans ce modèle, le temps est découpé en instants discrets durant lesquels tous les composants du système reçoivent et produisent une donnée. Cette modélisation permet des raisonnements beaucoup plus simples en évitant de devoir prendre en compte le temps de calcul de chaque opération. Dans le monde du logiciel critique, la fiabilité du matériel et de son fonctionnement sont primordiaux, et on accepte d’être plus lent si on devient plus sûr. Afin d’augmenter cette fiabilité, plutôt que de concevoir manuellement tout le système, on utilise des machines qui synthétisent automatiquement le système souhaité à partir d’une description la plus concise possible. Dans le cas du logiciel, ce mécanisme s’appelle la compilation, et évite des erreurs introduites par l’homme par inadvertance. Elle ne garantit cependant pas la bonne correspondance entre le système produit et la description donnée. Des travaux récents menés par une équipe INRIA dirigée par Xavier Leroy ont abouti en 2008 au compilateur CompCert d’un sous-ensemble large de C vers l’assembleur PowerPC pour lequel il a été prouvé dans l’assistant de preuve Coq que le code assembleur produit correspond bien à la description en C du programme source. Un tel compilateur offre des garanties fortes de bonne correspondance entre le système synthétisé et la description donnée. De plus, avec les compilateurs utilisés pour le temps réel critique, la plupart des optimisations sont désactivées afin d’éviter les erreurs qui y sont liées. Dans CompCert, des optimisations elles aussi prouvées sont proposées, ce qui pourrait permettre ces passes dans la production de systèmes temps réel critiques sans en compromettre la fiabilité. Le but de cette thèse est d’avoir une approche similaire mais spécifique à un langage synchrone, donc plus approprié à la description de systèmes temps réel critiques que ne l’est le C. Un langage synchrone flots de données semblable à Lustre, nommé Ls, et un langage impératif semblable au langage C, nommé Obc y sont proposés ainsi que leur sémantique formelle et une chaîne de compilation avec des preuves de préservation de sémantique le long de cette chaîne. / Synchronous languages first appeared during the 80’s, in order to provide a mathematical model for safety-critical systems. In this model, time is discrete. At each instant, all components of the system simultaneously receive and produce some data. This model allows simpler reasonning on the behaviour of the system, as it does not involve the time required for each of the operations for every component. In safety-critical systems, safety is the rule, so a poor performance behaviour can be allowed if it improves safety. In order to improve safety, rather than conceiving directly the system, machines are used to automatically design the system from a given concise description. In the case of software, this machine is called a compiler, and avoids issues due to some human inadvertence. But it does not ensure that the produced system and the description specification really show the same behaviour. Some recent work from an INRIA team lead by Xavier Leroy achieved in 2008 the realisation of the CompCert compiler from a large subset of C to PowerPC assembly, for which it was proven inside of the Coq proof assistant that the produced system fits its source description. Such a compiler offers strong guarantees that the produced system and its given description by the programmer really fit. Furthermore, most current compiler’s optimizations are disabled when dealing with safety-critical systems in order to avoid tedious compilation errors that optimizations may introduce. Proofs for optimizations may allow their use in this domain without affecting the faith we could place in the compiler. The aim of this thesis is to follow a similar path, but this one on a language which would be more suited for safety-critical systems than the C programming language. Some dataflow synchronous programming language very similar to Lustre, called Ls is described with its formal semantics, as well as an imperative programming language similar to a subset of C called Obc. Furthermore some compilation process is described as well as some proofs that the semantics is preserved during the compilation process.

Dans cette thèse, nous étudions les constructions cryptographiques prouvées pour la protection de la vie privée. Pour cela nous nous sommes intéressés aux preuves et arguments à divulgation nulles de connaissance et leurs applications. Un exemple de ces constructions est la signature de groupe. Ce protocole a pour but de permettre à un utilisateur de s'authentifier comme appartenant à un groupe, sans révéler son identité. Afin que les utilisateurs restent responsable de leurs agissements, une autorité indépendante est capable de lever l'anonymat d'un utilisateur en cas de litige. Une telle construction peut ainsi être utilisée, par exemple, dans les systèmes de transport en commun. Un utilisateur qui rentre dans un bus prouve ainsi son appartenance aux utilisateurs possédant un abonnement valide, sans révéler qui il est, et évitant ainsi que la société de transport ne le trace. En revanche, en cas d'incident sur le réseau, la société peut faire appel à la police pour lever l'anonymat des usagers présents au moment de l'incident. Nous avons proposé deux constructions de ces signatures de groupe, prouvées sûres sous des hypothèses simples dans le monde des couplages et des réseaux euclidiens. Dans la continuité de ces travaux, nous avons aussi proposé la première construction de chiffrement de groupe (l'équivalent de la signature de groupe pour le chiffrement) à base de réseaux euclidiens. Finalement, ces travaux nous ont amené à la construction d'un schéma de transfert inconscient adaptatif avec contrôle d'accès à base de réseaux euclidiens. Ces constructions à base de réseaux ont été rendues possibles par des améliorations successives de l'expressivité du protocole de Stern, qui reposait initialement sur la difficulté du problème du décodage de syndrome. / In this thesis, we study provably secure privacy-preserving cryptographic constructions.We focus on zero-knowledge proofs and their applications.Group signatures are an example of such constructions.This primitive allows users to sign messages on behalf of a group (which they formerly joined), while remaining anonymous inside this group.Additionally, users remain accountable for their actions as another independent authority, a judge, is empowered with a secret information to lift the anonymity of any given signature.This construction has applications in anonymous access control, such as public transportations.Whenever someone enters a public transportation, he signs a timestamp. Doing this proves that he belongs to the group of people with a valid subscription.In case of problem, the transportation company hands the record of suspicious signatures to the police, which is able to un-anonymize them.We propose two constructions of group signatures for dynamically growing groups. The first is based on pairing-related assumptions and is fairly practical. The second construction is proven secure under lattice assumptions for the sake of not putting all eggs in the same basket.Following the same spirit, we also propose two constructions for privacy-preserving cryptography.The first one is a group encryption scheme, which is the encryption analogue of group signatures. Here, the goal is to hide the recipient of a ciphertext who belongs to a group, while proving some properties on the message, like the absence of malwares. The second is an adaptive oblivious transfer protocol, which allows a user to anonymously query an encrypted database, while keeping the unrequested messages hidden.These constructions were made possible through a series of work improving the expressiveness of Stern's protocol, which was originally based on the syndrome decoding problem.