Local mirror of Automated Stateful Protocol Verification entry of the Archive of Formal Proofs (AFP).
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

69 lines
4.0 KiB

  1. To cite the use of this formal theory, please use
  2. Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull.
  3. Automated Stateful Protocol Verification. In Archive of Formal Proofs, 2020.
  4. http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html,
  5. Formal proof development
  6. A BibTeX entry for LaTeX users is
  7. Article{ hess.ea:automated:2020,
  8. abstract= {In protocol verification we observe a wide spectrum from fully
  9. automated methods to interactive theorem proving with proof
  10. assistants like Isabelle/HOL. In this AFP entry, we present a
  11. fully-automated approach for verifying stateful security protocols,
  12. i.e., protocols with mutable state that may span several sessions.
  13. The approach supports reachability goals like secrecy and
  14. authentication. We also include a simple user-friendly
  15. transaction-based protocol specification language that is embedded
  16. into Isabelle.},
  17. author = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker and Anders Schlichtkrull},
  18. date = {2020-04-08},
  19. file = {https://www.brucker.ch/bibliography/download/2020/hess.ea-automated-outline-2020.pdf},
  20. filelabel= {Outline},
  21. issn = {2150-914x},
  22. journal = {Archive of Formal Proofs},
  23. month = {apr},
  24. note = {\url{http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html}, Formal proof development},
  25. pdf = {https://www.brucker.ch/bibliography/download/2020/hess.ea-automated-2020.pdf},
  26. title = {Automated Stateful Protocol Verification},
  27. url = {https://www.brucker.ch/bibliography/abstract/hess.ea-automated-2020},
  28. year = {2020},
  29. }
  30. An overview of the formalization is given in:
  31. Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and
  32. Anders Schlichtkrull. Performing Security Proofs of Stateful
  33. Protocols. In 34th IEEE Computer Security Foundations Symposium
  34. (CSF). IEEE, 2021.
  35. https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019
  36. A BibTeX entry for LaTeX users is
  37. @InProceedings{ hess.ea:performing:2021,
  38. abstract = {In protocol verification we observe a wide spectrum from
  39. fully automated methods to interactive theorem proving with proof
  40. assistants like Isabelle/HOL. The latter provide overwhelmingly high
  41. assurance of the correctness, which automated methods often cannot:
  42. due to their complexity, bugs in such automated verification tools are
  43. likely and thus the risk of erroneously verifying a flawed protocol is
  44. non-negligible. There are a few works that try to combine advantages
  45. from both ends of the spectrum: a high degree of automation and
  46. assurance. We present here a first step towards achieving this for a
  47. more challenging class of protocols, namely those that work with a
  48. mutable long-term state. To our knowledge this is the first approach
  49. that achieves fully automated verification of stateful protocols in an
  50. LCF-style theorem prover. The approach also includes a simple
  51. user-friendly transaction-based protocol specification language
  52. embedded into Isabelle, and can also leverage a number of existing
  53. results such as soundness of a typed model.},
  54. author = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker and Anders Schlichtkrull},
  55. booktitle = {34th {IEEE} Computer Security Foundations Symposium (CSF)},
  56. location = {June 21-25, 2021, Dubrovnik, Croatia},
  57. pdf = {https://www.brucker.ch/bibliography/download/2021/hess.ea-performing-2021.pdf},
  58. publisher = {{IEEE}},
  59. title = {Performing Security Proofs of Stateful Protocols},
  60. url = {https://www.brucker.ch/bibliography/abstract/hess.ea-performing-2021},
  61. year = {2021},
  62. }