afp-mirror
/
Stateful_Protocol_Composition_and_Typing
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 2 Wiki Activity
Local mirror of Stateful Protocol Composition and Typing 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.
4 Commits
1 Branch
463 KiB
 
 
Branch: master
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Stateful_Protocol_Compositi.../CITATION

39 lines
2.2 KiB
Raw Permalink Blame History 

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

  2. 

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

  4.   Protocol Composition and Typing. In Archive of Formal Proofs, 2020. 

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

  6.   Formal proof development

  7. 

  8. A BibTeX entry for LaTeX users is

  9. @Article{ hess.ea:stateful:2020,

  10. 	abstract= {We provide in this AFP entry several relative soundness 

  11.                    results for security protocols. In particular, we prove 

  12.                    typing and compositionality results for stateful protocols

  13.                    (i.e., protocols with mutable state that may span several

  14.                    sessions), and that focuses on reachability properties. Such

  15.                    results are useful to simplify protocol verification by 

  16.                    reducing it to a simpler problem: Typing results give 

  17.                    conditions under which it is safe to verify a protocol in a 

  18.                    typed model where only "well-typed" attacks can occur whereas 

  19.                    compositionality results allow us to verify a composed protocol

  20.                    by only verifying the component protocols in isolation. The 

  21.                    conditions on the protocols under which the results hold are 

  22.                    furthermore syntactic in nature allowing for full automation. 

  23.                    The foundation presented here is used in another entry to 

  24.                    provide fully automated and formalized security proofs of 

  25.                    stateful protocols.},

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

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

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

  29. 	filelabel= {Outline},

  30. 	issn	= {2150-914x},

  31. 	journal	= {Archive of Formal Proofs},

  32. 	month	= {apr},

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

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

  35. 	title	= {Stateful Protocol Composition and Typing},

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

  37. 	year	= {2020},

  38. }