[pt] Ao descrever-se a prova de um teorema, é fundamental que haja cautela para que esta não contenha erros ou inconsistências. Para provas muito longas, no entanto, a detecção de erros pode tornar-se uma tarefa humanamente inviável. Um assistente de provas é um programa cuja finalidade é realizar esta detecção de erros para um usuário de forma eficiente, bem como facilitar a construção e compreensão de provas complexas a partir de outras já existentes. O Lean Theorem Prover, desenvolvido em 2012 por Leonardo de Moura, é um assistente de provas que trabalha com descrição de provas através de uma linguagem computacional compilável. Propomos aqui uma descrição no Lean Theorem Prover das provas de funcionamento de diversos algoritmos pertinentes à área de criptografia. / [en] When describing a proof of a theorem, one must be cautious to ensure said proof does not contain errors or inconsistencies. For very long proofs, however, error detection can become humanly infeasible. A proof assistant is a program whose purpose is to perform said error detection efficiently, as well as to assist in the creation and comprehension of complex proofs out of simpler, existing proofs. The Lean Theorem Prover, developed in 2012 by Leonardo de Moura, is a proof assistant which functions via description of proofs in a compilable computer language. We present a description of proofs of correctness of various algorithms pertaining to cryptography in the Lean Theorem Prover.

[pt] Apesar da alta sensibilidade alcançada por Fotodetectores comercialmente disponíveis, a implementação de circuitos de gerenciamento é capaz de fortalecer a robustez das medidas, criando um aparato com mais recursos em aplicações específicas. Duas aplicações práticas dessa hipótese são apresentadas em contextos diferentes, Criptografia Quântica e Monitoramento de Fibras Ópticas fazendo uso da plataforma FPGA. / [en] Despite the high sensitivity reached by Photon Detectors so far, the implementation of a background managing system often enforces the robustness of measurements thus creating a resourceful apparatus for specific applications. In this document, the management tools offered by Software Defined Hardware (SDHs) is put to test. By associating the power of FPGAs and Photon Detectors, enhanced measurement stations were assembled. Two different applications, a Bell State Projection Analysis Station and a Photon Counting Optical Time Domain Reflectometry (v-OTDR)Automatic Setup, are presented. Even though both experiments involve the detection of single photons, the background technologies differ drastically.

[pt] Normalmente, aplicações semânticas utilizam o conceito de linked data, onde é possível obter dados de diversas fontes e em múltiplos formatos. Desta forma, as aplicações semânticas processam muito mais dados do que as aplicações tradicionais. Uma vez que nem todas as informações são públicas, alguma forma de autenticação será imposta ao usuário. Consultar dados de múltiplas fontes pode requerer muitos pedidos de autenticação, normalmente através de uma combinação de conta de usuário e senha. Tais operações consomem tempo e, considerando-se o tempo extra que uma aplicação semântica leva para processar os dados coletados, pode tornar a experiência frustrante e incômoda para os usuários, devendo ser minimizado, sempre que possível. O propósito desta dissertação é o de analisar e comparar as técnicas de autenticação disponíveis para as aplicações semânticas e propor um protocolo mais rápido e mais seguro para autenticação em aplicações semânticas. / [en] Usually, Linked Data makes Semantic Web Applications query much more information for processing than traditional Web applications. Since not all information is public, some form of authentication may be imposed on the user. Querying data from multiple data sources might require many authentication prompts. Such time consuming operations, added to the extra amount of time a Semantic Web application needs to process the data it collects might be frustrating to the users and should be minimized. The purpose of this thesis is to analyze and compare several Semantic Web authentication techniques available, leading to the proposal of a faster and more secure authentication protocol for Semantic Web Applications.

[pt] A criptografia quântica se apresenta como uma área relativamente nova e interdisciplinar que, fundamentada nas leis da mecânica quântica, promete solucionar o grande desafio da criptografia simétrica clássica atual, a distribuição de chaves. A distribuição quântica de chaves provê comunicação absolutamente segura entre duas partes, possibilitando o compartilhamento de um segredo, que será utilizado na posterior encriptação da mensagem. Esta dissertação relata a implementação física experimental de um sistema óptico de distribuição quântica de chaves com codificação em freqüência por dupla-modulação em amplitude e fase e sincronização por multiplexação no domínio do comprimento de onda. São introduzidos os conceitos teóricos básicos necessários ao desenvolvimento do tema e apresentadas medições de caracterização dos principais componentes do sistema, bem como resultados de medidas sistêmicas clássicas e quânticas. / [en] The quantum cryptography rises as a relatively new and interdisciplinary area that, grounded in the quantum mechanics laws, promises to solve the major challenge in the actual symmetric classical cryptography, the key distribution. The quantum key distribution enables absolutely secure communication between two parts, making them able to share a secret that will be used in the posterior message encryptation. This dissertation reports the experimental physical implementation of an optical quantum key distribution system with frequency coding by amplitude and phase double-modulation process and wavelengthdivision multiplexing synchronization. The mean theoretical foundations are briefly introduced and the characterization measurements of the most important devices are shown, as like results from systemic classical and quantum measurements.

