CardS4 swMATH ID: 1627 Software Authors: Goré, Rajeev Prabhakar; Thê Nguyên, Phuong Description: CardS4: Modal theorem proving on Java smardcards We describe a successful implementation of a theorem prover for modal logic S4 that runs on a Java smart card with only 512 KBytes of RAM and 32KBytes of EEPROM. Since proof search in S4 can lead to infinite branches, this is “proof of principle” that non-trivial modal deduction is feasible even on current Java cards. We hope to use this prover as the basis of an on-board security manager for restricting the flow of “secrets” between multiple applets residing on the same card, although much work needs to be done to design the appropriate modal logics of “permission” and “obligations”. Such security concerns are the major impediments to the commercial deployment of multi-application smart cards. Homepage: http://ftp.rsise.anu.edu.au/papers/gore/CardS4/jtit.pdf Keywords: security of mobile code; modal deduction Related Software: Cited in: 1 Publication Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year CardS4: Modal theorem proving on Java smardcards. Zbl 1002.68633Goré, Rajeev Prabhakar; Thê Nguyên, Phuong 2001 Cited by 2 Authors 1 Goré, Rajeev Prabhakar 1 Thê Nguyên, Phuong Cited in 0 Serials Cited in 1 Field 1 Computer science (68-XX) Citations by Year