Applications of Access Control Logics to Online Banking Systems
MetadataShow full item record
- Master theses 
Digitalisation has in many ways helped us become more productive and efficient. Technology has transformed the way we do banking. Online banking systems have made banking significantly simpler, and are offered by most modern banks today. Most users are uncritical as to how the functionality of these conform to the expectations. These systems deal with sensitive information, and attackers have a lot to gain by being able to exploit these systems. Because of this, users are dependent on correct and secure systems. In 2021, broken access control is regarded by OWASP as the most common security risk to web applications. This means that a large number of web applications can be exploited by at-tackers, by bypassing the intended permissions of users. In this thesis, we design a specification for an online banking system. These specifications are derived from research on existing systems and testing. Further, we introduce a formal language combining modal logic with first order logic, and introduce an axiomatic system based on this logic, created with the intent of reasoning about the access control of our system. We reason about the correctness of our axiomatic system, and use these axioms to formalize examples relevant to the design specification. Completion of these elements was a continuous process. Some challenges surfaced regarding domain knowledge, as well as with the use of first order logic for reasoning about continuous elements of the system. We found that modal logic was convenient for allowing us to represent the actions of actors and their corresponding outcomes in the system. We conclude that the project represents a starting point for further development of a standardized approach to formal verification of access control systems.