Formal security analysis of basic network-attached storage

We study formal security properties of network-attached storage (NAS) in an applied pi calculus. We model NAS as an implementation of a specification based on traditional centralized storage. We show the correctness of the implen by proving that it is fully abstract with respect to the specification. Our result can be viewed as a strong guarantee of security for a basic network-attached storage design. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; H.3.4 [Information Storage and Retrieval]: Systems and Software—Distributed Systems; D.4.6 [Operating Systems]: Security and Protection General Terms Security, Verification, Languages, Theory Keywords torage, full abstraction, applied pi calculus

• Type: Conference
• Year: 2005
• Where: CCS
• Authors: Avik Chaudhuri, Martín Abadi
• Keywords: Applied Pi Calculus, CCS 2005, Formal Security Properties, Network-attached Storage, Security Privacy