Smart cards for transit : multi-use remotely interrogated stored-data cards for fare and toll payment /

"FTA-MA-26-0020-95-1."

Use of Java Cards in a telematic voting system.

This paper presents a general view of the telematic voting system developed by its authors, with a special emphasis on the important role that smart cards play in this scenario. The use of smart cards as basic pieces for providing secure cryptographic operations in this type of voting scheme is justified. The differences and advantages of Java Cards in comparison with the ?classical? smart cards (those that completely conform to the ISO/IEC 7816 standard) are also discussed. As an example, the paper describes one of the applets implemented in the voting Java Card as part of the general telematic voting application.

Privacy and security enhanced offline oblivious transfer for massive data distribution

Unauthorized accesses to digital contents are serious threats to international security and informatics. We propose an offline oblivious data distribution framework that preserves the sender's security and the receiver's privacy using tamper-proof smart cards. This framework provides persistent content protections from digital piracy and promises private content consumption.

Android as a cloud ticket validator

Trabalho Final de Mestrado para a obtenção do grau de Mestre em Engenharia Informática e de Computadores

Accommodation management system using mobile devices

Os dispositivos móveis são pessoais, intransmissíveis e cada vez mais utilizados, tornando-se assim numa boa ferramenta para a realização de um conjunto de serviços na indústria hoteleira. Entre esses serviços que necessitam da identificação pessoal, encontram-se a possibilidade do cliente reservar um quarto ou utilizar o serviço de quartos. Atualmente é muito utilizado, nos locais de alojamento, um smart card que possibilite ao cliente ter acesso a alguns dos serviços disponíveis. O objetivo deste documento é apresentar uma alternativa ao sistema de cartões, utilizando para o efeito, dispositivos móveis. De modo a garantir a segurança e uma utilização semelhante ao sistema de cartões existentes foi utilizada a tecnologia NFC (Near Field Communication) que, ao permitir o modo de emulação de cartão, facilita a transação do sistema de smart card existente, para o da utilização de dispositivos móveis na realização das mesmas funções. Mais concretamente, será abordada a utilização de smartphones para o processo de abertura de portas. Para que exista uma melhor compreensão e para que haja um conhecimento das suas capacidades e limites foram estudados casos de uso da tecnologia NFC. Este documento apresenta ainda os processos de desenvolvimento de uma aplicação nativa para o sistema operativo Android, cujo objetivo é proporcionar ao cliente de um local de alojamento um novo modo de acesso ao quarto, utilizando a tecnologia NFC. Para além desta funcionalidade a aplicação permite ainda ao utilizador fazer reservas, fazer o check-in, fazer o check-out entre outras. Posteriormente serão apresentadas as conclusões e possíveis trabalhos futuros.

Muntatge d’una memòria en el sistema microprocessat Olorim

Aquest projecte parteix d'un projecte anterior realitzat per un company d'escola, en el qual es pretenia muntar un sistema per obtenir un diagnòstic dels pacients que pateixen bruxisme. El sistema que aquest company va muntar constava de dos subsistemes: el sistema de captura, encarregat de capturar el senyal mitjançant sensors i pretractar el senyal i el sistema de processament de dades, encarregat de rebre les dades provinents del sistema de captura mitjançant una ràdio sintonitzada a la freqüència 432,95MHz, que després s'envien al convertidor A/D de l'Olorim i s'emmagatzemen a la memòria interna de l'Olorim. Aquest projecte pretén millorar l'apartat de capacitat per a les dades i oferir major portabilitat mitjançant una targeta SD. Per dur a terme aquesta millora es recullen les dades emmagatzemades a la memòria interna del sistema microprocessat i s’emmagatzemen en una memòria SD. Les dades s'emmagatzemen a la targeta SD dins un fitxer creat prèviament amb l'ordinador, el qual ha de ser el primer fitxer que es crea a la targeta, ja que ha d'estar en sectors consecutius. En aquest fitxer s'aniran emmagatzemant les dades que ens proporcioni el sistema de captura en format RAW

Algorithms and cryptographic protocols using elliptic curves

En els darrers anys, la criptografia amb corbes el.líptiques ha adquirit una importància creixent, fins a arribar a formar part en la actualitat de diferents estàndards industrials. Tot i que s'han dissenyat variants amb corbes el.líptiques de criptosistemes clàssics, com el RSA, el seu màxim interès rau en la seva aplicació en criptosistemes basats en el Problema del Logaritme Discret, com els de tipus ElGamal. En aquest cas, els criptosistemes el.líptics garanteixen la mateixa seguretat que els construïts sobre el grup multiplicatiu d'un cos finit primer, però amb longituds de clau molt menor. Mostrarem, doncs, les bones propietats d'aquests criptosistemes, així com els requeriments bàsics per a que una corba sigui criptogràficament útil, estretament relacionat amb la seva cardinalitat. Revisarem alguns mètodes que permetin descartar corbes no criptogràficament útils, així com altres que permetin obtenir corbes bones a partir d'una de donada. Finalment, descriurem algunes aplicacions, com són el seu ús en Targes Intel.ligents i sistemes RFID, per concloure amb alguns avenços recents en aquest camp.

