Spelling suggestions: "subject:"rotação"" "subject:"lotação""
11 |
Criptografia homomórfica aplicada ao voto eletrônicoOliveira, Fábio Cristiano Souza 06 June 2014 (has links)
Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-09T12:55:09Z
No. of bitstreams: 2
Dissertação Fábio Cristiano Souza Oliveira.pdf: 2121278 bytes, checksum: 516ff0f247d542c702cb5df69410c229 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-09T12:55:09Z (GMT). No. of bitstreams: 2
Dissertação Fábio Cristiano Souza Oliveira.pdf: 2121278 bytes, checksum: 516ff0f247d542c702cb5df69410c229 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2014-06-06 / A democracia representativa depende do planejamento e da execução adequada de
uma eleição. Requisitos de segurança e restrições rigorosas são impostas na tentativa
de evitar resultados duvidosos e fraudes dos mais variados tipos. Sistemas de votação
eletrônica têm sido introduzidos visando mitigar os problemas associados aos métodos
tradicionais. No entanto, a segurança desses sistemas ainda é insuficiente,
principalmente, no que diz respeito à privacidade do eleitor e a verificabilidade fim-a-fim
do voto. Nos últimos anos, melhorias nos sistemas de votação têm sido propostas a
fim de atender a esses requisitos. Muitas propostas são baseadas nos fundamentos
matemáticos rígidos fornecidos por métodos criptográficos. Neste cenário, surge a
encriptação completamente homomórfica, o Santo Graal da criptografia moderna,
sugerida pela primeira vez em 1978 por Rivest, Adleman e Dertouzos. O principio
fundamental da criptografia homomórfica é a computação em dados encriptados. De lá
para cá, sistemas de votação foram desenvolvidos com o uso de esquemas
parcialmente homomórficos alegando favorecer a privacidade e a verificabilidade. No
entanto, em 2009 Gentry propôs o primeiro método matemático para a encriptação
completamente homomórfica trazendo novas perspectivas para aplicação desse
método criptográfico. Assim, esta pesquisa teve como objetivo analisar e categorizar
através de mapeamento sistemático, relatos de experiências e publicações científicas,
para identificar elementos de criptografia homomórfica que compõem as abordagens
de apoio à privacidade e a verificabilidade fim-a-fim do voto, bem como traçar uma
perspectiva para a encriptação completamente homomórfica no voto eletrônico. Foram
analisados 815 estudos, dos quais 13 foram selecionados e categorizados de acordo
com as questões de pesquisa. Após análise, foi possível perceber que a privacidade e
a verificabilidade do voto são fornecidas pela combinação de mecanismos
criptográficos e não criptográficos. A eficiência dos sistemas baseados em tecnologia
homomórfica é um desafio.
|
12 |
Proposta de um modelo para verificabilidade E2E no sistema eletrônico de votação brasileiro utilizando mecanismos de criptografia visualVarejão Junior, Gleudson Pinheiro 21 August 2014 (has links)
Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-09T14:26:19Z
No. of bitstreams: 2
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
DISSERTAÇÃO Gleidson Pinheiro Varejão Júnior.pdf: 5786318 bytes, checksum: db03ae4c22592a31990484cac439eb0d (MD5) / Made available in DSpace on 2015-03-09T14:26:20Z (GMT). No. of bitstreams: 2
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
DISSERTAÇÃO Gleidson Pinheiro Varejão Júnior.pdf: 5786318 bytes, checksum: db03ae4c22592a31990484cac439eb0d (MD5)
Previous issue date: 2014-08-21 / A história relata a ascensão da democracia sendo seleta a pequenos grupos
de uma população, como frequentemente ocorria em algumas nações. O Brasil é
um país democrático que tem participação da sociedade, que exerce seu direito
democrático através dos seus representantes. No entanto, evidências descritas por
Diego Aranha em (ARANHA, 2014) apontam que a maneira pela qual eles são
eleitos nem sempre atinge níveis aceitáveis de segurança e confiabilidade do
processo. Desde então os Sistemas Eletrônicos de Votação (SEV) vêm sendo
empregados em países como Holanda, Índia, Alemanha e Brasil, tendo como
principal objetivo atender aos requisitos, propriedades, regras e leis instauradas
para um sistema eleitoral, primando pela conformidade de padrões e preceitos
democráticos específicos de cada nação. No Brasil, o início do processo de
informatização das eleições ocorreu no ano de 1996, onde então foi apresentada
ao mundo a aplicabilidade de um modelo de votação 100% eletrônico, e que,
segundo autoridades responsáveis pelo processo, é apontado como seguro e
isento à fraude. Desde então muitas discussões surgiram a respeito da segurança
do mesmo. Um dos assuntos mais pautados entre profissionais e pesquisadores de
áreas afins ao sistema é a impossibilidade de se realizar um processo chamado
verificabilidade “fim-a-fim” (em inglês, “end-to-end”, abreviação E2E), que visa
prover mecanismos que possibilitam a verificação do voto por parte do eleitor,
muito em decorrência da inexistência de um mecanismo que viabilize a
materialização do voto. Levando em consideração os relatos, torna-se latente a
necessidade do vínculo entre a transparência e automação de recursos, mitigando
os riscos na ocorrência de fraudes e maximizando as possibilidades de auditoria e
recontagem dos votos. Dessa forma, a criptografia computacional vem mostrandose
uma das principais ferramentas para atender demandas de segurança em SEV.
Este trabalho visa estudar e avaliar os princípios de um SEV, bem como suas
principais tecnologias e desafios de segurança. A partir do estudo realizado, é
descrita a proposta de um modelo utilizando criptografia visual, a fim de prover
possíveis mecanismos que atendam o requisito de verificabilidade E2E com a
materialização do voto de um modo não tradicional, tendo como foco o emprego
desse esquema no Sistema Eletrônico de Votação brasileiro.
|
13 |
Três ensaios em economia política / Three essays in political economyAdalberto de Lima 14 November 2008 (has links)
Neste artigo utiliza-se a reforma constitucional brasileira de 1988 para investigar o impacto da extensão do direito de voto sobre a composição dos gastos públicos. Posterior ao processo de democratização a nova constituição estendeu o direito de voto aos analfabetos, o que representa uma mudança exógena na composição do eleitorado proporcionando uma clara estratégia de identificação. Uma vez que as taxas de analfabetismo variam consideravelmente entre os municípios, pode-se testar se políticas de gastos públicos favoráveis aos mais pobres sofreram elevações mais acentuadas nos municípios com maiores taxas iniciais de analfabetismo. Os resultados obtidos sugerem que o gasto com transferências se elevou mais acentuadamente naqueles municípios que exibiram maior percentual de eleitores analfabetos. Tudo o mais constante, uma mudança de um desvio padrão na taxa de analfabetismo está associada a uma elevação de 1,5 pontos percentuais na razão transferências/gasto total. / In the first paper, we explore Brazils 1988 Constitutional reform to investigate how a major change in the franchise affected the pattern and level of public spending. After redemocratization, the new Constitution extended the franchise to illiterate citizens previously not allowed to cast their votes. This exogenous change in the composition of the electorate is the base of our identification strategy. Since illiteracy rates varied substantially across municipalities, we are able to test whether pro-poor public expenditures increased more in municipalities with higher initial illiteracy rates. We do find that transfers rose more sharply in municipalities harboring more illiterate voters. The second paper studies the relationship between democracy and growth in a crosscountry analysis using data for years 1950-2005. Using econometric duration models to evaluate the impact of modernization hypothesis we find evidence supporting the exogenous modernization theory, in the sense that democracy has more duration in a richest and more educated country. But the duration of dictatorship isnt reduced by economic growth or rise of educational attainment. The last paper surveys the literature about the empirical comparison between directional and proximity models. We discuss the data collected process, estimation strategy and results, focusing in the post 1999 works. Theres no indication of superiority for neither of the theories, suggesting that the field is still active.
|
14 |
Economic and behavioral effects of safety net programsPinho Neto, Valdemar Rodrigues de 16 March 2018 (has links)
Submitted by VALDEMAR PINHO NETO (valdemar.pinhoneto@gmail.com) on 2018-04-10T17:49:52Z
No. of bitstreams: 1
thesis.pdf: 2845831 bytes, checksum: 3f9417a81a56993860f5189a313ae2e2 (MD5) / Approved for entry into archive by GILSON ROCHA MIRANDA (gilson.miranda@fgv.br) on 2018-04-11T19:04:16Z (GMT) No. of bitstreams: 1
thesis.pdf: 2845831 bytes, checksum: 3f9417a81a56993860f5189a313ae2e2 (MD5) / Made available in DSpace on 2018-04-12T14:57:05Z (GMT). No. of bitstreams: 1
thesis.pdf: 2845831 bytes, checksum: 3f9417a81a56993860f5189a313ae2e2 (MD5)
Previous issue date: 2018-03-16 / This thesis contains three independent but interrelated articles. Essentially, in this work, I empirically investigate the economic and behavioral effects of safety net programs. To do so, I use econometrics techniques allowing for causal inference, combined with high-quality administrative data sets. Below follows a brief description of the three articles that make up this thesis. I start by studying the behavioral effects of a large-scale Conditional Cash Transfer program, the Brazilian Bolsa Família (BF), on voting outcomes. Using a unique database on BF beneficiaries and where they vote, I explore random variation in program coverage among polling stations, a highly disaggregated level of observation with fewer than 400 registered voters. The findings indicate that the cash transfers positively affected voter turnout. I also find a positive effect on the support for the incumbent party that implemented and expanded the program. This positive effect comes from more people participating in the election but also from voters switching their choices, conditional on turnout. The electoral rewards to the incumbent candidate are mostly led by those beneficiaries who entered more recently in the program and the amount of money transferred matters for voting behavior. In the second paper, we examine the effectiveness of cash assistance targeted to disadvantaged youth. We exploit an exogenous variation in the provision of cash transfers from BF Program in Brazil to credibly identify how an additional year of exposure at the critical age of 18 impacts on educational, labor market, and economic self-sufficiency outcomes. We do not find evidence of significant effects of additional exposure to the program on educational attainment and economic self-sufficiency. However, we observe a small (but still positive) impact on school enrollment, which is mostly driven by male beneficiaries. We also find effects on formal labor supply only for men. For them, we show that one additional exposure to the program decreases the probability of working in the formal sector by 5.38 percentage points during the extra year of exposure. Five years later, this pattern reverses to an increase in participation in the formal labor force. Lastly, the third paper studies the effects of a maternity leave extension on labor market outcomes of women in Brazil, using detailed information on workers and firms in the formal labor market. Taking advantage of the exact leave taking dates and the staggered implementation of the extended leave policy across firms, our analysis compares outcomes within firms before and after the eligibility cutoff. While eligible women could have extended their leave period by 50% (from 120 to 180 days), take up only increases by 13 p.p. Also, employment effects are confined to the maternity leave extension spell, with no permanent effects on employment in the long run. Taken together, our findings indicate that this policy privileges a selected group of workers, while it is not able to retain them in the workforce.
|
15 |
Relações comerciais e alinhamento nas decisões em organizações multilaterais: um estudo dos padrões de votação na Assembleia Geral da ONU / Trade and alignment in decisions in multilateral organizations: a study of the voting patterns at the UN General AssemblyMignozzetti, Umberto Guarnier 21 March 2014 (has links)
Essa tese explora o efeito do comercio internacional sobre a proximidade dos países na Assembleia Geral da Organização das Nações Unidas. Utilizando a abordagem de variáveis instrumentais, para um banco de dados que vai de 1946 até 2012, mostramos que o aumento na interdependência comercial estaria associado à diminuição no alinhamento entre países na Assembleia Geral da Organização das Nações Unidas. Esses resultados são contra-intuitivos, pois a maior parte dos trabalhos em Economia Política Internacional demonstra que comércio está mais relacionado à cooperação que a conflito. O trabalho mostra que os resultados são robustos à diversas especificações e que eles tornam-se claros quando controlamos a possível causalidade reversa entre comércio e votações. Por fim, a discussão dos resultados enfatiza que os ganhos advindos do comércio fortalecem países na arena internacional. / This thesis explore the effect of trade interdependence over the countries alignments in the United Nations General Assembly. Using the instrumental variables approach, for a data set ranging from 1946 to 2012, we show that the more trade interdependence in time t the lower the countries alignment in t + 1. These results are counter intuitive, as most of the International Political Economy literature relates trade interdependence and cooperation positively. This work shows that this negative relation is robust to diverse specifications and becomes more consistent when the reverse causality is controlled. Finally, the discussion emphasizes that trade gains empower countries in the international arenas
|
16 |
Do people vote for education? evidence from Brazilian municipal elections / As pessoas votam em educação? evidência das eleições municipais brasileirasAssunção, Matheus de Mello de 27 September 2016 (has links)
Basic education is widely cited in the literature in economics as an essential factor to the development of a country. Moreover, by the externalities it generates, it is seen as a service whose optimal supply requires public financing or provision. In Brazil, as in other countries, basic education is constitutionally established as responsibility of states and municipalities. The demand of voters for education, however, is unknown. This paper seeks to fill this gap by estimating the impact of a change in municipal spending on basic education in the reelection chances of a mayor. For that, it uses as variation the federal transfers from the Fund for the Maintenance and Development of Fundamental Education and Valuing of Teachers (FUNDEF). In addition, it evaluates possible channels through which spending can bring political returns such as level of teacher training and infrastructure of schools. / A educação básica é largamente citada na literatura em economia como fator essencial para o desenvolvimento de um país. Além disso, pelas externalidades que gera, ela é tida como serviço cuja oferta social ótima exige financiamento ou provisão pública. No Brasil, assim como em outros países, a educação básica é constitucionalmente estabelecida como de responsabilidade de estados e municípios. A demanda dos eleitores por educação, entretanto, é pouco conhecida. Este trabalho procura preencher essa lacuna estimando o impacto de uma variação nos gastos municipais com educação básica nas chances de reeleição de um prefeito. Para isso, nós usamos como variação as transferências federais do Fundo de Manutenção e Desenvolvimento do Ensino Fundamental e de Valorização do Magistério (FUNDEF). Além disso, avalia possíveis canais pelos quais os gastos podem trazer retorno político tais como nível de formação de professores e infraestrutura das escolas
|
17 |
Sistema seguro de votação eletrônica multi-cédulas / Regivaldo Gomes Costa ; orientador, Altair Olivo SantinCosta, Regivaldo Gomes January 2008 (has links)
Dissertação (mestrado) - Pontifícia Universidade Católica do Paraná, Curitiba, 2008 / Bibliografia: f. 81-85 / Em uso desde a Grécia antiga e atualmente massificado na maioria dos países do mundo, o sistema de votação tradicional baseado em cédulas de papel possui diversos problemas associados à segurança, tais como dificuldades para evitar coerção do eleitor, ven / Being used since the old Greece, and currently seeing massive adoption in the majority of the countries in the world, the traditional ballots of paper-based voting systems has many problems related to security, such as difficulty to avoid coercion of vote
|
18 |
Framework para sistemas de votação digitalCabral, Patricia Dousseau January 2014 (has links)
Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2014. / Made available in DSpace on 2015-02-05T20:15:52Z (GMT). No. of bitstreams: 1
327879.pdf: 2388494 bytes, checksum: de15313240f2034ba2de7655be91ffbb (MD5)
Previous issue date: 2014 / Abstract : Votar é um mecanismo amplamente utilizado em tomadas de decisões, sendo comumente empregado por governos e empresas. A confiança no processo de votação é fundamental para a credibilidade do resultado. Cada vez mais eleições são conduzidas através da internet devido à sua acessibilidade e facilidade de utilização. Mas esta prática traz novos desafios, tais como a credibilidade no sistema e o risco de coerção dos votantes. Apesar disto, diversos sistemas de votação online foram e continuam sendo propostos, mas implementá-los e validá-los é uma tarefa complexa e difícil. Para facilitar o desenvolvimento e a avaliação destes sistemas, assim como a idealização de novos protocolos de votação digital, foi desenvolvido um framework orientado a objetos, que fornece a estrutura necessária a um sistema de votação, reduzindo o esforço necessário para o seu desenvolvimento. Com isto, é possível estender sistemas e protocolos de uma maneira simplificada e em um período de tempo menor, favorecendo focar nos pontos mais importantes da implementação, como a busca por vulnerabilidades, testes de diferentes cenários de utilização e possíveis ataques, permitindo encontrar pontos fracos que de outra maneira poderiam não ser notados. Para avaliar a adequação do framework, foram desenvolvidos quatro protocolos de votação digital, assim como um quarto utilizadopara mostrar a importância do framework na avaliação de protocolos.<b> / Abstract : Voting is a mechanism widely used in decision making and are commonlyemployed by governments and businesses. The confidence in the votingprocess is fundamental to the credibility of the result. Increasingly pollsare conducted over the internet due to its availability and ease of use. Butthis practice brings new challenges, such as confidence in the system, andcoercion of voters. Several online voting systems have been proposed, but implementingand evaluating them is a difficult and complex task. To facilitatethe development and evaluation of these systems, as well as the idealizationof new digital voting protocols, we developed an object-oriented frameworkthat provides the necessary structure of a voting system, reducing the effortrequired for its development. With it you can extend systems and protocolsin an easier way and in a shorter period of time, allowing focus on the mostimportant points of development, such as searching for vulnerabilities, differentusage scenarios and tests possible attacks, allowing you to find weaknessesthat might otherwise not be noticed. To assess the adequacy of theframework, four digital voting protocols were developed.
|
19 |
Comportamento eleitoral na América Latina e no BrasilSilva, Rafael da January 2016 (has links)
Tese (doutorado) - Universidade Federal de Santa Catarina, Centro de Filosofia e Ciências Humanas, Programa de Pós-Graduação em Sociologia Política, Florianópolis, 2016. / Made available in DSpace on 2016-10-19T13:22:27Z (GMT). No. of bitstreams: 1
342279.pdf: 1338322 bytes, checksum: c93837d84d88bdbed855c1b5abae67e6 (MD5)
Previous issue date: 2016 / Este trabalho, de um conjunto inicial de indagações acerca das bases da alienação eleitoral (abstenções, votos brancos e nulos) no contexto brasileiro, ampliou-se, incorporando as abstenções em perspectiva comparada entre os países presidencialistas da América Latina. Esse ajuste se deu, dentre vários motivos, pela escassez de estudos sobre esse contexto continental. Assim, para dar conta de explicar tais fenômenos, a tese se estruturou em duas partes relativamente autônomas, mas não independentes. A primeira, voltada à América Latina, incorporou países de regime presidencialista que fazem parte das pesquisas regulares do Latin American Public Opinion Project (LAPOP), cujo material empírico consiste em uma base que compila rodadas de 2004 a 2012 e outra base em nível agregado com dados dos países. As análises consistiram da interação dessas duas bases em um modelo multinível. A segunda parte focou no Brasil, estendendo as análises para os votos brancos e nulos, utilizando como material empírico o Estudo Eleitoral Brasileiro (ESEB), rodada de 2010, e dados agregados ao nível dos estados, do Tribunal Superior Eleitoral (TSE) e do Instituto Brasileiro de Geografia e Estatística (IBGE). Basicamente, utilizaram-se análises descritivas e de regressão logística. De forma geral, o estudo chegou às seguintes conclusões: no contexto latino-americano existem dinâmicas próprias que conferem singularidade aos preditores da abstenção, porém, aspectos presentes em países mais desenvolvidos também foram identificados entre os países latinos. Voltando-se para o Brasil, os votos brancos e nulos são expressões de protesto de um eleitor que detém certos recursos individuais como a escolaridade, porém é afastado da política. As abstenções no país assumem caráter estrutural e o eleitor não vê conflito em ser apoiador e estar satisfeito com a democracia, mas não participar eleitoralmente em uma situação de voto facultativo.<br> / Abstract : This coursework has started with a set of questions concerning the foundations of the electoral alienation (abstentions, blank and null votes) of the Brazilian context, and has increased with the inclusion of abstentions in a comparative perspective among the presidential countries of Latin America. This tune-up has taken place, among several reasons, due to the lack of studies about this continental context. Therefore, in order to explain these phenomena, the thesis was structured in two parts relatively autonomous, but not independent. The first part, focused on Latin America, included countries of presidential system that are part of regular surveys of the Latin American Public Opinion Project (LAPOP), whose empirical material consists of one foundation that compiles epochs from 2004 to 2012 and another one on an aggregate level with the countries? data. These analyses consisted of the interaction of these two foundations in a multilevel model. The second part focused on Brazil, extending the analyses to the blank and null votes, using as empirical material the Estudo Eleitoral Brasileiro (ESEB) (Brazilian Electoral Study), epoch of 2010, and aggregate data, at state level, from the Tribunal Superior Eleitoral (TSE) (Supreme Electoral Tribunal) and the Instituto Brasileiro de Geografia e Estatística (IBGE) (Brazilian Institute of Geography and Statistics). Basically, we used descriptive analyses and analyses of logistic regression. Overall, the study reached the following conclusions: in the Latin American context there are peculiar dynamics that give uniqueness to the abstention predictors, however, the electoral aspects found in more developed countries were also identified among Latin countries. Regarding Brazil, the blank and null votes are protest expressions of a voter who has certain individual resources like schooling, but is out of politics. Abstentions in Brazil take a structural nature and the voter sees no conflict in being supportive and being satisfied with democracy, but not engaging in electoral participation in a situation of voluntary voting.
|
20 |
Especificação e verificação de protocolos de votação em lógica linear com focusing / Specification and verification of voting protocols in focused linear logicSilva, Washington Cavalcante da 28 May 2018 (has links)
Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-02T21:58:30Z
No. of bitstreams: 1
WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-09T12:29:25Z (GMT) No. of bitstreams: 1
WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5) / Made available in DSpace on 2018-07-09T12:29:25Z (GMT). No. of bitstreams: 1
WashingtonCavalcanteDaSilva_DISSERT.pdf: 19392258 bytes, checksum: a56a3a92ea29a494f3f687951927abd8 (MD5)
Previous issue date: 2018-05-28 / A lógica linear (LL) tem se consolidado como um bom arcabouço para especificar sistemas
computacionais, uma vez que fórmulas podem ser interpretadas como recursos que podem ser
consumidos e/ou produzidos. Além disso, do ponto de vista da Teoria da Prova, a LL reconcilia
o aspecto construtivo da lógica intuicionista com a simetria da lógica clássica. Desta maneira, é
possível, de uma forma mais flexível, modelar estados de um sistema como fórmulas lógicas, e as
transições entre esses estados como etapas na construção de uma prova. No entanto, a busca por
provas, em geral, não é determinística, pois existem diferentes maneiras de se provar a mesma
proposição. Visando reduzir esse problema, um sistema de provas focado pode ser utilizado nesse
processo de busca. A grosso modo, um sistema focado considera provas em forma normal, reduzindo
assim as ocorrências de provas não essenciais que são sintaticamente diferentes, mas
equivalentes no final do processo. Neste trabalho, é apresentada a prova da completude de um
sistema focado para a LL, bem como outras propriedades essenciais desse sistema. Além disso,
o sistema focado será utilizado para especificar e verificar protocolos de votação, que definem
como deve ser escolhido um candidato, feita uma contagem de votos, e divulgado o resultado
de uma eleição. Para que isso seja possível, dois protocolos de votação serão especificados formalmente
utilizando sistemas de transição de estados, que modelam de forma natural os estados
e comportamento de tais protocolos. Junto a isso, para cada sistema, uma especificação em LL
será definida e demonstrada que é correta, ou seja, que um passo focado representa uma determinada
transição no sistema de estados modelado. Por fim, propriedades inerentes aos protocolos
de votação, como a garantia de que o resultado da eleição reflete o desejo dos eleitores, serão
apresentadas e demonstradas através de derivações no sistema focado. / Linear logic (LL) has been consolidated as a good framework for specifying computational systems,
since formulas can be interpreted as resources that can be consumed and / or produced
during a proof. From the point of view of Proof Theory, LL reconciles the constructive aspect of
intuitionistic logic with the symmetry of rules in classical logic. Hence, LL offers a more flexible
way to model states of a system as well as transitions among those states. We note that the proof
search procedure is inherently non-deterministic since there are different ways of proving the
same proposition. In order to tame this problem, focused systems have been proposed aiming at
reducing the number of choices during the proof search procedure. Roughly, a focused system
considers normal form proofs, thus eliminating the occurrences of nonessential proofs that are
syntactically different but equivalent. In this work, we present the proof of the completeness of
a focused system for LL as well as some other essential properties of this system. In addition,
we use the focused system for specifying and verifying voting protocols. Such systems define
how a candidate is chosen by tallying votes and computing the final result of an election. We
formally specify two voting protocols using transition systems, which naturally model the states
and behavior of such protocols. For each system, an encoding in LL is defined and we show that
our specification is correct: a focused step corresponds exactly to a transition in the modeled
system. Finally, we verify important properties of the voting protocols such as the fact that the
system ensures that the election result reflects the voters’ desire.
|
Page generated in 0.0733 seconds