Results 81 to 90 of about 1,014 (107)
Some of the next articles are maybe not open access.
Formal Verification of a JavaCard Virtual Machine with Frama-C
2021Formal verification of real-life industrial software remains a challenging task. It provides strong guarantees of correctness, which are particularly important for security-critical products, such as smart cards. Security of a smart card strongly relies on the requirement that the underlying JavaCard virtual machine ensures necessary isolation ...
Adel Djoudi +2 more
openaire +1 more source
2001
This abstract provides some background information on smart cards, and explains the challenges these cards represent for formal verification of software.
openaire +2 more sources
This abstract provides some background information on smart cards, and explains the challenges these cards represent for formal verification of software.
openaire +2 more sources
Proving correctness of JavaCard DL taclets using Bali
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005Developed at the University of Karlsruhe, KeY is an augmented commercial CASE tool with specification and deductive verification functionalities. Recently, lightweight, stand-alone tactics or "taclets" have been introduced in order to implement the JavaCard dynamic logic (JavaCard DL) sequent calculus within KeY.
openaire +1 more source
Design of an Authentication Protocol for Gsm Javacards
2002In this work, we present an authentication protocol derived by the integration of the Kerberos and Lamport authentication schemes. The protocol is targeted to the GSM network, involving users that interact through a mobile phone, and the network provider acting as trusted authority.
openaire +2 more sources
Static Program Analysis of Multi-Applet JavaCard Applications
2011Java Card provides a framework of classes and interfaces that hide the details of the underlying smart card interface and make it possible to load and run on the same card several applets, from different application providers with complex trust relationships.
Alexandros Loizidis +2 more
openaire +1 more source
Product Agent Concept Based on Feature Modelling and JavaCard Implementation
The International Journal of Advanced Manufacturing Technology, 2002This paper describes research currently being carried out in the area of holonic systems. The work presented deals with the idea that process management (manufacturing, repairing, etc.) may be achieved by human operators or automated systems, but also by the product carrying and managing its own information. Each product can act as an autonomous entity
P. Charpentier, D. Jacquel, F. Chaxel
openaire +1 more source
Die JavaCard als Programmier- und Ausführungsplattform für verteilte Anwendungen
1999Chipkarten, die durch ihren integrierten Prozessor einfach zu nutzende Rechenkapazitat an einem beliebigen Ort bereitstellen, finden in immer mehr Bereichen Verwendung. In jungster Zeit wurden Kartenbetriebs systeme entwickelt, die Mehrfachanwendungen ermoglichen, sowie Karten, die in einer Hochsprache programmiert werden konnen und die es erlauben ...
Stefan Fünfrocken +2 more
openaire +1 more source
MAJA Konzept eines Multiple Application JavaCard Environment
1998Wir stellen die Ziele des aktuellen Chipkartenprojekts an der TU Darmstadt vor. Dabei geht es um den Einsatz einer multifunktionalen Chipkarte mit der Moglichkeit, dynamisch Anwendungen durch den Benutzer zu laden und zu entladen.
openaire +1 more source
Validation of the JavaCard Platform with Implicit Induction Techniques
2003The bytecode verifier (BCV), which performs a static analysis to reject potentially insecure programs, is a key security function of the Java(Card) platform. Over the last few years there have been numerous projects to prove formally the correctness of bytecode verification, but relatively little effort has been made to provide methodologies ...
Gilles Barthe, Sorin Stratulat
openaire +1 more source
Tool-Assisted Specification and Verification of the JavaCard Platform
2002Bytecode verification is one of the key security functions of the JavaCard architecture. Its correctness is often cast relatively to a defensive virtual machine that performs checks at run-time, and an offensive one that does not, and can be summarized as stating that the two machines coincide on programs that pass bytecode verification.
Gilles Barthe +3 more
openaire +1 more source