This paper presents a case study in the application of formal modelling and verification techniques to a large-scale distributed operating system for Grids called XtreemOS. The process algebraic language of applied pi-calculus is used to model one of the mutual authentication protocols in the XtreemOS trust model, and an associated tool called ProVerif is used to verify the data leakage and mutual authentication properties in the protocol. The results, beside enhancing the level of assurance of the protocol in a critical part of the system, contribute to better understanding of the level of detail in the protocol's specification hence enabling better implementation of the protocol.
|Publication status||Published - 26 Jun 2012|
|Event||3rd International ACM Sigsoft Symposium on Architecting Critical Systems 2012 - Bertinoro, Italy|
Duration: 26 Jun 2012 → …
|Conference||3rd International ACM Sigsoft Symposium on Architecting Critical Systems 2012|
|Period||26/06/12 → …|