Naslov
Progressing Collaborative Systems

Autori
Kanovich, Max ; Ban Kirigin, Tajana ; Nigam, Vivek ; Scedrov, Andre

Vrsta, podvrsta i kategorija rada
Sažeci sa skupova, pp prezentacija, znanstveni

Skup
Workshop on Foundations of Security and Privacy (FCS-PrivMod 2010)

Mjesto i datum
Edinburgh, Ujedinjeno Kraljevstvo, 14.07.2010. - 15.07.2010

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
collaborative systems ; critical configurations ; policy compliance ; multiset rewriting ; complexity ; model checking ; linear logic

Sažetak
This paper builds on existing models for collaborative systems with confidentiality policies. The actions in these models are balanced, namely, they have an equal number of facts in their pre- and postconditions. Here we consider a further restriction that each instance of an action is used at most once in a process. Administrative processes usually involve such progressing behavior, that is, whenever a transaction is performed, it does not need to be repeated. We investigate the complexity of the decision problem whether there exists a sequence of transitions from an initial state to a final state that avoids any critical states, e.g., states which conflict with the given confidentiality policies. We show that this problem is NP-complete when balanced actions do not involve fresh values and when the system is progressing. The same problem is shown to be PSPACE-complete when the system is not progressing, and PSPACE-hard when the system is progressing, but when actions may update values with fresh ones. The bounds hold even when balanced actions change only one fact in a configuration. We implement some examples in logic-based verification tools and model- check that they comply with certain policies.

Izvorni jezik
Engleski

Znanstvena područja
Matematika

Napomena
Http://www.loria.fr/~cortier/FCS-PrivMod10/

POVEZANOST RADA