Vivek Nigam, Bounded memory Dolev-Yao adversaries in collaborative systems
TCS Oberseminar, 27.05.2011, 11 Uhr c.t.
Bounded memory Dolev-Yao adversaries in collaborative systems
This paper extends existing models for collaborative systems.
We investigate 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 remember at
any moment a bounded number of symbols. 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, and bounding the size
of facts, that is, the number of symbols they contain. 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
create fresh values. We investigate 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 the size of messages
is an input bound and when all actions are balanced and can possibly
create fresh values. As an application we turn to security protocol analysis and
demonstrate 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.
abgelegt unter: Oberseminar