This master’s thesis focuses on the possibility of using contactless smart cards as an electronic hiding place in an activity known as Geocaching. The first part explains the theoretical knowledge about cards, smart card programming, the development of android applications for communication with the smart card using the NFC interface and usage of eliptic curves to sign digital messages. The second part is dedicated to the design of a Java card application and an Android application, which are able to communicate

Master's thesis analyses modern hash functions. The requirements for these features and briefly outlined some of the types of attacks are given in the first part. The second part focuses on the specication Skein hash function, which is among the candidates for the new SHA-3 standard, and a description of the JCOP platform, which is a function implemented. In the last part of the work there are discussed implementation problematic parts and evaluation of the selected solution.

Made available in DSpace on 2014-12-17T15:46:59Z (GMT). No. of bitstreams: 1 BrunoEGG_TESE.pdf: 2215931 bytes, checksum: 5d86c012a04f884e6dec73c92c1d88ef (MD5) Previous issue date: 2012-06-01 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications. / As aplica??es para smart cards representam um mercado que cresce a cada ano. Normalmente, essas aplica??es manipulam e armazenam informa??es que requerem garantias de seguran?a, tais como valores monet?rios ou informa??es confidenciais. A qualidade e a seguran?a do software para cart?es inteligentes pode ser aprimorada atrav?s de um processo de desenvolvimento rigoroso que empregue t?cnicas formais da engenharia de software. Neste trabalho propomos o m?todo BSmart, uma especializa??o do m?todo formal B dedicada ao desenvolvimento de aplica??es para smart cards na linguagem Java Card. O m?todo descreve, em um conjunto de etapas, como uma aplica??o smart card pode ser gerada a partir de refinamentos em sua especifica??o formal. O desenvolvimento ? suportado por um conjunto de ferramentas, automatizando a gera??o de parte dos refinamentos e a tradu??o para as aplica??es Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especifica??o e refinamento descrito no m?todo foi formalizado e verificado utilizando o pr?prio m?todo B, com o aux?lio da ferramenta Atelier B [Cle12a]. Destaca-se que a aplica??o Java Card ? traduzida a partir do ?ltimo passo de refinamento, denominado de implementa??o. A especifica??o dessa tradu??o foi feita na linguagem ASF+SDF [BKV08]. Inicialmente, descreveu-se as gram?ticas das linguagens B e Java (SDF) e, em uma etapa posterior, especificou-se as transforma??es de B para Java Card atrav?s de regras de reescrita de termos (ASF). Essa abordagem foi um importante aux?lio durante o processo de tradu??o, al?m de servir ao prop?sito de document?lo. Cumpre destacar a biblioteca KitSmart [Dut06, San12], componente essencial ao m?todo BSmart, que inclui modelos em B de todas as 93 classes/interfaces da API Java Card na vers?o 2:2:2, dos tipos de dados Java e Java Card e de m?quinas que podem ser ?teis ao especificador, mas que n?o est?o presentes na API padr?o. Tendo em vista validar o m?todo, seu conjunto de ferramentas e a biblioteca KitSmart, procedeu-se com o desenvolvimento, seguindo o m?todo BSmart, de uma aplica??o de passaporte eletr?nico. Os resultados alcan?ados neste trabalho contribuem para o desenvolvimento smart card, na medida em que possibilitam a gera??o de aplica??es Java Card completas (cliente e servidor) e menos sujeitas a falhas.

La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études. / Verification of the resistance of attacks against embedded implementations of the Java Card bytecode verifiers is a complex task. Current methods are not sufficient, only the generation of manual testing is possible. To automate this process, we propose a method called VTG (Vulnerability Test Generation). Based on a formal representation of the functional behavior of the system under test, a set of intrusion test is generated. This method is based on techniques of mutation and model-based testing. Initially, the model is transferred according to rules that we have defined to represent potential attacks. The tests are then extracted from the mutant models. Two Event-B models have been proposed. The first represents the structural constraints of the Java Card application files. The VTG allows in seconds to generate hundreds of abstract tests. The second model is composed of 66 events to represent 61 Java Card instructions. The mutation is effected in a few seconds. Extraction tests to generate 223 test 45 min. Each test checks a precondition or a combination of preconditions of a statement. This method allowed us to test different implementations of mechanisms through Java Card bytecode verifier. Although developed for our case study, the proposed method is generic and has been applied to other case studies.

The thesis is focused on implementation of aplication for secure telephone communication on data network. Application is developed for operating system Android. For call management is responsible signaling protocol SIP and for transfer of voice data is used protocol RTP. For security of call is first created cryptografic key for symetric cryptography. After generating key is established call, which is encrypted by symetric cipher AES. Encrypting between communicating sides is provided in application or on microSD card. Part of solution is measurement of speed of cryptographic primitives, which are used for secure call.

