• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

Bounded memory Dolev-Yao adversaries in collaborative systems

Information and Computation. 2014. No. 238. P. 233-261.
Kanovich M., Ban Kirigin T., Nigam V., Scedrov Andre.

In a collaborative system, the agents collaborate to achieve a common goal, but they are not willing to share some sensitive private information.

The question is how much damage can be done by a malicious participant sitting inside the system.

We assume that all the participants (including internal adversaries) have bounded memory – at any moment, they can store only a fixed number of messages of a fixed size. The Dolev–Yao adversaries can compose, decompose, eavesdrop, and intercept messages, and create fresh values (nonces), but within their bounded memory.

We prove that the secrecy problem is PSPACE-complete in the bounded memory model where all actions are balanced and a potentially infinite number of the nonce updates is allowed.

We also show that the well-known security protocol anomalies (starting from the Lowe attack to the Needham–Schroeder protocol) can be rephrased within the bounded memory paradigm with the explicit memory bounds.