Advertisement

System description: CardTAP: The first theorem prover on a smart card

  • Rajeev Goré
  • Joachim Posegga
  • Andrew Slater
  • Harald Vogt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

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 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.

Keywords

Smart Card Propositional Logic Theorem Prover Automate Reasoning Proof Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    Bernhard Beckert and Joachim Posegga. IeanTAP: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339–358, 1995.MathSciNetCrossRefGoogle Scholar
  3. 3.
    Schlumberger Inc. Cyberflex. http://www.cyberflex.austin.et.slb.com, 1997.Google Scholar
  4. 4.
    JavaSoft Inc. Javacard API. http://www.javasoft.com/products/javacard/, 1997.Google Scholar
  5. 5.
    Francis J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216, 1986.zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Rajeev Goré
    • 1
  • Joachim Posegga
    • 2
  • Andrew Slater
    • 1
  • Harald Vogt
    • 2
  1. 1.Automated Reasoning ProjectAustralian National UniversityCanberra
  2. 2.Technologiezentrum, IT SecurityDeutsche Telekom AGDarmstadt

Personalised recommendations