CardS4 : modal theorem proving on Java smart cards

• Autorzy: Gore R.P. , Nguyen P.T.
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

security of mobile code; modal deduction

PL

bezpieczeństwo; kod; kryptografia

• Wydawca: Instytut Łączności - Państwowy Instytut Badawczy
• Czasopismo: Journal of Telecommunications and Information Technology
• Rocznik: 2002
• Tom: nr 4
• Strony: 68--80
• Opis fizyczny: Bibliogr. 39 poz., rys.

Twórcy

autor

Gore R.P.

• Australian National University, Canberra, Australia

autor

Nguyen P.T.

Bibliografia

• [1] M. Abadi, “Secrecy by typing in security protocols”, J. ACM, vol. 46, no. 5, pp. 749–786, 1999.
• [2] M. Abadi, M. Burrows, B. Lampson, and G. Plotkin, “A calculus for access control in distributed systems”, ACM Trans. Program. Lang. Syst., vol. 15, no. 4, pp. 706–734, 1993.
• [3] M. Abadi and A. D. Gordon, “A calculus for cryptographic protocols: the spi calculus”, in Fourth ACM Conference on Computer and Communications Security. ACM Press, 1997.
• [4] M. Burrows, M. Abadi, and R. Needham, “A logic of authentication”, ACM Trans. Comput. Syst., vol. 8, pp. 18–36, 1990.
• [5] P. Boury and N. El Kadhi, “Static analysis of Java cryptographic applets”, in ECOOP’2001 Workshop on Formal Techniques for Java Programs. Tech. Rep., FernUniversität Hagen, 2001. [Online]. Available: http://www.informatik.fernuni-hagen.de/import/pi5/workshops/ecoop2001 papers.html.
• [6] N. Bonnette and R. Gor´e, “A labelled sequent system for tense logic Kt”, in AI98: Proceedings of the Australian Joint Conference on Artificial Intelligence, LNAI. Springer, 1998, vol. 1502, pp. 71–82.
• [7] D. Bell and L. La Padula, “Secure computer systems: unified exposition and multics interpretation”. Tech. Rep., MITRE Corp., July1975, no. MTR-2997.
• [8] K. Brunnstein, “Hostile activeX control demonstrated”, RISKS Forum, vol. 18, no. 82, 1997.
• [9] A. Chander, D. Dean, and J. Mitchell, “A state-transition model of trust management and access control”, in 14th Computer Security Foundations Workshop. IEEE Computer Society, 2001, pp. 27–43.
• [10] CERT Coordination Center. CERT(R) Advisory CA-2000-15. “Netscape allows Java applets to read protected resources”. [Online]. Available: http://www.cert.org/advisories/CA-2000-15.html.
• [11] H. Comon and V. Shmatikov, “Is it possible to decide whether a cryptographic protocol is secure or not?”, J. Telecommun. Inform. Technol., no. 4, pp. 5–15, 2002.
• [12] N. El Kadhi, “Automatic verification of confidentiality properties of cryptographic programs”, in Networking and Information Systems, vol. 3, no. 6, Herm`es, 2001. [Online]. Available: http://www.epita.fr:8000/ el-kad n/Hermes.ps.
• [13] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, in Synthese Library, D. Reidel, Ed. Dordrecht, Holland, 1983, vol. 169.
• [14] P. Girard, “Which security policy for multiapplication smart cards”, in Proc. USENIX Worksh. Smart Card Technol., Chicago, USA, 1999, pp. 21–28.
• [15] R. I. Goldblatt, Logics of Time and Computation, CSLI Lecture Notes. Stanford: Center for the Study of Language and Information, 1987, no. 7.
• [16] R. Gor´e, “Tableau methods for modal and temporal logics”, in Handbook of Tableau Methods, M. D’Agostino, D. Gabbay, R. H¨anle, and J. Posegga, Eds. Kluwer, 1999, ch. 6, pp. 197–396.
• [17] A. Gordon and A. Jeffrey, “Authenticity by typing for security protocols”, in 14th Computer Security Foundations Workshop. IEEE Computer Society, 2001, pp. 145–159.
• [18] J. A. Goguen and J. Meseguer, “Security policies and security models”, in IEEE Symp. Secur. Priv., 1982.
• [19] R. Gor´e and L. D. Nguyen, “CardKt: automated multi-modal deduction on Java cards for multi-application security”, in Proc. Java Card Workshop, LNCS. Springer, 2001 (to appear).
• [20] A. Heuerding, “Automated deduction in some propositional modal logics”. Institut f¨ur Angewandte Mathematik und Informatik, Universit¨ate Bern, Switzerland, 1999.
• [21] G. E. Hughes and M. J. Cresswell, A New Introduction to Modal Logic. Routledge, 1996.
• [22] R. Harper, F. Honsell, and G. Plotkin, “A framework for defining logics”, J. Assoc. Comput. Machin., vol. 40, no. 1, pp. 143–184, 1993.
• [23] J. Hudelmaier, “Improved decision procedures for the modal logics K, T and S4”.
• [24] R. Ladner, “The computational complexity of probability in systems of modal propositional logic”, SIAM J. Comput., vol. 6, no. 3, pp. 467–480, 1977.
• [25] X. Leroy, “Java bytecode verification: an overview”, in Proceedings of 13th International Conference on Computer-Aided Verification, G. Berry, H. Comon, and A. Finkel, Eds., Lecture Notes in Computer Science. Springer, 2001, vol. 2102, pp. 265–285.
• [26] X. Leroy and F. Rouaix, “Security properties of typed applets. Secure Internet programming – security issues for mobile and distributed objects”, in Lecture Notes in Computer Science. Springer, 1999, vol. 603, pp. 147–182. [Online]. Available: http://pauillac.inria.fr/~xleroy/publi/sip-typed-applets.ps.gz.
• [27] T. Lindholm and F. Yellin, The Java Virtual Machine Specification. The Java series. 2nd ed. Addison-Wesley, 1999.
• [28] F. Massacci, “Tableaux methods for access control in distributed systems”, in Automated Reasoning with Analytic Tableaux and Related Methods, D. Galmiche, Ed., Lecture Notes in Artificial Intelligence. Springer, 1997, vol. 1227, pp. 246–260.
• [29] A. Mathuria, “Contributions to authentication logics and analysis of authentication protocols”. Ph.D. thesis, School of Information Technology and Computer Science, University of Woolongong, Woolongong, Australia, 1997.
• [30] G. McGraw and E. Felten, Securing Java – Getting Down to Business with Mobile Code. Wiley, 1999. [Online]. Available: http://www.securingjava.com/.
• [31] D. Monniaux, “Analysis of cryptographic protocols using logics of belief: an overview”, J. Telecommun. Inform. Technol., no. 4, pp. 57–67, 2002.
• [32] G. Necula, “Proof-carrying code”, in Conference Record of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1997, pp. 106–119.
• [33] L. C. Paulson, ML for the Working Programmer. 2nd ed. Cambridge University Press, 1996.
• [34] P. Girard, J.-L. Lanet, V. Wiels, G. Zanon, P. Bieber, and J. Cazin, “Checking secure interactions of smart card applets”. Tech. Rep., Gemplus R&D Centre, 2000. [Online]. Available:http://www.gemplus.com/smart/r d/projects/pacap.htm.
• [35] A. Rao and M. Georgeff, “A model-theoretic approach to the verification of situated reasoning systems”, in Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93). Morgan-Kauffman, 1993, pp. 318–324.
• [36] E. Rose and K. Rose, “Lightweight bytecode verification”, In OOPSLA Satel. Worksh. Form. Underpin. Java, 1998.
• [37] G. F. Shvarts, “Autoepistemic modal logics”, in Theoretical Aspects about Reasoning about Knowledge, R. Parikh, Ed., 1990, pp. 97–109.
• [38] G. Smith, “A new type system for secure information flow”, in 14th Computer Security Foundations Workshop. IEEE Computer Society, 2001, pp. 115–125.
• [39] Sun Microsystems: “Java 2 platform micro edition technology for creating mobile devices”. White paper. [Online]. Available: http://java.sun.com/products/cldc/wp/KVMwp.pdf.