Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2011 / Oberseminar / On the Complexity of Linear Authorization Logics (Preliminary Results)


Inhaltsbereich

On the Complexity of Linear Authorization Logics (Preliminary Results)

TCS Oberseminar, 26.08.2011 11 Uhr c.t.
Wann 11:15 12:15 26.08.2011
von bis
Wo L109
Termin übernehmen vCal
iCal

On the Complexity of Linear Authorization Logics (Preliminary Results)
by Vivek Nigam

Linear Authorization Logics have been used in the Proof-Authentication Framework (PCA) to specify effect-based policies, such as policies involving consumable resources. A key requirement of PCA is the need to create proof-objects, which requires proof search. We demonstrate that the propositional multiplicative fragment of linear authorization logics is undecidable. Therefore, PCA using simple linear policies might already not be feasible. However, we also identify a first-order fragment for which the provability problem is decidable. In particular, we capitalize on the recent work on the decidability of the reachability problem for MSR systems with balanced actions to identify a fragment of linear authorization logics that is PSPACE-complete, namely the fragment of balanced bipolars. This is accomplished by first formalizing a (sound and complete) correspondence between linear authorization logic provability and MSR reachability and then showing that MSR reachability is PSPACE-complete.

Artikelaktionen

abgelegt unter:

Funktionsleiste