Conformance checking of single access point pattern in JAAS using codecharts

Security design patterns are usually described using a variety of UML diagrams beside textual statements. Because, UML class diagrams are used to describe the structural aspects and UML sequence and/or activity diagrams are used to describe the behavioral aspects. So, when implementing, verifying, and/or detecting instances of those patterns, the issue of formality is raised. Many researchers have tried to formalize UML diagrams, however, loss of information and other problems were found. It is important that a security pattern is implemented correctly as incorrect implementation might result into a security flaw. This paper is the second of a series of papers for representing security patterns in Codecharts. We introduce using Codecharts to formally model the structural aspects of security patterns. In this paper, we show formal modelling of Single Access point pattern (SAP) in Codecharts. Furthermore, we show how TTP Toolkit is employed to verify design conformance of SAP in Java Authentication and Authorization Service (JAAS).