Pith. sign in

REVIEW 3 major objections 5 minor 144 references

A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper argues that an Eclipse IDE wrapping Alice & Bob notation, the AnBx compiler, OFMC, and ProVerif makes formal verification of security protocols usable by non-specialists, and supports this with student surveys showing high…

desk verdict A genuinely useful tool paper with one solid benchmark and an honest limitations section; the abstract's educational-impact claim outruns the evidence. read the letter →

arxiv 2411.17926 v1 pith:N5KWYJPV submitted 2024-11-26 cs.CR cs.SE

Rémi Garcia , Paolo Modesti This is my paper · ORCID
classification cs.CRcs.SE
keywords securityprotocolsformalmethodsAnBxAliceandBobnotationOFMCProVerifmodel-drivendevelopmentcryptographyeducation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish that a well-integrated IDE can lower the adoption barrier for formal verification of security protocols, so that even students with little formal-methods or cryptography background can model, verify, and implement protocols. The vehicle is the AnBx IDE, which wraps the Alice & Bob high-level notation, the AnBx compiler and code generator, the OFMC model checker, and the ProVerif verifier in an Eclipse environment with live validation, push-button verification, parallel single-goal checking, and clear result visualisation. The authors surveyed 35 students who used the toolkit; most rated it highly useful, 65.71 percent called it very important for completing their projects, and more than two-thirds said they would use it again. If correct, this would make formal methods a routine part of security protocol design and education rather than a specialist-only activity.

What carries the argument

The load-bearing object is the AnBx IDE itself: an Eclipse plug-in whose grammar-based editor provides scoping, type and arity checking, and quick fixes on AnB, AnBx, ProVerif, and OFMC/IF specifications, and whose task scheduler, console colouring, single-goal parallel verification, and attack-trace reconstruction automate the loop between modelling and verification. The Alice & Bob notation (and its AnBx extension) is a high-level, human-readable way to write a protocol as message exchanges between named agents, with goals stated separately; the compiler turns AnBx into AnB for OFMC and into applied-pi for ProVerif, and generates Java implementations, so the same model is verified at abstract and concrete levels.

What would settle it

A controlled comparison in which similar students are randomly assigned to design and verify a protocol using either the AnBx IDE or a plain command-line toolchain, then take an objective applied-cryptography test and submit independently scored protocol models; if IDE users do not significantly outperform the control group on correctness or misconception reduction, the central claim is not supported.

Watch

Extended reading notes

Core claim

The central claim is that integrating a high-level protocol notation with automated verification tools inside an IDE turns formal verification into a workable workflow for non-experts. Concretely, the AnBx IDE supports editing, validation, verification, and Java code generation from a single AnBx model; it automates intermediate steps such as IF-file generation, single-goal verification in parallel, and OFMC attack-trace reconstruction into AnB and Java. Survey responses from 35 university students indicate that the IDE was important to completing their projects and that they would use it again; the paper also reports that the IDE addresses six documented barriers to formal-method adoption — complexity, limited tool integration, unfamiliar interfaces, interpretability of results, scalability, and documentation.

Load-bearing premise

The load-bearing premise is that students' self-reported survey ratings accurately measure real learning and workflow benefit, rather than gratitude or social-desirability bias; the paper itself acknowledges in Section 6.4 that the evaluation relies on the accuracy of self-assessment surveys.

Editorial extensions

If this is right

  • Practitioners and students with limited formal-methods background can complete verified security-protocol projects, which lowers the main barrier to formal methods adoption identified in expert surveys.
  • Parallel single-goal verification cuts ProVerif verification time by at least half on the benchmarked protocols, making iterative verification practical on multicore machines.
  • Because the same AnBx model feeds OFMC, ProVerif, and the Java and Docker code generator, verified designs can be executed directly, reducing translation errors between specification and implementation.
  • The IDE's immediate validation and quick fixes can forestall common cryptographic mistakes during modelling, which is the mechanism by which it claims to help learners grasp applied cryptography.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next step not tested in the paper is whether IDE-assisted users can later design and verify a new protocol without the IDE; the survey measures self-perception, not retention or transfer.
  • The misconception survey and the IDE's error messages target the same failures (for example, confusing public and symmetric keys), which suggests the IDE's pedagogical value may come from immediate corrective feedback rather than from explanations; a pre/post misconception test would separate those channels.
  • The paper's architecture — a browser-style editor, a task scheduler, single-goal parallelisation, and trace reconstruction — appears transferable to other security verification tools or other domain-specific languages, although the paper only lists this as future work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents the AnBx IDE, an Eclipse-based development environment for designing, verifying, and implementing security protocols. It builds on the AnB/AnBx notation, the AnBx compiler and code generator, OFMC, and ProVerif, and adds editing support, validation, task scheduling, result visualisation, attack-trace reconstruction, and Dockerised Java code generation. The authors evaluate the IDE against six barriers to formal-method adoption drawn from the literature, report a misconception survey of 59 cybersecurity students, a satisfaction survey of 35 students, usage statistics from the Eclipse Marketplace, and a benchmark comparing all-goal versus single-goal parallel verification. The paper claims that the IDE is valuable as a workflow aid and helps users grasp essential cybersecurity concepts, including users with limited formal-methods or cryptography backgrounds.

Significance. If the effectiveness claims were substantiated, the AnBx IDE would be a useful practical contribution to lowering the adoption barrier for formal verification of security protocols, particularly in educational settings. The paper's strengths include a detailed and specific account of the tool's features, a reproducible benchmark (Table 1) with concrete timing data for eleven protocols, long-term usage statistics, and an honest and explicit statement of assumptions and limitations in Section 6.4. However, the central claim that the IDE 'helps users grasp essential cybersecurity concepts' is not supported by the evidence presented: the evaluation relies entirely on self-reported Likert ratings from a self-selected student sample, with no control group, no pre/post measurement of learning, and no objective learning-gain metric. The paper's own Section 6.4 acknowledges that the evaluation depends on the accuracy of self-assessment surveys.

major comments (3)
  1. [Abstract and Section 6.2] The abstract's claim that the IDE 'helps users grasp essential cybersecurity concepts' is not supported by the study design. The misconception survey in Section 2.3 and the user-evaluation survey in Section 6.2 were administered to almost entirely disjoint cohorts; there is no pre-test/post-test comparison within the same group of users, and no comparison condition involving a different tool or method. The Likert items in Section 6.2 measure perceived usefulness and satisfaction, not actual gains in conceptual understanding. The evidence can support a claim about perceived usefulness, but not a causal claim about learning.
  2. [Section 6.4] The assumptions paragraph explicitly states that the evaluation 'relies on the accuracy of self-assessment surveys in capturing users' perceptions of the IDE's usability and educational impact.' This is an unverified premise that is load-bearing for the paper's educational-effectiveness claim. Since the survey in Section 6.2 is the sole evidence for that claim, the stated assumption is not a minor caveat but a gap in the chain of evidence. The paper should either provide an objective learning-gain measure (e.g., a pre/post knowledge test on the same cohort) or explicitly restrict the paper's claims to perceived usefulness and user satisfaction.
  3. [Section 6.2, 'Importance of Tools' and 'Verification Tasks'] The interpretation of the survey results overstates their significance. The participants chose to use the toolkit as part of their project proposals (as the paper notes for pedagogical reasons), so the sample is self-selected, and the high ratings may reflect selection bias rather than the IDE's intrinsic value. The statement that most students rated the tools as 'Very important' for completing their projects is anecdotal self-report; the paper itself admits that 'it is not possible to perform a quantitative evaluation, as projects are very different in nature.' The average mark of 67/100 for IDE users is not compared against a matched control group and cannot substantiate a workflow-effectiveness claim.
minor comments (5)
  1. [Section 2.3] There is a typo in the phrase 'Most of of the participants'; it should be 'Most of the participants'.
  2. [Section 6.2] The sentence 'Participants appreciated the ability to monitor tasks and ure verification processes' contains a typo: 'ure' should be 'use'.
  3. [Section 5.2.6] The sentence 'Theuseralso hastheoption to sort the list of protocols alphabetically' is missing spaces; it should read 'The user also has the option'.
  4. [Section 5.1.4] In the discussion of the ProVerif scoping example, 'evente' should probably be 'event e' (the event name).
  5. [Table 1] The table would be easier to read if the benchmark methodology included standard deviations or at least a statement that the measurements are averages over 20 runs; the current presentation gives no indication of variance across runs.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation chain: the IDE effectiveness claim rests on user surveys and external usage data, not on a self-referential reduction.

full rationale

The paper's central claim is an empirical usability and educational-effectiveness claim about an IDE, not a derived mathematical result. There is no fitted parameter later renamed as a prediction, no equation that reduces to an input by construction, and no uniqueness theorem imported from the authors' own prior work to force a particular choice. The self-citations (e.g., [26], [33], [37], [79], [83]) document the lineage of the AnBx language, compiler, and prototype; they do not by themselves entail the effectiveness claim, which is supported by user surveys and Eclipse Marketplace statistics. Section 6.4 explicitly acknowledges that the evaluation 'relies on the accuracy of self-assessment surveys in capturing users' perceptions of the IDE's usability and educational impact,' and Section 6.2 concedes 'it is not possible to perform a quantitative evaluation, as projects are very different in nature.' These are validity limitations (self-report, no control condition, disjoint cohorts for the knowledge survey and the satisfaction survey), not circular reductions: the survey responses are an independent empirical input, not a restatement of the conclusion. The verification-time benchmark against external tools OFMC and ProVerif is self-contained. No circular step can be exhibited, so the score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no fitted numerical parameters, new forces, or new mathematical entities. Its load-bearing assumptions are the correctness of the underlying verification tools and compiler, and the validity of self-reported user feedback for evaluating effectiveness. The AnBx language and forwarding channels are prior work [37], not introduced here.

assumptions (4)
  • domain assumption Dolev-Yao attacker model: the adversary controls the network and can compose and decompose messages symbolically.
    Used as the threat model for the OFMC and ProVerif verification workflows described in Sections 3.4 and 4.
  • domain assumption OFMC is sound and complete; ProVerif is sound but may report false attacks.
    Stated in Section 3.4; the IDE's verification feedback is trusted to reflect protocol security.
  • domain assumption AnBx compiler translations to AnB, ProVerif, and Java preserve the protocol's security properties.
    The IDE pipeline relies on the compiler, described in Section 3.3 and reference [26], without re-verifying the compiler in this paper.
  • ad hoc to paper Survey respondents' self-assessments and ratings are accurate.
    Section 6.4 explicitly depends on the accuracy of self-assessment surveys for the user evaluation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols." pith.science (2026). https://pith.science/paper/N5KWYJPV

@misc{pith2026241117926,
  author       = {Pith},
  title        = {Pith review of: A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/N5KWYJPV}},
  note         = {Machine review of arXiv:2411.17926}
}
read the original abstract

To develop trustworthy distributed systems, verification techniques and formal methods, including lightweight and practical approaches, have been employed to certify the design or implementation of security protocols. Lightweight formal methods offer a more accessible alternative to traditional fully formalised techniques by focusing on simplified models and tool support, making them more applicable in practical settings. The technical advantages of formal verification over manual testing are increasingly recognised in the cybersecurity community. However, for practitioners, formal modelling and verification are often too complex and unfamiliar to be used routinely. In this paper, we present an Eclipse IDE for the design, verification, and implementation of security protocols and evaluate its effectiveness, including feedback from users in educational settings. It offers user-friendly assistance in the formalisation process as part of a Model-Driven Development approach. This IDE centres around the Alice & Bob (AnB) notation, the AnBx Compiler and Code Generator, the OFMC model checker, and the ProVerif cryptographic protocol verifier. For the evaluation, we identify the six most prominent limiting factors for formal method adoption, based on relevant literature in this field, and we consider the IDE's effectiveness against those criteria. Additionally, we conducted a structured survey to collect feedback from university students who have used the toolkit for their projects. The findings demonstrate that this contribution is valuable as a workflow aid and helps users grasp essential cybersecurity concepts, even for those with limited knowledge of formal methods or cryptography. Crucially, users reported that the IDE has been an important component to complete their projects and that they would use again in the future, given the opportunity.

Figures

Figures reproduced from arXiv: 2411.17926 by the authors.

Figure 1
Figure 1. AnBx Protocol Example noted that this setting is also more efficient, as symmetric encryption is notoriously faster than the asymmetric one. The Types section includes declarations of identifiers of different types and functions dec￾larations, while the section Knowledge denotes the initial knowledge of each agent. Optional sections, Definitions and Equations, can be used respectively to specify macros with parame￾t… view at source ↗
Figure 2
Figure 2. AnB Protocol Example can also be translated into low level goals suitable for verification with various tools. Supported goals are: 1) Weak Authentication goals have the form B weakly authenticates A on Msg and are defined in terms of non-injective agreement [61]; 2) Authentication goals have the form B authenticates A on Msg and are defined in terms of injective agreement on the runs of the protocol, assessing the … view at source ↗
Figure 3
Figure 3. AnBx Compiler back-end (adapted from [26]) Following this, the sequence of actions can be reordered into an optimised executable narra￾tion (Opt-ExecNarr) using optimisation techniques such as common sub-expression elimination (CSE). This optimisation minimises the number of cryptographic operations and reduces overall execution time. The Java code generation requires an additional step, as illustrated in [PITH_FUL… view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Model Driven Development with the AnBx IDE ( manual automatic) workflow, as well as supporting users with early warnings, error messages, and suggestions to identify, correct, and prevent mistakes. While every step in this process would typically have to be performed m…
Figure 5
Figure 5. Figure 5: Control and visualisation over the modelling and verification process with the [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]
Figure 6
Figure 6. Figure 6: Tracking declarations with ProVerif scoping [PITH_FULL_IMAGE:figures/full_fig_p017_6.png]
Figure 7
Figure 7. Figure 7: Error message and quick fix [PITH_FULL_IMAGE:figures/full_fig_p019_7.png]
Figure 9
Figure 9. Figure 9: AnBxC dialog is orchestrated by an Ant file, a standard build file for the Eclipse platform and other IDEs. Alternatively, the associated Java project can be opened in Eclipse, where users can manually run its Ant build file. Observing the execution trace at a concrete…
Figure 10
Figure 10. Figure 10: View of verification results 5.2.7. Scheduling with priorities and Task manager As users launch many tasks, the order of execution needs to be considered for productivity. The tasks are organised in a queue, and we implement a priority policy for the waiting tasks. A …
Figure 11
Figure 11. Figure 11: Task manager window If a task is killed, this fact is reported in the console next to its running time. This feature can be particularly useful, for example, when console outputs are logged. The maximum number of concurrent tasks can be set in the configuration window…
Figure 12
Figure 12. Figure 12: Eclipse Marketplace statistics for the AnBx IDE (01/2018 – 10/2024) Poland, the United Kingdom, the United States, China, Italy, France, Spain, Russia, India, Bulgaria, and Denmark, among others. 6.4. Assumptions and Limitations The analysis and evaluation of the IDE …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

144 extracted references · 57 canonical work pages

  1. [1]

    Garcia, P

    R. Garcia, P. Modesti, A practical approach to formal methods: An Eclipse integrated development environment (IDE) for security protocols, Electronics 13 (23) (2024).doi: 10.3390/electronics13234660

    work page doi:10.3390/electronics13234660 2024

  2. [2]

    Vanhoef, F

    M. Vanhoef, F. Piessens, Key reinstallation attacks: Forcing nonce reuse in WPA2, in: B. Thuraisingham, D. Evans, T. Malkin, D. Xu (Eds.), Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dal- las, TX, USA, October 30 - November 03, 2017, ACM, 2017, pp. 1313–1328. doi: 10.1145/3133956.3134027

    arXiv 2017

  3. [3]

    Cassidy, Diagnosis of the OpenSSL Heartbleed Bug, available online: https:// www.seancassidy.me/diagnosis-of-the-openssl-heartbleed-bug.html (accessed on 22 November 2024) (2014)

    S. Cassidy, Diagnosis of the OpenSSL Heartbleed Bug, available online: https:// www.seancassidy.me/diagnosis-of-the-openssl-heartbleed-bug.html (accessed on 22 November 2024) (2014)

    2014

  4. [4]

    Fogel, S

    B. Fogel, S. Farmer, H. Alkofahi, A. Skjellum, M. Hafiz, POODLEs, More POODLEs, FREAK Attacks Too: How Server Administrators Responded to Three Serious Web Vulnerabilities, Springer International Publishing, 2016, pp. 122–137. doi:10.1007/ 978-3-319-30806-7_8

    2016

  5. [5]

    E. S. Alashwali, K. Rasmussen, What’s in a Downgrade? A Taxonomy of Downgrade Attacks in the TLS Protocol and Application Protocols Using TLS, Springer International Publishing, 2018, pp. 468–487.doi:10.1007/978-3-030-01704-0_27

    work page doi:10.1007/978-3-030-01704-0_27 2018

  6. [6]

    Cremers, M

    C. Cremers, M. Horvat, S. Scott, T. van der Merwe, Automated analysis and verification of tls 1.3: 0-rtt, resumption and delayed authentication, in: 2016 IEEE Symposium on Security and Privacy (SP), IEEE, 2016.doi:10.1109/sp.2016.35

    doi:10.1109/sp.2016.35 2016

  7. [7]

    Bhargavan, B

    K. Bhargavan, B. Blanchet, N. Kobeissi, Verified models and reference implementations for the TLS 1.3 standard candidate, in: 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, IEEE Computer Society, 2017, pp. 483–502. doi:10.1109/SP.2017.26

    doi:10.1109/sp.2017.26 2017

  8. [8]

    Blanchet, Composition theorems for cryptoverif and application to TLS 1.3 (2018) 16– 30doi:10.1109/csf.2018.00009

    B. Blanchet, Composition theorems for cryptoverif and application to TLS 1.3 (2018) 16– 30doi:10.1109/csf.2018.00009

    arXiv 2018

Show all 144 references
  1. [9]

    K.Cohn-Gordon, C.Cremers, B.Dowling, L.Garratt, D.Stebila, Aformalsecurityanalysis of the signal messaging protocol, J. Cryptol. 33 (4) (2020) 1914–1983. doi:10.1007/ S00145-020-09360-1. 35

    2020

  2. [10]

    Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: Com- puter Security Foundations Workshop, IEEE, IEEE Computer Society, 2001, pp

    B. Blanchet, An efficient cryptographic protocol verifier based on Prolog rules, in: Com- puter Security Foundations Workshop, IEEE, IEEE Computer Society, 2001, pp. 0082–

    2001

  3. [11]

    Meier, B

    S. Meier, B. Schmidt, C. Cremers, D. A. Basin, The TAMARIN prover for the symbolic analysis of security protocols, in: N. Sharygina, H. Veith (Eds.), Computer Aided Verifi- cation - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19,

    2013

  4. [12]

    Basin, S

    D. Basin, S. Mödersheim, L. Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security 4 (3) (2005) 181–208. doi: 10.1007/s10207-004-0055-7

    2005 doi

  5. [13]

    M.Dark, S.Belcher, M.Bishop, I.Ngambeki, Practice, practice, practice...secureprogram- mer!, in: Proceeding of the 19th Colloquium for Information System Security Education, 2015

    2015

  6. [14]

    NIST, Cve-2020-13777, available online: https://nvd.nist.gov/vuln/detail/ CVE-2020-13777/ (accessed on 22 November 2024) (2020)

    2020

  7. [15]

    Garavel, M

    H. Garavel, M. H. ter Beek, J. van de Pol, The 2020 expert survey on formal methods, in: M. H. ter Beek, D. Nickovic (Eds.), Formal Methods for Industrial Critical Systems - 25th InternationalConference, FMICS2020, Vienna, Austria, September2-3, 2020, Proceedings, Vol. 12327 o...

    2020

  8. [16]

    Kulik, B

    T. Kulik, B. Dongol, P. G. Larsen, H. D. Macedo, S. Schneider, P. W. V. Tran-Jørgensen, J. Woodcock, A survey of practical formal methods for security, Formal Aspects Comput. 34 (1) (2022) 1–39.doi:10.1145/3522582

    2022 doi

  9. [17]

    Dolev, A

    D. Dolev, A. Yao, On the security of public-key protocols, IEEE Transactions on Informa- tion Theory 2 (29) (1983).doi:10.1109/tit.1983.1056650

    1983

  10. [18]

    Sommerville, Software Engineering, 9th edition, Addison-Wesley, 2010

    I. Sommerville, Software Engineering, 9th edition, Addison-Wesley, 2010

    2010

  11. [19]

    Bugliesi, R

    M. Bugliesi, R. Focardi, Language based secure communication, in: Computer Security Foundations Symposium, 2008. CSF’08. IEEE 21st, 2008, pp. 3–16.doi:10.1109/csf. 2008.17

    2008 doi

  12. [20]

    Avalle, A

    M. Avalle, A. Pironti, R. Sisto, Formal verification of security protocol implementa- tions: a survey, Formal Aspects of Computing 26 (1) (2014) 99–123. doi:10.1007/ s00165-012-0269-9

    2014

  13. [21]

    J. A. Davis, M. Clark, D. Cofer, A. Fifarek, J. Hinchman, J. Hoffman, B. Hulbert, S. P. Miller, L. Wagner, Study on the Barriers to the Industrial Adoption of Formal Methods, Springer Berlin Heidelberg, 2013, pp. 63–77.doi:10.1007/978-3-642-41010-9_5

    2013 doi

  14. [22]

    Skevoulis, V

    S. Skevoulis, V. Makarov, Integrating formal methods tools into undergraduate computer science curriculum, in: Proceedings. Frontiers in Education. 36th Annual Conference, IEEE, 2006, pp. 1–6.doi:10.1109/fie.2006.322570

    2006

  15. [23]

    Scheurer, Formal Methods: The Problem Is Education, Springer Berlin Heidelberg, 2000, pp

    T. Scheurer, Formal Methods: The Problem Is Education, Springer Berlin Heidelberg, 2000, pp. 198–210. doi:10.1007/3-540-40891-6_18. 36

    2000 doi

  16. [24]

    Pomorova, S

    O. Pomorova, S. Lysenko, Formal and intelligent methods for security and resilience: Ed- ucation and training issues, Information & Security: An International Journal 35 (2016) 133–150. doi:10.11610/isij.3507

    2016 doi

  17. [25]

    Avalle, A

    M. Avalle, A. Pironti, D. Pozza, R. Sisto, JavaSPI: A framework for security protocol implementation, International Journal of Secure Software Engineering 2 (4) (2011) 34–48. doi:10.4018/jsse.2011100103

    2011 doi

  18. [26]

    Modesti, AnBx: Automatic generation and verification of security protocols implemen- tations, in: 8th International Symposium on Foundations & Practice of Security, Vol

    P. Modesti, AnBx: Automatic generation and verification of security protocols implemen- tations, in: 8th International Symposium on Foundations & Practice of Security, Vol. 9482 of LNCS, Springer, 2015, pp. 156–173.doi:10.1007/978-3-319-30303-1_10

    2015 doi

  19. [27]

    Almousa, S

    O. Almousa, S. Mödersheim, L. Viganò, Alice and Bob: Reconciling formal models and implementation, in: C. Bodei, G.-L. Ferrari, C. Priami (Eds.), Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th B...

    2015 doi

  20. [28]

    D. J. J. Wing, Lightweight formal methods, H. Saiedian. An invitation to formal methods. IEEE Computer (1996). doi:10.1007/3-540-45251-6_1

    1996 doi

  21. [29]

    Zamansky, M

    A. Zamansky, M. Spichkova, G. Rodríguez-Navas, P. Herrmann, J. O. Blech, Towards classification of lightweight formal methods, in: E. Damiani, G. Spanoudakis, L. A. Ma- ciaszek (Eds.), Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Softwa...

    2018 doi

  22. [30]

    A. D. Brucker, D. Marmsoler, Teaching Formal Methods in Application Domains: A Case Study in Computer and Network Security, Springer Nature Switzerland, 2024, pp. 124–140. doi:10.1007/978-3-031-71379-8_8

    2024 doi

  23. [31]

    Brambilla, J

    M. Brambilla, J. Cabot, M. Wimmer, Model-Driven Software Engineering in Practice, Sec- ond Edition, Synthesis Lectures on Software Engineering, Morgan & Claypool Publishers,

  24. [32]

    P. H. Nguyen, M. E. Kramer, J. Klein, Y. L. Traon, An extensive systematic review on the model-driven development of secure systems, Inf. Softw. Technol. 68 (2015) 62–81. doi:10.1016/J.INFSOF.2015.08.006

    2015 doi

  25. [33]

    Garcia, P

    R. Garcia, P. Modesti, An IDE for the design, verification and implementation of security protocols, in: 2017 IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2017, Toulouse, France, October 23-26, 2017, IEEE Com- puter Society, 2017,...

    2017 doi

  26. [34]

    Bettini, Implementing domain-specific languages with Xtext and Xtend, Packt Publish- ing Ltd, 2016

    L. Bettini, Implementing domain-specific languages with Xtext and Xtend, Packt Publish- ing Ltd, 2016

    2016

  27. [35]

    Eclipse Community, Xtext documentation, available online:http://eclipse.org/Xtext/ documentation/ (accessed on 22 November 2024)

    2024

  28. [36]

    S. Mödersheim, Algebraic properties in alice and bob notation, in: Proceedings of the The Forth International Conference on Availability, Reliability and Security, ARES 2009, March 16-19, 2009, Fukuoka, Japan, IEEE Computer Society, 2009, pp. 433–440.doi: 10.1109/ARES.2009.95. 37

    2009 doi

  29. [37]

    Bugliesi, S

    M. Bugliesi, S. Calzavara, S. Mödersheim, P. Modesti, Security protocol specification and verification with anbx, Journal of Information Security and Applications 30 (2016) 46–63. doi:10.1016/j.jisa.2016.05.004

    2016 doi

  30. [38]

    Blanchet, V

    B. Blanchet, V. Cheval, V. Cortier, ProVerif with Lemmas, Induction, Fast Subsumption, and Much More, in: 43RD IEEE Symposium on Security and Privacy (S&P’22), San Francisco, United States, 2022.doi:10.1109/sp46214.2022.9833653

    2022

  31. [39]

    Shaukat, A

    R. Shaukat, A. Shahoor, A. Urooj, Probing into code analysis tools: A comparison of C# supporting static code analyzers, in: 2018 15th International Bhurban Conference on Applied Sciences and Technology (IBCAST), 2018, pp. 455–464.doi:10.1109/IBCAST. 2018.8312264

    2018

  32. [40]

    Fetaji, S

    M. Fetaji, S. Loskovska, B. Fetaji, M. Ebibi, Combining virtual learning environment and integrated development environment to enhance e-learning, in: 2007 29th International Conference on Information Technology Interfaces, 2007, pp. 319–324.doi:10.1109/ITI. 2007.4283790

    2007

  33. [41]

    M. Broy, A. Brucker, A. Fantechi, M. Gleirscher, K. Havelund, M. A. Kuppe, A. Mendes, A. Platzer, J. Ringert, A. Sullivan, Does every computer scientist need to know formal methods?, Form. Asp. Comput.Just Accepted (Jun. 2024).doi:10.1145/3670795

    2024 doi

  34. [42]

    Gleirscher, D

    M. Gleirscher, D. Marmsoler, Formal methods in dependable systems engineering: a survey of professionals from europe and north america, Empir. Softw. Eng. 25 (6) (2020) 4473–

    2020

  35. [43]

    J. M. Spivey, Z Notation - a reference manual (2. ed.), Prentice Hall International Series in Computer Science, Prentice Hall, 1992

    1992

  36. [44]

    B. J. Wadsworth, Piaget’s Theory of Cognitive and Affective Development: Foundations of Constructivism, Longman Publishing, 1996

    1996

  37. [45]

    J. S. Bruner, The Process of Education, Harvard University Press, 2009.doi:10.2307/j. ctvk12qst

    2009 doi

  38. [46]

    Raimondo, S

    M. Raimondo, S. Marrone, S. Bernardi, A. Palladino, Demonstrating the necessity of model generation in security protocol verification, in: 28th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2023, Sinaia, Romania, September 12-15, 2023, IEE...

    2023

  39. [47]

    L. C. Paulson, T. Nipkow, M. Wenzel, From LCF to isabelle/hol, Formal Aspects Comput. 31 (6) (2019) 675–698.doi:10.1007/S00165-019-00492-1

    2019 doi

  40. [48]

    Abadi, R

    M. Abadi, R. Needham, Prudent engineering practice for cryptographic protocols, in: 1994 IEEE Computer Society Symposium on Research in Security and Privacy, 1994. Proceed- ings., 1994, pp. 122–136.doi:10.1109/32.481513

    1994 doi

  41. [49]

    K. R. M. Leino, V. Wüstholz, The dafny integrated development environment, in: C. Dubois, D. Giannakopoulou, D. Méry (Eds.), Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014, Vol. 149 of EPTCS, 2014, pp. 3–15.do...

    2014 doi

  42. [50]

    Unwin, H

    A. Unwin, H. Hofmann, Gui and command-line - conflict or synergy?, in: K. Berk, M. Pourahmadi (Eds.), Proceedings of the 31st Symposium on the Interface: models, predictions, and computing, Schaumburg, Illinois, June 9 - 12, 1999, Computing science and statistics, Interface Fo...

    1999

  43. [51]

    Tabassum, S

    M. Tabassum, S. Watson, H. R. Lipford, Comparing educational approaches to secure programming: Tool vs. TA, in: Thirteenth Symposium on Usable Privacy and Security, SOUPS 2017, Santa Clara, CA, USA, July 12-14, 2017, USENIX Association, 2017. URL https://www.usenix.org/confere...

    2017

  44. [52]

    Kuusinen, Software developers as users: Developer experience of a cross-platform in- tegrated development environment, in: P

    K. Kuusinen, Software developers as users: Developer experience of a cross-platform in- tegrated development environment, in: P. Abrahamsson, L. Corral, M. Oivo, B. Russo (Eds.), Product-Focused Software Process Improvement - 16th International Conference, PROFES2015, Bolzano,...

    2015 doi

  45. [53]

    Lindmeier, A

    A. Lindmeier, A. Mühling, Keeping secrets: K-12 students’ understanding of cryptography, in: T. Brinda, M. Armoni (Eds.), WiPSCE ’20: Workshop in Primary and Secondary Computing Education, Virtual Event, Germany, October 28-30, 2020, ACM, 2020, pp. 14:1–14:10. doi:10.1145/3421...

    2020

  46. [54]

    J. Geels, Ordinary users do not understand digital signatures, in: Proceedings of the 13th Nordic Conference on Human-Computer Interaction, NordiCHI 2024, Uppsala, Sweden, October 13-16, 2024, ACM, 2024, pp. 66:1–66:15.doi:10.1145/3679318.3685402

    2024

  47. [55]

    A. M. Braga, R. Dahab, N. Antunes, N. Laranjeiro, M. Vieira, Understanding how to use static analysis tools for detecting cryptography misuse in software, IEEE Trans. Reliab. 68 (4) (2019) 1384–1403.doi:10.1109/TR.2019.2937214

    2019

  48. [56]

    Gleirscher, S

    M. Gleirscher, S. Foster, J. Woodcock, New opportunities for integrated formal methods, ACM Comput. Surv. 52 (6) (2020) 117:1–117:36.doi:10.1145/3357231

    2020 doi

  49. [57]

    R. J. van Glabbeek, P. Höfner, D. van der Wal, Analysing awn-specifications using mcrl2 (extended abstract), in: C. A. Furia, K. Winter (Eds.), Integrated Formal Methods - 14th InternationalConference, IFM2018, Maynooth, Ireland, September5-7, 2018, Proceedings, Vol. 11023 of ...

    2018 doi

  50. [58]

    Runge, I

    T. Runge, I. Schaefer, L. Cleophas, T. Thüm, D. G. Kourie, B. W. Watson, Tool support for correctness-by-construction, in: A. Koziolek, I. Schaefer, C. Seidl (Eds.), Software Engineering 2021, Fachtagung des GI-Fachbereichs Softwaretechnik, 22.-26. Februar 2021, Braunschweig/V...

    2021

  51. [59]

    Fares, J

    E. Fares, J. Bodeveix, M. Filali, Correct pattern-based development through refinements and weakest preconditions calculus, in: D. Marmsoler, M. Sun (Eds.), Formal Aspects of Component Software - 20th International Conference, FACS 2024, Milan, Italy, September 9-10, 2024, Pro...

    2024 doi

  52. [60]

    Bonfanti, M

    S. Bonfanti, M. Carissoni, A. Gargantini, A. Mashkoor, Asm2c++: A tool for code gener- ation from abstract state machines to arduino, in: C. W. Barrett, M. D. Davies, T. Kahsai 39 (Eds.), NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May ...

    2017 doi

  53. [61]

    Lowe, A hierarchy of authentication specifications, in: CSFW’97, IEEE Computer Society Press, 1997, pp

    G. Lowe, A hierarchy of authentication specifications, in: CSFW’97, IEEE Computer Society Press, 1997, pp. 31–43

    1997

  54. [62]

    J. P. Galeotti, C. A. Furia, E. May, G. Fraser, A. Zeller, Automating full functional verification of programs with loops, CoRR abs/1407.5286 (2014). arXiv:1407.5286, doi:10.48550/arxiv.1407.5286

    2014 doi arXiv

  55. [63]

    Barbosa, G

    M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao, B. Parno, Sok: Computer-aided cryptography, in: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, IEEE, 2021, pp. 777–795.doi:10.1109/ SP40001.2021.00008

    2021

  56. [64]

    Team, Avispa v1.0 user manual, available online:https://people.rennes.inria.fr/ Thomas.Genet/Crypt/AVISPA_manual.pdf (accessed on 22 November 2024)

    A. Team, Avispa v1.0 user manual, available online:https://people.rennes.inria.fr/ Thomas.Genet/Crypt/AVISPA_manual.pdf (accessed on 22 November 2024)

    2024

  57. [65]

    Delaune, L

    S. Delaune, L. Hirschi, A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols, Journal of Logical and Algebraic Methods in Pro- gramming 87 (2017) 127–144.doi:10.1016/j.jlamp.2016.10.005

    2017 doi

  58. [66]

    Blanchet, B

    B. Blanchet, B. Smyth, V. Cheval, ProVerif 2.05: Automatic cryptographic protocol veri- fier, user manual and tutorial, available online:https://bblanche.gitlabpages.inria. fr/proverif/manual.pdf (accessed on 22 November 2024) (2023)

    2023

  59. [67]

    Carlsen, Optimal privacy and authentication on a portable communications system, ACM SIGOPS Oper

    U. Carlsen, Optimal privacy and authentication on a portable communications system, ACM SIGOPS Oper. Syst. Rev. 28 (3) (1994) 16–23.doi:10.1145/182110.182112

    1994

  60. [68]

    compute.dtu.dk/~samo/ (accessed on 22 November 2024)

    Sebastian Mödersheim, OFMC distribution and tutorials, available online:https://www2. compute.dtu.dk/~samo/ (accessed on 22 November 2024)

    2024

  61. [69]

    ITU-T Recommendation H.530: Symmetric Security Procedures for H.510 (Mobility for H.323 Multimedia Systems and Services) (2002)

    2002

  62. [70]

    Kaufman, Internet key exchange (IKEv2) protocol, Tech

    C. Kaufman, Internet key exchange (IKEv2) protocol, Tech. rep. (2005)

    2005

  63. [71]

    S. International Organization for Standardization, Genève, ISO/IEC 9798-2:2008, Infor- mation technology – Security techniques – Entity Authentication – Part 2: Mechanisms using symmetric encipherment algorithms, Third edition (2008)

    2008

  64. [72]

    S. International Organization for Standardization, Genève, ISO/IEC 9798-4:1999, Infor- mation technology – Security techniques – Entity Authentication – Part 3: Mechanisms using a cryptographic check function, Second edition (1999)

    1999

  65. [73]

    Concepts Tools 17 (3) (1996) 93–102.doi:10.1007/3-540-61042-1_43

    G.Lowe, Breakingandfixingtheneedham-schroederpublic-keyprotocolusingFDR,Softw. Concepts Tools 17 (3) (1996) 93–102.doi:10.1007/3-540-61042-1_43

    1996 doi

  66. [74]

    R. M. Needham, M. D. Schroeder, Using encryption for authentication in large networks of computers, Commun. ACM 21 (12) (1978) 993–999.doi:10.1145/359657.359659

    1978

  67. [75]

    D. J. Otway, O. Rees, Efficient and timely mutual authentication, ACM SIGOPS Oper. Syst. Rev. 21 (1) (1987) 8–10.doi:10.1145/24592.24594. 40

    1987

  68. [76]

    L. C. Paulson, Inductive analysis of the internet protocol TLS, ACM Trans. Inf. Syst. Secur. 2 (3) (1999) 332–351.doi:10.1145/322510.322530

    1999

  69. [77]

    T. Y. Woo, S. S. Lam, Authentication for distributed systems, Computer 25 (1) (1992) 39–52. doi:10.1109/2.108052

    1992 doi

  70. [78]

    L. C. Paulson, The yahalom protocol, in: Security Protocols: 7th International Workshop, Cambridge, UK, April 19-21, 1999. Proceedings 7, Springer, 2000, pp. 78–84. doi:10. 1007/10720107_11

    1999

  71. [79]

    Garcia, P

    R. Garcia, P. Modesti, Automatic generation of security protocols attacks specifications and implementations, Cyber Security and Applications 2 (2024) 100038.doi:10.1016/j. csa.2024.100038

    2024

  72. [80]

    Likert, A technique for the measurement of attitudes., Archives of psychology (1932)

    R. Likert, A technique for the measurement of attitudes., Archives of psychology (1932)

    1932

  73. [81]

    L. A. Clark, D. Watson, Constructing validity: New developments in creating objective measuring instruments., Psychological assessment 31 (12) (2019) 1412. doi:10.1037/ pas0000626

    2019

  74. [82]

    doi:10.1109/csfw.2001.930138

    2001

  75. [83]

    Modesti, Integrating formal methods for security in software security education, Infor- matics in Education 19 (3) (2020) 425–454.doi:10.15388/infedu.2020.19

    P. Modesti, Integrating formal methods for security in software security education, Infor- matics in Education 19 (3) (2020) 425–454.doi:10.15388/infedu.2020.19

    2020 doi

  76. [84]

    K. R. M. Leino, Dafny: An automatic program verifier for functional correctness, in: E. M. Clarke, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected...

    2010 doi

  77. [85]

    Brezocnik, B

    Z. Brezocnik, B. Vlaovic, A. Vreze, Spinrcp: the eclipse rich client platform integrated development environment for the spin model checker, in: N. Rungta, O. Tkachuk (Eds.), 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA,...

    2014 doi

  78. [86]

    G. J. Holzmann, The SPIN Model Checker - primer and reference manual, Addison-Wesley, 2004

    2004

  79. [87]

    org, [Online; accessed 14 October 2024] (2024)

    LimeSurvey Team, Limesurvey: an open source survey tool,https://www.limesurvey. org, [Online; accessed 14 October 2024] (2024)

    2024

  80. [88]

    S. Owre, J. M. Rushby, N. Shankar, PVS: A prototype verification system, in: D. Kapur (Ed.), Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, Vol. 607 of Lecture Notes in Computer Sci...

    1992 doi

  81. [89]

    Metere, L

    R. Metere, L. Arnaboldi, Metacp: Cryptographic protocol design tool for formal verifi- cation, CoRR abs/2105.09150 (2021). arXiv:2105.09150, doi:10.48550/arxiv.2105. 09150. 41

    2021 doi arXiv

  82. [90]

    Braghin, M

    C. Braghin, M. Lilli, E. Riccobene, M. Baba, Kant: A domain-specific language for mod- eling security protocols, in: F. J. D. Mayo, L. F. Pires, E. Seidewitz (Eds.), Proceedings of the 12th International Conference on Model-Based Software and Systems Engineering, MODELSWARD 20...

    2024 doi

  83. [91]

    Glouche, T

    Y. Glouche, T. Genet, O. Heen, O. Courtay, A security protocol animator tool for avispa, in: ARTIST2 workshop on security specification and verification of embedded systems, Pisa, 2006, pp. 1–7. URL https://people.irisa.fr/Thomas.Genet/span/

    2006

  84. [92]

    Masci, C

    P. Masci, C. A. Muñoz, An integrated development environment for the prototype verifica- tion system, in: R. Monahan, V. Prevosto, J. Proença (Eds.), Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019, Vol....

    2019 doi

  85. [93]

    Armando, D

    A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuéllar, P. H. Drielsma, P.-C. Héam, O. Kouchnarenko, J. Mantovani, et al., The AVISPA tool for the automated validation of internet security protocols and applications, in: Computer Aided Verification, Springer, ...

    2005 doi

  86. [94]

    doi:10.18420/SE2021_34

    doi

  87. [95]

    Lifepillar, Vim mode for formal languages, available online: https://github.com/ lifepillar/vim-formal-package (accessed on 22 November 2024)

    2024

  88. [96]

    B. F. Jorden Whitefield, Ralf Sasse, Sublime Text 3 plug-in for Tamarin, available on- line: https://github.com/tamarin-prover/editor-sublime (accessed on 22 November 2024)

    2024

  89. [97]

    Boichut, T

    Y. Boichut, T. Genet, Y. Glouche, O. Heen, Using animation to improve formal specifica- tions of security protocols, in: 2nd Conference on Security in Network Architectures and Information Systems (SARSSI 2007), 2007, pp. 169–182

    2007

  90. [98]

    Nicolas, V

    G. Nicolas, V. Cheval, ProVerif Syntax Highlighting for VS Code, available online:https: //marketplace.visualstudio.com/items?itemName=georgio.proverif-vscode (ac- cessed on 22 November 2024)

    2024

  91. [99]

    Rusinowitch, Automated analysis of security protocols, in: L

    M. Rusinowitch, Automated analysis of security protocols, in: L. Brim, O. Grumberg (Eds.), 12th International Workshop on Functional and Constraint Logic Programming, WFLP 2003, in connection with RDP’03, Federated Conference on Rewriting, Deduction and Programming, Boulder, C...

    2003 doi

  92. [100]

    de Ruiter, ProVerif Editor, available online:https://proverifeditor.sourceforge

    J. de Ruiter, ProVerif Editor, available online:https://proverifeditor.sourceforge. net/ (accessed on 22 November 2024)

    2024

  93. [101]

    78–94.doi:10.1109/csf.2012.25

    B.Schmidt, S.Meier, C.Cremers, D.Basin, AutomatedanalysisofDiffie-Hellmanprotocols and advanced security properties, in: Computer Security Foundations Symposium (CSF), 2012 IEEE 25th, IEEE, 2012, pp. 78–94.doi:10.1109/csf.2012.25. 42 Appendix A. AnBx IDE key features and requi...

    2012 doi

  94. [102]

    Malladi, B

    S. Malladi, B. Blanchet, ProVerif Web interface, available online:http://proverif20. paris.inria.fr/index.php (accessed on 22 November 2024)

    2024

  95. [104]

    Úlfur Jóhann Edvardsson, V. J. L. Hoffmann, OFMC-GUI, available online: https:// github.com/ulfur88/OFMC-GUI (accessed on 22 November 2024)

    2024

  96. [107]

    Open Eclipse and selectHelp→ Eclipse Marketplace

  97. [108]

    Search forAnBx, then selectAnBx IDEfrom the list and pressInstall

  98. [109]

    Alternatively, use the Eclipse Update Manager: • Open Help→ Install New Software..., add the following update site URL:https://www

    Ensure the update site is active for future updates by checkingHelp→ Install New Soft- ware...→ Manage..., and verifying that the update site is enabled. Alternatively, use the Eclipse Update Manager: • Open Help→ Install New Software..., add the following update site URL:http...

  99. [110]

    In Eclipse, selectAnBx Tools→ Configuration

  100. [111]

    • Config File: Path toanbxc.cfg

    Set the paths to: • AnBxC Exe Path: Path toanbxc.exe. • Config File: Path toanbxc.cfg. • ProVerif Exe Path: Path toproverif.exe. • OFMC Exe Path: Path toofmc.exe. Optionally, configure a folder for logging tool outputs via the configuration interface. Addi- tional details are ...

  101. [112]

    Selecting a protocol, such asFresh_From_A.AnBx, from thecasestudies folder

  102. [113]

    Clicking theAnBxC button on the toolbar

  103. [114]

    Choosing an output format (e.g.,AnB, ProVerif Typed, orJava)

  104. [115]

    Appendix B.5

    Observing the verification results in the Console view. Appendix B.5. Creating a New Project To create a new AnBx project:

  105. [116]

    Select File→ New→ Project→ AnBx Project

  106. [117]

    Create new AnBx/AnB files inside thesrc folder: File→ New→ Other→ AnBx file

  107. [118]

    44 Appendix B.6

    Similarly, create ProVerif files under thesrc folder: File→ New→ Other→ PV file. 44 Appendix B.6. Running Protocol Verification and Code Generation The output of verification or code generation will be displayed in theConsole view. If the Console is not visible: • Select Windo...

  108. [120]

    Choose the output formatAnB (default)and tickLaunch associated validator

  109. [121]

    • Specify the number of sessions (e.g., 1, 2, 3, etc.)

    (Only the first time) Configure OFMC: • Click on the icon. • Specify the number of sessions (e.g., 1, 2, 3, etc.). • If the session number (n) is greater than 1, the tool will sequentially verify the protocol for 1 session andn sessions. • Click OK

  110. [122]

    Appendix D.1.2

    The compiler will translate the file from.AnBx to .AnB and automatically run OFMC to verify the protocol against its specified security goals. Appendix D.1.2. Verifying .AnB or .IF Files

  111. [123]

    Select the .AnB or .IF file in Eclipse and click theOFMC button in the Eclipse toolbar

  112. [124]

    • If the session number (n) is greater than 1, the tool will sequentially verify the protocol for 1 session andn sessions

    Configure OFMC as follows: • Specify the number of sessions (e.g., 1, 2, 3, etc.). • If the session number (n) is greater than 1, the tool will sequentially verify the protocol for 1 session andn sessions

  113. [125]

    48 Figure D.19: ProVerif Protocol Verification Appendix D.2

    Click OK to begin the verification process. 48 Figure D.19: ProVerif Protocol Verification Appendix D.2. ProVerif Protocol Verification ProVerif is used to verify protocols specified in.AnBx or .PV files. It supports advanced verification of security goals using symbolic model...

  114. [126]

    Select the .AnBx file in Eclipse and click theAnBxC button in the Eclipse toolbar

  115. [127]

    Choose the output formatProVerif (default)and tickLaunch associated validator

  116. [128]

    • Options includepitype (process type inference) andsolve (solver for symbolic traces)

    (Optional) Configure ProVerif: • Click on the icon to set options for ProVerif. • Options includepitype (process type inference) andsolve (solver for symbolic traces)

  117. [129]

    The compiler will translate the file from.AnBx to .PV and automatically run ProVerif to verify the protocol against its specified security goals

    Click OK. The compiler will translate the file from.AnBx to .PV and automatically run ProVerif to verify the protocol against its specified security goals. Appendix D.2.2. Verifying .PV Files

  118. [130]

    Select the .PV file in Eclipse and click theProVerif button in the Eclipse toolbar

  119. [131]

    Configure the verification options: • Default options arepitype and solve

  120. [132]

    Appendix D.3

    Click OK to run ProVerif and verify the protocol. Appendix D.3. Notes on Verification • Verification results are displayed in the Eclipse console or associated output window. • If verification fails, inspect the error messages and ensure that the protocol and its config- urati...

  121. [133]

    Download and configure the Eclipse plug-in as described in Appendix B

  122. [134]

    Key parameters include: • pathstemplates: Location of the template files (.st)

    Ensure the configuration fileanbxc.cfg is correctly set up. Key parameters include: • pathstemplates: Location of the template files (.st). • pathjavadest: Path where the generated Java files will be stored

  123. [135]

    Appendix E.2

    Verify thatpathjavadest points to the source folder of your Java project in Eclipse (e.g., C:/JavaProjects/genAnBx/src/). Appendix E.2. Generating Java Code To generate Java code for an AnBx protocol file (e.g.,Fresh_From_A.AnBx) using Eclipse:

  124. [136]

    Open your Eclipse workspace

  125. [137]

    Click on theAnBxC button in the toolbar

  126. [138]

    Select the desired output format (Java for standard generation)

  127. [139]

    The generated files will include Java source files and a corresponding.properties configu- ration file for the protocol

    Press OK. The generated files will include Java source files and a corresponding.properties configu- ration file for the protocol. Appendix E.3. Setting Up and Running the Project in Eclipse To run the generated Java code in Eclipse:

  128. [140]

    • Specify a project name and location (e.g.,C:/JavaProjects/genAnBx)

    Create a New Java Project: • Navigate toFile→ New→ Project→ Java Project. • Specify a project name and location (e.g.,C:/JavaProjects/genAnBx). • Click Finish

  129. [141]

    • Navigate toJava Build Path→ Libraries

    Add the AnBxJ.jar Library: • Right-click on the project folder and selectProperties. • Navigate toJava Build Path→ Libraries. • If AnBxJ.jar is not listed, clickAdd External JARs...and select theAnBxJ.jar file

  130. [142]

    Ensure Proper Configuration: • Verify that thekeypath in anbxc.cfg points to the correct keystore location. • The default value for keystores is: 50 # Paths keypath = ../../keystore/ • Expand the keystore file into a folder at the same level as the src folder (e.g., C:/JavaPro...

  131. [143]

    • If you do not see the new files, refresh the folder to load them

    Generate and Import Code: • AftergeneratingJavacode, Thegeneratedfileswillappearunderthespecifiedprotocol folder (e.g., src/Prot for protocol Prot). • If you do not see the new files, refresh the folder to load them

  132. [144]

    • Otherwise, use thebuild.xml ant file generated alongside the Java code

    Run the Project: • If Run associated validatoris enabled (see Figure 9), the program will execute imme- diately after being built. • Otherwise, use thebuild.xml ant file generated alongside the Java code. • Right-click on thebuild.xml file and selectRun As→ Ant Build

  133. [145]

    • Check the console output for details on errors or missing dependencies

    If the application does not run as expected: • Refresh the workspace and rebuild the project. • Check the console output for details on errors or missing dependencies. Appendix F. Additional Features and Components Information about these features and components can be found i...

  134. [2013]

    8044 of Lecture Notes in Computer Science, Springer, 2013, pp

    Proceedings, Vol. 8044 of Lecture Notes in Computer Science, Springer, 2013, pp. 696–701. doi:10.1007/978-3-642-39799-8_48

    2013 doi

  135. [2017]

    doi:10.2200/S00751ED2V01Y201701SWE004

    doi

  136. [4546]

    doi:10.1007/S10664-020-09836-5

    doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.