[pt] Essa dissertação se propõe a introduzir nas aulas de matemática da escola básica um tema que traga significado e interesse ao alunado e que, a partir dele, seja possível desenvolver conteúdos novos e clássicos da disciplina, pertinentes a esse nível de escolaridade. O tema escolhido foi a criptografia que possibilitou o desenvolvimento de uma abordagem histórica da sua evolução até o código RSA, a promoção de discussões sobre a relevância atual do assunto até os nossos dias e o trabalho com conteúdos importantes da matemática. Com o intuito de aprimorar e avaliar a proposta, uma pequena aplicação numa escola pública foi feita, através de uma oficina, com resultados bastante satisfatórios. Pretende-se que este trabalho seja mais uma fonte para auxiliar diversos professores na construção de novas propostas pedagógicas adaptadas à realidade de cada sala de aula com olhar motivador, significativo e contemporâneo. / [en] This dissertation proposes to introduce in the math class of the elementary school a theme that brings meaning and interest to the students and, from it, it is possible to develop new and classic content, relevant discipline at this level of education. The theme chosen was the encryption that made possible the development of a historical approach of its development until the RSA code, the promotion of discussions on the current relevance of the subject until our days and working with important content of mathematics. In order to improve and evaluate the proposal, a small application in a public school was made, through a workshop, with results quite satisfactory. It is intended that this work is more a source to assist several teachers in the construction of new pedagogical proposals adapted to the reality of each classroom with motivating, meaningful and contemporary look.

[pt] No futuro próximo, viveremos em cidades inteligentes. Nossas casas, nossos carros e a maioria dos nossos equipamentos estarão interconectados. Se a infraestrutura das cidades inteligentes não fornecerem privacidade e segurança, os cidadãos ficarão relutantes em participar e as principais vantagens de uma cidade inteligente irão se dissolver. Vários algoritmos de criptografia recentemente foram quebrados ou enfraquecidos e os comprimentos das chaves estão aumentando, conforme cresce o poder computacional. Um estudo recente descobriu que 93 porcento de 20.000 aplicações Android tinham violado uma ou mais regras de criptografia. Essas violações enfraquecem a criptografia ou as inutiliza. Outro problema é a autenticação. Uma chave privada comprometida de única autoridade de certificação intermediária pode comprometer toda cidade inteligente que utilizar certificados digitais para autenticação. Neste trabalho, investigamos por que tais violações ocorrem. Propomos o HX: um algoritmo de criptografia modular baseado em funções de hash resistentes à colisão que reduz automaticamente as violações de regras de criptografia e o HXAuth: um protocolo de autenticação de chave simétrica para trabalhar em conjunto com o SRAP ou independentemente, com um segredo previamente partilhado. Nossos experimentos apontam na direção de que a maioria dos desenvolvedores não tem o conhecimento básico necessário em criptografia para utilizar corretamente um algoritmo de criptografia. Nossos experimentos também provam que o HX é seguro, modular e é mais forte, mais eficaz e mais eficiente do que o AES, o Salsa20 e o HC-256. / [en] In the near future, we will live in smart cities. Our house, our car and most of our appliances will be interconnected. If the infrastructure of the smart cities fails to provide privacy and security, citizens will be reluctant to participate and the main advantages of a smart city will dissolve. Several encryption algorithms have been broken recently or significantly weakened and key lengths are increasing as computing power availability grows. In addition to the ever growing computing power a recent study discovered that 93 percent from 20,000 Android applications had violated one or more cryptographic rules. Those violations either weaken the encryption or render them useless. Another problem is authentication. A single compromised private key from any intermediate certificate authority can compromise every smart city which will use digital certificates for authentication. In this work, we investigate why such violations occur and we propose: HX, a modular encryption algorithm based on Collision Resistant Hash Functions that automatically mitigates cryptographic rules violations and HXAuth, a symmetric key authentication protocol to work in tandem with Secure RDF Authentication Protocol (SRAP) or independently with a pre-shared secret. Our experiments points in the direction that most developers do not have the necessary background in cryptography to correctly use encryption algorithms, even those who believed they had. Our experiments also prove HX is safe, modular and is stronger, more effective and more efficient than AES, Salsa20 and HC-256.

