Access Control Verification in Smart Contracts Using Colored Petri Nets
Round 1
Reviewer 1 Report
Comments and Suggestions for AuthorsThis article is about the use of CPN in DAML modeling which is used for access control authentication. To be honest, it is not a fresh new idea to use CPN in smart contracts but the article has mentioned some important areas which are quite useful to the successful implementation. There are a few problems described below.
1) You have clearly described the detailed process from transforming the DAML contract up to verifying authorization properties. I have two concerns. The first concern is about the processing speed but you have mentioned in line#238 that the "number of seconds reported by the tool is zero". Where can I get this figure? Sometimes such authentication takes a long time which would affect the access convenience. The second concern is something like the Achilles's heel: It is quite easy to have a security gap between the integration of the two processes. Is there fault tolerance provided in case the intermediate step is down?
2) Testing is the best verification tool in most scientific concepts. It would be great if more testing data and results were provided.
Comments on the Quality of English Language
Good enough except a few typos found.
Author Response
Comment 1: You have clearly described the detailed process from transforming the DAML contract up to verifying authorization properties. I have two concerns. The first concern is about the processing speed but you have mentioned in line#238 that the "number of seconds reported by the tool is zero". Where can I get this figure? Sometimes such authentication takes a long time which would affect the access convenience. The second concern is something like the Achilles's heel: It is quite easy to have a security gap between the integration of the two processes. Is there fault tolerance provided in case the intermediate step is down?
Response 1: The number of seconds is reported in CPN Tools when using the Calculate state tool. There is a Save Report feature the prints a summary report regarding the generated state space. This is stated in the revised manuscript. Concerning the second point, this is an interesting observation. One way to address this Achilles's heel issue is by merging both processes into one (e.g., use a single program rather than two) to generate the final CPN. Also, we recommend using other smart contract testing methods to supplement our approach.
Comment 2: Testing is the best verification tool in most scientific concepts. It would be great if more testing data and results were provided.
Response 2: A total of eight DAML contracts were analyzed using our approach. All the artifacts created during analysis can be found in the paper’s GitHub repository which is referenced in the manuscript (https://github.com/ialazzon/cpn_daml_paper/). This repository also includes all the source code, including Java EMF and Python. It is a Gradle project where the reader can easily install and build the projects and start experimenting with the eight test contracts.
Reviewer 2 Report
Comments and Suggestions for AuthorsAccess Control Verification in Smart Contracts Using Colored Petri Nets
Review
This paper presents the access control in DAML smart contracts that utilizes Colored Petri Nets, by using a model-driven based approach which employs a meta-model for capturing access control requirements.
The approach is supported by tools that automates all steps: parsing DAML code, generating DAML model instances, transforming the DAML models into CPN models, and model checking the generated CPN models.
The topic is interesting. The manuscript is well structured, contains modeling, solving the problem and presentation of results.
The References are relevant. The Conclusions are related to the results.
However, some recommendations for changes to improve the impact:
1. The state of the art must be enriched.
2. A comparison with other approaches from relevant publications would validate the research.
3. Figures 4 and 6 must improve legibility.
Author Response
Comment 1: The state of the art must be enriched.
Response 1: We have placed a conclusion paragraph at the end of the related work section. In addition, we have added more references.
Comment 2: A comparison with other approaches from relevant publications would validate the research.
Response 2: We have made comparisons while presenting each paper in the related work. In addition, we have added a summary paragraph at the end of the Related Work section in the revised manuscript to emphasize how our approach is unique compared with other approaches.
Comment 3: Figures 4 and 6 must improve legibility.
Response 3: Done. We have enlarged the sizes of both figures.
Reviewer 3 Report
Comments and Suggestions for AuthorsThe paper presents an approach for the verification of access control in DAML smart contracts that utilizes Colored Petri Nets (CPNs). The approach is a model-driven based approach which employs a new meta-model for capturing access control requirements in DAML contracts. The approach is tested using several DAML scripts involving access control extracted from different domains of blockchain applications. The work is sound and can be published after few improvements: in line 37, specify billions of what; in line 41, define CPNs; in line 86 define LTL: explain better line 300. With these corrections paper can be published.
Comments for author File: 
Comments.pdf
The use of English language is fine, but a review by a native speaker is advisable.
Author Response
Comment 1: The work is sound and can be published after few improvements: in line 37, specify billions of what; in line 41, define CPNs; in line 86 define LTL: explain better line 300. With these corrections paper can be published.
Response 1: billions of dollars. It is now updated in the revised manuscript. In addition, we added the definitions as requested. In Line 300, we believe that the confusion was due to using the CPN marking notation: 1’alice++1’bob. To remove the confusion, we added this sentence to make the notation clear: “This multi-set has two tokens that correspond to Alice and Bob”.
Reviewer 4 Report
Comments and Suggestions for AuthorsAt the moment, unfortunately, the work is not ready for publication for the following reasons:
1. There is no formalized presentation of the algorithms
2. Figures 1, 3, 4, 6, 7 are not clear
3. It is not clear on what dates the testing was carried out, the results presented in Part 7 are very small
4. There is no testing on real systems
Author Response
Comment 1: There is no formalized presentation of the algorithms
Response 1: We had thought about that even before we submitted the paper. However, we’ve felt that it is not trivial nor informative to present the algorithms. The algorithms will be big in size. For example, each template maps to a transaction in addition to several places that are linked later to the output of other transformations. The full source code is available in the paper’s GitHub repository which is referenced in the manuscript (https://github.com/ialazzon/cpn_daml_paper/).
Comment 2: Figures 1, 3, 4, 6, 7 are not clear
Response 2: We have enlarged Figures 4 and 6. We believe that the other figures are visually clear and that there is no need to enlarge them as well.
Comment 3: It is not clear on what dates the testing was carried out, the results presented in Part 7 are very small
Response 3: The testing was carried out in August 2024. All the artifacts created during analysis can be found in the paper’s GitHub repository which is referenced in the manuscript (https://github.com/ialazzon/cpn_daml_paper/). This repository also includes all the source code, including Java EMF and Python. It is a Gradle project where the reader can easily install and build the projects and start experimenting with all test contracts.
Comment 4: There is no testing on real systems
Response 4: A total of eight DAML contracts were analyzed using our approach. All the artifacts created during analysis can be found in the paper’s GitHub repository which is referenced in the manuscript (https://github.com/ialazzon/cpn_daml_paper/). This repository also includes all the source code, including Java EMF and Python. It is a Gradle project where the reader can easily install and build the projects and start experimenting with the eight test contracts. These eight DAML contracts include all access control relevant features, such as observers, signatories, and controllers. In the conclusion section, we stated that “the evaluation can be extended by analyzing DAML contracts deployed in real-life use cases”. We are working on adding one or more such contracts to the repository.
Reviewer 5 Report
Comments and Suggestions for AuthorsThis paper presents an approach for the verification of access control in DAML smart contracts that utilizes Colored Petri Nets (CPNs).
I have some comments
1- the authors write DAML in the first line of Abstract before the readers know what is it, they should write the full name first.
2- Please put a table or Figure for related works to compare them.
3- I suggest to put a discussion section after the Evaluation section.
Comments on the Quality of English LanguageNo commednts
Author Response
Comment 1: The authors write DAML in the first line of Abstract before the readers know what is it, they should write the full name first.
Response 1: Done. We have added the full name as well.
Comment 2: Please put a table or Figure for related works to compare them.
Response 2: The related work section cites several related papers and compares them with our approach. Since there is no related paper that has the exact same contribution (also on DAML smart contracts), we decided that presenting a comparison in the form of a table or figure is not suitable. We have made the best efforts in comparing our approach with other approaches and we have added a new paragraph at the end of the section summarizing our unique contributions.
Comment 3: I suggest to put a discussion section after the Evaluation section.
Response 3: We would like to thank the reviewer for making this suggestion. However, the evaluation section discusses in detail the analysis of the two CPNs from Section 5. We feel that there is no need to create a separate discussion section.
Round 2
Reviewer 2 Report
Comments and Suggestions for AuthorsThe revised manuscript can advance for publication.
Reviewer 4 Report
Comments and Suggestions for AuthorsNo significant changes were made, the authors refer that everything what is needed can be viewed in their repository on GitHub.
Reviewer 5 Report
Comments and Suggestions for AuthorsThey did good job
Comments on the Quality of English LanguageNo comments
