SPDL specifications:Security Enhancement and Technique to Overcome Software Weakness for Android-Based Local Storage

This dataset is for publishing our SPDL specifications for proposed protocol described in "(Submitted to journal)Security Enhancement and Technique to Overcome Software Weakness for Android-Based Local Storage".
One can check any detail information by reading above paper.

[Tools for Security Protocol Verification]
A poorly designed security protocol can attract malicious attacks because of its potential vulnerability. To prevent such attacks, security protocol verification before implementation is important. As a flaw in the security protocol design is among the security weaknesses, prevention is important. Thus, the security properties of the security protocol should be verified in advance using a formal technique. Various tools have been used for security protocol verification, such as Failures-Divergences Refinement (FDR)/Casper, Automated Validation of Internet Security Protocols and Applications (AVISPA), Proverif, and Scyther. In this study, the proposed preventive technique is verified using Scyther, based on a protocol description written in Security Protocol Description Language (SPDL); this provides verification, counterevidence, and analysis of the protocol in graphical user interface (GUI) form.

[Modeling Proposed Protocol in SPDL for Scyther]
Scyther receives the protocol description specified in SPDL and provides verification results. All entities, such as the client or server, are represented by roles. In this study, roles D and S are defined as the client and server, respectively. We publish our SPDL specifications for each global variable definition, initialization phase, and authentication phase on Mendeley Data and provide it publicly available to the research community.