Formal Security Analysis of Basic Network-Attached Storage

Avik Chaudhuri and Martín Abadi

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 implementation 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.


    author = {Avik Chaudhuri and Mart\'{\i}n Abadi},
    title = {Formal security analysis of basic network-attached storage},
    booktitle = {Proceedings of the 3rd ACM workshop on
                 Formal Methods in Security Engineering (FMSE'05)},
    year = {2005},
    pages = {43--52},
    publisher = {ACM}