Isabelle/OFMC - Linking OFMC and Isabelle/HOL https://www.brucker.ch/projects/isabelle-ofmc/
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.
 
 
 
 

61 lines
2.8 KiB

  1. To cite ofmc-isabelle, please use
  2. Achim D. Brucker and Sebastian A. Mödersheim. Integrating Automated
  3. and Interactive Protocol Verification. In Workshop on Formal Aspects
  4. in Security and Trust (FAST 2009). Lecture Notes in Computer Science (5983),
  5. pages 248-262, Springer-Verlag , 2009.
  6. doi: 10.1007/978-3-642-12459-4_18
  7. A BibTeX entry for LaTeX users is
  8. @InCollection{ brucker.ea:integrating:2009,
  9. title = {Integrating Automated and Interactive Protocol
  10. Verification},
  11. author = {Achim D. Brucker and Sebastian A. M{\"o}dersheim},
  12. booktitle = {Workshop on Formal Aspects in Security and Trust (FAST
  13. 2009)},
  14. publisher = {Springer-Verlag},
  15. address = {Heidelberg},
  16. series = {Lecture Notes in Computer Science},
  17. number = {5983},
  18. categories = {isabelleofmc},
  19. pages = {248--262},
  20. doi = {10.1007/978-3-642-12459-4_18},
  21. editor = {Pierpaolo Degano and Joshua Guttman},
  22. year = {2009},
  23. classification= {workshop},
  24. keywords = {protocol verification, model-checking, theorem proving},
  25. areas = {security, formal methods},
  26. public = {yes},
  27. abstract = {A number of current automated protocol verification tools
  28. are based on abstract interpretation techniques and other
  29. over-approximations of the set of reachable states or
  30. traces. The protocol models that these tools employ are
  31. shaped by the needs of automated verification and require
  32. subtle assumptions. Also, a complex verification tool may
  33. suffer from implementation bugs so that in the worst case
  34. the tool could accept some incorrect protocols as being
  35. correct. These risks of errors are also present, but
  36. considerably smaller, when using an LCF-style theorem
  37. prover like Isabelle. The interactive security proof,
  38. however, requires a lot of expertise and time.
  39. We combine the advantages of both worlds by using the
  40. representation of the over-approx\-imated search space
  41. computed by the automated tools as a ``proof idea'' in
  42. Isabelle. Thus, we devise proof tactics for Isabelle that
  43. generate the correctness proof of the protocol from the
  44. output of the automated tools. In the worst case, these
  45. tactics fail to construct a proof, namely when the
  46. representation of the search space is for some reason
  47. incorrect. However, when they succeed, the correctness only
  48. relies on the basic model and the Isabelle core.},
  49. pdf = {https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009.pdf},
  50. note = {An extended version of this paper is available as IBM
  51. Research Technical Report, RZ3750.},
  52. filelabel = {Extended Version},
  53. file = {https://www.brucker.ch/bibliography/download/2009/brucker.ea-integrating-2009-b.pdf},
  54. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-integrating-2009}
  55. }