System Description: card TAP: The First Theorem Prover on a Smart Card

Abstract. 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 propositional 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. 1 Smart Cards: the Secure PC of Tomorrow Smart cards are currently evolving into one of the most exciting and most significant technologies of the information society. Current smart cards on the market are in fact small computers consisting of a processor, ROM and RAM, an operating system, a file system, etc. Although their resources are still quite restricted, continuous advances in chip manufacturing will soon enable to market smart cards with 32 bit processors and up to 128 KByte of memory. Manufacturers are also t...

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt
• Keywords: CADE 1998, Current Smart Cards, Logical Reasoning, Smart Card Technology, Smart Cards