Affiliations: Institute of Informatics, Comenius University, Mlynska
dolina, 842 48 Bratislava, Slovakia. [email protected] | Dipartimento di Informatica, Università di Pisa, Largo
B. Pontecorvo 3, 56127 Pisa, Italy. {maggiolo,milazzo}@di.unipi.it
Note: [] Address for correspondence: Institute of Informatics, Comenius
University, Mlynska dolina, 842 48 Bratislava, Slovakia
Abstract: 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.
