System description: CardTAP: The first theorem prover on a smart card
We present the first implementation of a theorem prover running on a smart card. The prover is written in Java and implements a dual tableau calculus. Due to the limited resources available on current smart cards, the prover is restricted to prepositional classical logic. It can be easily extended to full first-order logic.
The potential applications for our prover lie within the context of security related functions based on trusted devices such as smart cards.
KeywordsSmart Card Propositional Logic Theorem Prover Automate Reasoning Proof Tree
Unable to display preview. Download preview PDF.
- 1.G Necula and P Lee. Proof carrying code. Technical Report CMU-CS-96-165, Carnegie Mellon University, School of Computer Science, Pittsburgh, PA, September 1996.Google Scholar
- 3.Schlumberger Inc. Cyberflex. http://www.cyberflex.austin.et.slb.com, 1997.Google Scholar
- 4.JavaSoft Inc. Javacard API. http://www.javasoft.com/products/javacard/, 1997.Google Scholar