Bounded memory Dolev–Yao adversaries in collaborative systems

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.

Authors

• Max Kanovich
• Tajana Ban Kirigin
• Vivek Nigam
• Andre Scedrov

Keywords

• Collaborative systems
• Protocol security
• Complexity results