[pt] A criptografia quântica foi proposta como uma solução para o problema da distribuição de chaves criptográficas com segurança total garantida pelos princípios da mecânica quântica. Através dessa técnica é possível saber se um espião tentou interceptar a transmissão, o que é impossível utilizando técnicas de transmissão clássicas. Nesse trabalho foi feito um breve resumo da teoria de criptografia quântica, de suas técnicas de transmissão e dos problemas tecnológicos enfrentados. Foi analisada em detalhes a técnica de transmissão de qubits utilizando codificação de freqüência e feita uma comparação dos diferentes esquemas de modulação frente aos protocolos BB84 e B92. Foi demonstrado que os dois esquemas de modulação existentes (AM-AM e PM-PM) são na realidade equivalentes e foi proposto um novo esquema, o AM-PM o único que suporta o protocolo BB84 clássico. Medidas foram realizadas classicamente nos formatos AM-AM e AM-PM. / [en] Quantum cryptography has been proposed as a solution to the cryptographic key distribution problem with absolute security guaranteed by the principles of quantum mechanics. Through this scheme it is possible to find out whether a spy tried to eavesdrop on the transmission, which was impossible to discover using classical transmission techniques. In this work a brief review of quantum cryptography theory, transmission techniques and technological problems involved were performed. It was analyzed in detail the transmission technique employing frequency coding, and a comparison was made between the different modulation schemes and the BB84 and B92 protocols. It was demonstrated that the two existing modulation formats (AM-AM and PM-PM) are in fact equivalent and a new format (AM-PM) was proposed, the only one able to accommodate classical BB84. Classical measurements were performed on the AM-AM and AMPM formats.

[pt] A importância da Internet das Coisas (IoT) tem aumentado significativamente nos últimos anos, e dispositivos IoT têm sido usados em diferentes indústrias e tipos de aplicação, como casas inteligentes, sensores indutriais, veículos autonomos, wearables, etc. Apesar deste cenário trazer inovações tecnológicas, novas experiências para usuários, e novas soluções de negócio, também levanta preocupações relevantes relacionadas a segurança da informação e privacidade. Neste trabalho nós apresentamos o EdgeSec Framework, um novo framework de segurança para IoT desenvolvido como uma solução de segurança para os middlewares ContextNet e Mobile-Hub. O seu objetivo principal é estender e melhorar uma arquitetura e uma implementação já existentes para estes middlewares, criando uma solução mais genérica, robusta e flexível,e garantindo autenticação, autorização, integridade e confidencialidade de dados. O framework foi elaborado com foco na total extensiblidade através da introdução de interfaces de protocolos, que podem ser implementadas por plugins, tornando-o compatível com uma variedade de algoritmos de segurança e dispositivos IoT. Uma implementação completa foi realizada como prova de conceito, e testes de desempenho e experimentos foram realizados para avaliar a viabilidade da solução. Os resultados mostram que o EdgeSec Framework pode melhorar significativamente a segurança do Mobile-Hub e diversos tipos de aplicações IoT através de uma maior compatibilidade e flexibilidade, e garantindo todas as proteções básicas de segurança. / [en] The importance of the Internet of Things (IoT) has increased significantly in recent years, and IoT devices are being used in many different industries and types of applications, such as smart homes, industrial sensors, autonomous vehicles, personal wearables, and more. While this brings technology innovation, new user experiences, and new business solutions, it also raises important concerns related to information security and privacy. In this work we present EdgeSec Framework, a new IoT security framework, made concrete as a security solution for ContextNet and Mobile-Hub middlewares. Its main goal is to extend and improve on an existing security architecture and implementation, creating a more generic, robust, and flexible solution that ensures authentication, authorization, data integrity and confidentiality. The framework was designed with full extensibility in mind by introducing protocol interfaces that can be implemented by external plugins, making it compatible to a variety of security algorithms and edge devices. A complete implementation was developed as proof-of-concept, and performance tests and experiments were made to evaluate the feasibility of the solution. Results show that EdgeSec framework can greatly improve the security of Mobile-Hub and similar IoT middlewares by increasing its compatibility and flexibility, and ensuring all the basic security protections.

