afp-mirror
/
Automated_Stateful_Protocol_Verification
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 2 Wiki Activity
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.
3 Commits
1 Branch
350 KiB
 
 
 
 
 
 
Branch: master
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Automated_Stateful_Protocol.../CITATION

69 lines
4.0 KiB
Raw Permalink Blame History 

  1. To cite the use of this formal theory, please use

  2. 

  3.   Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and Anders Schlichtkrull. 

  4.   Automated Stateful Protocol Verification. In Archive of Formal Proofs, 2020. 

  5.   http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html, 

  6.   Formal proof development

  7. 

  8. A BibTeX entry for LaTeX users is

  9. 

  10. Article{ hess.ea:automated:2020,

  11. 	abstract= {In protocol verification we observe a wide spectrum from fully 

  12.                    automated methods to interactive theorem proving with proof 

  13.                    assistants like Isabelle/HOL. In this AFP entry, we present a 

  14.                    fully-automated approach for verifying stateful security protocols, 

  15.                    i.e., protocols with mutable state that may span several sessions. 

  16.                    The approach supports reachability goals like secrecy and 

  17.                    authentication. We also include a simple user-friendly 

  18.                    transaction-based protocol specification language that is embedded 

  19.                    into Isabelle.},

  20. 	author	= {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker and Anders Schlichtkrull},

  21. 	date	= {2020-04-08},

  22. 	file	= {https://www.brucker.ch/bibliography/download/2020/hess.ea-automated-outline-2020.pdf},

  23. 	filelabel= {Outline},

  24. 	issn	= {2150-914x},

  25. 	journal	= {Archive of Formal Proofs},

  26. 	month	= {apr},

  27. 	note	= {\url{http://www.isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html}, Formal proof development},

  28. 	pdf	= {https://www.brucker.ch/bibliography/download/2020/hess.ea-automated-2020.pdf},

  29. 	title	= {Automated Stateful Protocol Verification},

  30. 	url	= {https://www.brucker.ch/bibliography/abstract/hess.ea-automated-2020},

  31. 	year	= {2020},

  32. } 

  33. 

  34. An overview of the formalization is given in:

  35. 

  36.     Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, and

  37.     Anders Schlichtkrull. Performing Security Proofs of Stateful

  38.     Protocols. In 34th IEEE Computer Security Foundations Symposium

  39.     (CSF). IEEE, 2021.

  40.     https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019

  41. 

  42. A BibTeX entry for LaTeX users is

  43. 

  44. @InProceedings{ hess.ea:performing:2021,

  45.         abstract  = {In protocol verification we observe a wide spectrum from

  46.                      fully automated methods to interactive theorem proving with proof

  47.                      assistants like Isabelle/HOL. The latter provide overwhelmingly high

  48.                      assurance of the correctness, which automated methods often cannot:

  49.                      due to their complexity, bugs in such automated verification tools are

  50.                      likely and thus the risk of erroneously verifying a flawed protocol is

  51.                      non-negligible. There are a few works that try to combine advantages

  52.                      from both ends of the spectrum: a high degree of automation and

  53.                      assurance. We present here a first step towards achieving this for a

  54.                      more challenging class of protocols, namely those that work with a

  55.                      mutable long-term state. To our knowledge this is the first approach 

  56.                      that achieves fully automated verification of stateful protocols in an

  57.                      LCF-style theorem prover. The approach also includes a simple

  58.                      user-friendly transaction-based protocol specification language

  59.                      embedded into Isabelle, and can also leverage a number of existing

  60.                      results such as soundness of a typed model.},

  61.         author	  = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker and Anders Schlichtkrull},

  62. 	booktitle = {34th {IEEE} Computer Security Foundations Symposium (CSF)},

  63. 	location  = {June 21-25, 2021, Dubrovnik, Croatia},

  64. 	pdf	  = {https://www.brucker.ch/bibliography/download/2021/hess.ea-performing-2021.pdf},

  65. 	publisher = {{IEEE}},

  66. 	title	  = {Performing Security Proofs of Stateful Protocols},

  67. 	url	  = {https://www.brucker.ch/bibliography/abstract/hess.ea-performing-2021},

  68. 	year	  = {2021},

  69. }