Muntatge d’una memòria en el sistema microprocessat Olorim

Aquest projecte parteix d'un projecte anterior realitzat per un company d'escola, en el qual es pretenia muntar un sistema per obtenir un diagnòstic dels pacients que pateixen bruxisme. El sistema que aquest company va muntar constava de dos subsistemes: el sistema de captura, encarregat de capturar el senyal mitjançant sensors i pretractar el senyal i el sistema de processament de dades, encarregat de rebre les dades provinents del sistema de captura mitjançant una ràdio sintonitzada a la freqüència 432,95MHz, que després s'envien al convertidor A/D de l'Olorim i s'emmagatzemen a la memòria interna de l'Olorim. Aquest projecte pretén millorar l'apartat de capacitat per a les dades i oferir major portabilitat mitjançant una targeta SD. Per dur a terme aquesta millora es recullen les dades emmagatzemades a la memòria interna del sistema microprocessat i s’emmagatzemen en una memòria SD. Les dades s'emmagatzemen a la targeta SD dins un fitxer creat prèviament amb l'ordinador, el qual ha de ser el primer fitxer que es crea a la targeta, ja que ha d'estar en sectors consecutius. En aquest fitxer s'aniran emmagatzemant les dades que ens proporcioni el sistema de captura en format RAW

Propuesta basada en el modelo internacional de tarjetas de acreditación para extranjeros como alternativa para la promoción del turismo en la ciudad de Bogotá

Basados en estadísticas publicadas por entidades oficiales como el Ministerio de Comercio, Industria y Turismo, el DANE y la Alcaldía de Bogotá donde se refleja un aumento significativo en las cifras de visitantes extranjeros y en la participación de la ciudad de Bogotá como principal destino turístico del país. Se comprende que la variación positiva en las cifras publicadas sobre el número de visitantes de todo tipo y eventos internacionales por parte de las entidades oficiales nombradas anteriormente, son el resultado de una gestión y enfoque claro que estos organismos han logrado desarrollar en su intento por hacer más competitivo y sostenible el turismo de la ciudad de Bogotá, dentro del sector turismo en Colombia. Ese enfoque de hacer más competitivo el turismo en Bogotá hace que actualmente la gestión de los programas de desarrollo nacional y distrital brinde oportunidades de acceso, apoyo y tendencia de crecimiento en la oferta turística que hace muy atractiva la inversión en el sector, razón por la cual este documento pretende generar una propuesta para adaptar un modelo de acreditación a extranjeros que actualmente funciona en diferentes capitales del mundo como España o Nueva York, ajustado de acuerdo a un previo análisis del entorno y las características del sector turístico en Bogotá y en Colombia. La propuesta desarrollada estructura todas las características del servicio, su funcionamiento y las políticas de mercadeo. Esta definición permitirá medir la viabilidad a nivel de mercado y los resultados a nivel financiero aterrizando la propuesta a una posible implementación en el corto plazo.

O significado da distribuição para os grandes bancos verejistas: análise e consequências sob o ponto de vista de marketing

Trata da revolução em curso nos canais de distribuição dos grandes bancos varejistas em função dos impactos provocados pela tecnologia, pela globalização, pelas parcerias e pela formação de um novo ambiente de distribuição eletrônico, remoto e virtual denominado como marketspace. Esse novo ambiente, até o ano de 2007, deverá canalizar 2/3 dos negócios bancários que envolvam efetiva intermediação financeira. A revolução é tão importante que pode significar o início de um novo ciclo no negócio dos grandes bancos varejistas. Os impactos sobre marketing são igualmente poderosos, exigindo dos bancos uma completa revisão de sua estratégia mercadológica. Evidências foram colhidas de extensiva revisão bibliográfica, através de entrevistas em profundidade e de pesquisa amostrai com clientes bancários. Cursos de ação são sugeridos.

Superando os riscos da segurança baseada em perímetro - Uma abordagem com identificação federada através de certificados digitais A3/ICP-Brasil e SAML

The traditional perimeter-based approach for computer network security (the castle and the moat model) hinders the progress of enterprise systems and promotes, both in administrators and users, the delusion that systems are protected. To deal with the new range of threats, a new data-safety oriented paradigm, called de-perimeterisation , began to be studied in the last decade. One of the requirements for the implementation of the de-perimeterised model of security is the definition of a safe and effective mechanism for federated identity. This work seeks to fill this gap by presenting the specification, modelling and implementation of a mechanism for federated identity, based on the combination of SAML and X.509 digital certificates stored in smart-cards, following the A3 standard of ICP-Brasil (Brazilian official certificate authority and PKI)

Desenvolvimento formal de aplicações para smartcards

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.

JCML - Java Card Modeling Language: Definição e Implementação

Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers