Napredna pretraga

Pregled bibliografske jedinice broj: 484388

Bounded memory Dolev-Yao adversaries in collaborative systems


Max Kanovich; Tajana Ban Kirigin; Vivek Nigam; Andre Scedrov
Bounded memory Dolev-Yao adversaries in collaborative systems // Formal Aspects of Security and Trust Lecture Notes in Computer Science, 2011, Volume 6561/2011 / Degao, Pierpaolo ; Etalle, Sandro ; Guttman, Joshua (ur.).
Berlin: Springer, 2011. str. 18-33


Naslov
Bounded memory Dolev-Yao adversaries in collaborative systems

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

Vrsta, podvrsta i kategorija rada
Poglavlja u knjigama, znanstveni

Knjiga
Formal Aspects of Security and Trust Lecture Notes in Computer Science, 2011, Volume 6561/2011

Urednik/ci
Degao, Pierpaolo ; Etalle, Sandro ; Guttman, Joshua

Izdavač
Springer

Grad
Berlin

Godina
2011

Raspon stranica
18-33

ISBN
978-3-642-19750-5

Ključne riječi
Collaborative Systems, Policy Compliance, Multiset Rewriting, Complexity, Model Checking, Security protocols, Adversary

Sažetak
This paper extends existing models for collaborative systems. We in- vestigate how much damage can be done by insiders alone, without collusion with an outside adversary. In contrast to traditional intruder models, such as in protocol security, all the players inside our system, including potential adversaries, have similar capabilities. They have bounded storage capacity, that is, they can only re- member at any moment a bounded number of facts. This is technically imposed by only allowing balanced actions, that is, actions that have the same number of facts in their pre and post conditions. On the other hand, the adversaries inside our system have many capabilities of the standard Dolev-Yao intruder, namely, they are able, within their bounded storage capacity, to compose, decompose, overhear, and intercept messages as well as update values with fresh ones.We in- vestigate the complexity of the decision problem of whether or not an adversary is able to discover secret data. We show that this problem is PSPACE-complete when all actions are balanced and can update values with fresh ones. If we further impose the condition, called progressing, that in a plan any instance of an action can be used at most once, then this new problem is NP-complete when actions are balanced and only a fixed number of updates with fresh values is allowed and it is PSPACE-hard when actions are balanced and any number of updates with fresh values is allowed. Finally, we return to traditional intruder models and demon- strate that many protocol anomalies, such as the Lowe anomaly in the Needham- Schroeder public key exchange protocol, can also occur when the intruder is one of the insiders with bounded memory.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Filozofija

Napomena
Http://www.iit.cnr.it/FAST2010/



POVEZANOST RADA


Projekt / tema
009-0091328-0941 - Logika i stvarnost (Majda Trobok, )
120-1203164-3074 - Matematička logika i primjene (Zvonimir Šikić, )

Ustanove
Filozofski fakultet, Rijeka,
Fakultet strojarstva i brodogradnje, Zagreb,
Sveučilište u Rijeci - Odjel za matematiku

Autor s matičnim brojem:
Tajana Ban-Kirigin, (229313)