Smart cards are widely used in different areas of modern life including identification, banking, and transportation cards. Some types of cards are able to store data and process information as well. A number of them can run cryptographic algorithms to enhance the security of their transactions and it is usually believed that the information and values stored in them are completely safe. However, this is generally not the case due to the threat of the side channel. Side channel analysis is the process of obtaining additional information from the internal activity of a physical device beyond that allowed by its specifications. There exist different techniques to attempt to obtain information from a cryptosystem using other ways than the normally permitted. This thesis presents a series of experiments intended to study the side channel from a particular type of smart card, known as Java Cards. This investigation uses the well known technique, Correlation Analysis, and a new type of side channel attack called fast correlation in the frequency domain to study the side channel of Java Cards. This research presents a giant magnetoresistor (GMR) probe and for the first time, this type of sensor is used to investigate the side channel. A novel setup designed for studying the side channel of smart cards is described and two metrics used to evaluate the analysis results are presented. After testing the GMR probe and methodology on electronic devices executing the Advanced Encryption Standard (AES), such as 8 bit microcontrollers and 128 bit AES implementations on FPGAs, these techniques were applied to analyse two different models of Java Cards working in the contactless mode. The results show that successful attacks on a software implementation of AES running on both models of Java Cards are possible.

Smart cards are widely used in different areas of modern life including identification, banking, and transportation cards. Some types of cards are able to store data and process information as well. A number of them can run cryptographic algorithms to enhance the security of their transactions and it is usually believed that the information and values stored in them are completely safe. However, this is generally not the case due to the threat of the side channel. Side channel analysis is the process of obtaining additional information from the internal activity of a physical device beyond that allowed by its specifications. There exist different techniques to attempt to obtain information from a cryptosystem using other ways than the normally permitted. This thesis presents a series of experiments intended to study the side channel from a particular type of smart card, known as Java Cards. This investigation uses the well known technique, Correlation Analysis, and a new type of side channel attack called fast correlation in the frequency domain to study the side channel of Java Cards. This research presents a giant magnetoresistor (GMR) probe and for the first time, this type of sensor is used to investigate the side channel. A novel setup designed for studying the side channel of smart cards is described and two metrics used to evaluate the analysis results are presented. After testing the GMR probe and methodology on electronic devices executing the Advanced Encryption Standard (AES), such as 8 bit microcontrollers and 128 bit AES implementations on FPGAs, these techniques were applied to analyse two different models of Java Cards working in the contactless mode. The results show that successful attacks on a software implementation of AES running on both models of Java Cards are possible.

A SIM, Subscriber Identity Module, is the removable circuit board found in a modern cellular phone. It carries the network identity information and is a type of smart card which can also be found on payment cards (EMV), ID cards and so on. A smart card is basically a small computer, providing a safe and controlled execution environment. Historically smart card software was very hardware dependent and mostly developed by the manufacturers themselves. With the introduction of the open Java Card standard created by Sun Microsystems (Oracle) this was meant to change. However, information still remains scattered and is hard to obtain. This paper is meant to serve both as an introduction to the field and also as a good foundation for future studies. It begins with a theoretical discussion about smart card hardware and software architectures, network standards in the context of SIM cards, typical applications, coming trends and technologies and ends off with an overview of the Java Card standard. The following section discusses the supplied example SIM card application coupled with an introduction how to use the Gemalto Developer Suite for application development and testing. The paper ends with an extensive appendix section going in depth about some of the more important subjects.

Master's thesis deals with the security risks of current authentication methods. There are described methods which are based on user's knowledge and ownership of authentication object and biometric authentication method. The practical part of this Master's thesis deals with a specific design of authentication system based on protocol ACP, when the user proves his identity by smart card on provider assets, which is represented by ACP portal on the user's computer.

The thesis describes the design of scheme for access system with user authentication via smart cards. The first chapter explains various types of identification items used for authentication of users and different types of readers and terminals, followed by chapter 2 with a deeper insight on smart cards with focus on their types, what internal structure and principle of communication with card readers are used, etc. with primary focus on Java cards. The third chapter describes Java Card cryptography - especially elliptic curve cryptography used on this platform. The fourth part focuses on PACE protocol with subsections dedicated to the individual parts of the protocol and its applicability to smart cards environment. Chapter 5 explains the proposed design of the authentication scheme elaborated in the thesis, including a detailed description of specific parts, their funcionality and exemplary usage in the created applications.