Security in a Model for Long-running Transactions

• Autorzy: Gruska D.P. , Maggiolo-Schettini A. , Milazzo P.
• Języki publikacji: EN

Abstrakty

EN

Communicating Hierarchical Transaction-based Timed Automata have been introduced to model systems performing long-running transactions. Here, for these automata a security concept is introduced, which is based on a notion of opacity and on the assumption that an attacker can not only observe public system activities, but also cause abortion of some of them. Different intruder capabilities as well as different kinds of opacity are defined and the resulting security properties are investigated. Security of long-running transactions is defined by the mentioned notion of opacity and conditions for compositionality are established.

Słowa kluczowe

EN

communnicating hierarchical timed automata; long-running transactions; opacity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 189--203
• Opis fizyczny: bibliogr. 13 poz., wykr.

Twórcy

autor

Gruska D.P.

autor

Maggiolo-Schettini A.

autor

Milazzo P.

• Institute of Informatics Comenius University Bratislava, Mlynska dolina, 842-48 Bratislava, Slovakia

Bibliografia

• [1] Alur, R., Dill, D.: A theory of timed automata, Theoretical Computer Science 126, 1994.
• [2] Bryans, J., Koutny,M., Ryan, P.: Modelling non-deducibility using Petri Nets. Proc. of the 2nd Int. Workshop on Security Issues with Petri Nets and other Computational Models (WISP'04), 2004.
• [3] Bryans, J., Koutny, M., Mazare L., Ryan, P.: Opacity generalised to transition systems, Proc. of Formal Aspects in Security and Trust (FAST'06), LNCS 3866, Springer, Berlin, 2006
• [4] Busi, N., Gorrieri, R.: Positive non-interference in elementary and Trace Nets. Proc. of Appl. and Theory of Petri Nets, LNCS 3099, Springer, Berlin, 2004.
• [5] Dhem, J.F., Koeune, F., Leroux, P.A., Mestre, P., Quisquater, J.J., Willems, J.L.: A practical implementation of the timing attack, Proc. of the Third Working Conference on Smart Card Research and Advanced Applications (CARDIS 1998), LNCS 1820, Springer, Berlin, 1998.
• [6] Felten, E.W., Schneider,M.A.: Timing attacks on web privacy, Proc. of the 7th ACMConference on Computer and Communications Security, 2000.
• [7] Goguen, J.A., Meseguer, J.: Security policies and security models, Proc. of IEEE Symposium on Security and Privacy, 1982.
• [8] Gorrieri, R., Martinelli, F.: A simple framework for real-time cryptographic protocol analysis with compositional proof rules. Science of Computer Programming 50, 2004.
• [9] Handschuh, H., Heys, H.M.: A timing attack on RC5, Proc. Selected Areas in Cryptography, LNCS 1556, Springer, Berlin, 1999.
• [10] Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS and other systems, Proc. Of Advances in Cryptology (CRYPTO'96), LNCS 1109, Springer, Berlin, 1996.
• [11] Lanotte, R., Maggiolo-Schettini, A., Milazzo, P., Troina, A.: Modeling long-running transactions with Communicating Hierarchical Timed Automata, Proc. of Formal Methods for Open Object-Based Distributed Systems (FMOODS'06), LNCS 4037, Springer, Berlin, 2006.
• [12] Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: closing a decidability gap, Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004.
• [13] Song. D., Wagner, D., Tian, X.: Timing analysis of Keystrokes and SSH timing attacks Proc. of the 10th USENIX Security Symposium, 2001.