Franck Pommereau

Sam Sanjabi and Franck Pommereau
Proc. of COLSEC'10, IEEE Digital library, IEEE, 2010

Abstract. We present a security analysis of the SPREADS system, a distributed storage service based on a centralized peer-to-peer architecture. We formally modelled the salient behavior of the actual system using ABCD, a high level specification language with a coloured Petri net semantics, which allowed the execution states of the system to be verified. We verified the behavior of the system in the presence of an external Dolev-Yao attacker, unearthing some replay attacks in the original system. Furthermore, since the implementation is also a formal model, we have been able to show that any execution of the model satisfies certain desirable security properties once these flaws are repaired.

Keywords. Privacy Protection for Collaborative Systems, Security for Speecific Collaboration Domains (P2P), Security in Collaborative Multi-Agent Systems, Secure Collaborative Agents, Middleware Security.

Download PDF

@InProceedings{COLSEC10,
  author =       {Sanjabi, Sam and Pommereau, Franck},
  title =        {Modelling, Verification, and Formal Analysis of
                  Security Properties in a P2P System},
  booktitle =    {Workshop on Collaboration and Security (COLSEC'10)},
  pages =        {543--548},
  year =         {2010},
  publisher =    {IEEE},
  series =       {IEEE Digital Library},
  keywords =     {privacy protection for collaborative systems,
                  security for specific collaboration domains (P2P),
                  security in collaborative multi-agent systems,
                  secure collaboratove agents, middleware security}
}