[pt] Dois dispositivos de contagem de fótons únicos, sensíveis a comprimentos de onda no infravermelho próximo e médio, são propostos e experimentalmente investigados. Ambos utilizam uma técnica de dois estágios, composta de uma etapa inicial de conversão de freqüências em um cristal não-linear seguida de detecção por um fotodiodo avalanche de silício. Enquanto o primeiro projeto é voltado à detecção de fótons únicos a 1.55 μm para comunicações quânticas via fibra óptica, usando um processo intra-cavidade, o segundo projeto prevê o desenvolvimento de um contador de fótons operando a 4.65 μm para sistemas de espaço livre. Neste caso, um estudo de viabilidade para um sistema prático de criptografia quântica operando em um comprimento de onda no infravermelho médio é realizado. Os resultados mostram que, usando a tecnologia disponível na atualidade, tal sistema pode ser construído, embora sua utilidade se mostre restrita a enlaces possuindo certas condições meteorológicas específicas. / [en] Two single photon counting devices, operating at near- and mid-infrared wavelengths, are introduced and experimentally investigated. Both use a twostage technique, comprised of an initial frequency up-conversion procedure inside a nonlinear crystal followed by a silicon avalanche photodiode. Whereas the first project consists on detection of single photons at 1.55 ìm for fiber-optic-based quantum communications, using a cavity-enhanced procedure, the second project envisions the development of a single-photon counter operating at 4.65 ìm for free-space systems. In this case, a feasibility study for a practical quantum key distribution system operating in a mid-infrared wavelength is performed. The results show that, using present-day technology, such a system can be constructed, albeit its usefulness would be restricted to operation under very specific weather conditions.

[pt] Este trabalho apresenta o estudo de comunicação óptica quântica no infravermelho, utilizando um sistema híbrido fibra-óptica – espaço-livre, como prova de princípio para o estabelecimento de chaves secretas a fim de utilização em criptografia do tipo one-time pad. Ao modular a polarização da luz de um laser em polarizações ortogonais, podem-se codificar os bits clássicos 1 e 0 em cada uma dessas polarizações, sendo detectadas por detectores contadores de fótons únicos, e, assim, utilizar o canal quântico para transmissão dos bits quânticos entre dois interlocutores, utilizandoos para o estabelecimento da chave criptográfica, que pode ser usada em qualquer tipo de informação a ser transmitida por um canal clássico ou quântico. Ao realizar a transmissão em espaço-livre, sujeita a variações climáticas, como temperatura atmosférica, luz solar, presença de nuvens, chuva e vento, foi também estudada a influência destes fenômenos na qualidade da transmissão e dos dados obtidos. Os resultados experimentais demonstraram consistência com a teoria e com outros trabalhos publicados na área até esta data com relação às taxas de erro de bit quântico e também à taxa de transmissão de bits. As taxas de erro obtidas, por estarem abaixo do limiar teórico para segurança da informação em comunicação quântica, provam, ainda, a possibilidade de estabelecimento de chave secreta para criptografia através do uso de distribuição quântica das chaves (QKD). Os resultados também apresentaram boa qualidade da informação recuperada após a descriptografia. / [en] This work presents the study of optical quantum communication in the infrared region, using a hybrid optical-fiber – free-space system, as proof of principle for the agreement on secret keys by two parties for use in one-time pad encryption. By modulating the polarization of laser light into orthogonal polarizations, one can encode the classic bits 1 and 0 in each of these polarizations, being detected by single photon counter detectors, and can use the quantum channel to transmit the quantum bits between two interlocutors. It is then possible to use those bits to establish the cryptographic key, which can be used in any type of information to be transmitted by a classic or quantum channel. While carrying out transmission in free space optics, subject to climatic variations, such as atmospheric temperature, sunlight, presence of clouds and rain, and the presence of wind, the influence of these phenomena on the quality of transmission and on the data obtained was also studied. The experimental results showed consistency with the theory and with other works published to date with regard to quantum bit error rates and to the bit rate. The error rates obtained, being below the theoretical threshold for information security in quantum communication, further proves the possibility of establishing a secret key for encryption through the use of quantum key distribution (QKD). It also presented good quality on the information recovered after decryption.