Model Checking Access Control Protocol for Spreadsheets

Spreadsheets are one of the most used software systems in business and academia. Since the first introduction of electronic spreadsheets for personal computers in 1979, spreadsheets have significantly evolved. With recent technological advancements and new features added, spreadsheets have become powerful computing platforms capable of complex analysis and modelling. However, numerous publications over the years described cases of spreadsheet errors. In focus of this research paper are spreadsheet errors caused by unauthorized access and modifications of spreadsheets in multi-user environments. Specifically, this paper is structured around formal verification of the novel ABAC4S (Attribute Based Access Control for Spreadsheets) protocol designed for prevention or detection of unauthorized modifications to spreadsheets in multi-user environments. We utilized a model checking approach to verify ABAC4S protocol rules for correctness.