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.
38 lines
2.2 KiB
38 lines
2.2 KiB
To cite the use of this formal theory, please use
|
|
|
|
Andreas V. Hess, Sebastian Mödersheim, and Achim D. Brucker. Stateful
|
|
Protocol Composition and Typing. In Archive of Formal Proofs, 2020.
|
|
http://www.isa-afp.org/entries/tateful_Protocol_Composition_and_Typing.html,
|
|
Formal proof development
|
|
|
|
A BibTeX entry for LaTeX users is
|
|
@Article{ hess.ea:stateful:2020,
|
|
abstract= {We provide in this AFP entry several relative soundness
|
|
results for security protocols. In particular, we prove
|
|
typing and compositionality results for stateful protocols
|
|
(i.e., protocols with mutable state that may span several
|
|
sessions), and that focuses on reachability properties. Such
|
|
results are useful to simplify protocol verification by
|
|
reducing it to a simpler problem: Typing results give
|
|
conditions under which it is safe to verify a protocol in a
|
|
typed model where only "well-typed" attacks can occur whereas
|
|
compositionality results allow us to verify a composed protocol
|
|
by only verifying the component protocols in isolation. The
|
|
conditions on the protocols under which the results hold are
|
|
furthermore syntactic in nature allowing for full automation.
|
|
The foundation presented here is used in another entry to
|
|
provide fully automated and formalized security proofs of
|
|
stateful protocols.},
|
|
author = {Andreas V. Hess and Sebastian M{\"o}dersheim and Achim D. Brucker},
|
|
date = {2020-04-08},
|
|
file = {https://www.brucker.ch/bibliography/download/2020/hess.ea-stateful-outline-2020.pdf},
|
|
filelabel= {Outline},
|
|
issn = {2150-914x},
|
|
journal = {Archive of Formal Proofs},
|
|
month = {apr},
|
|
note = {\url{http://www.isa-afp.org/entries/tateful_Protocol_Composition_and_Typing.html}, Formal proof development},
|
|
pdf = {https://www.brucker.ch/bibliography/download/2020/hess.ea-stateful-2020.pdf},
|
|
title = {Stateful Protocol Composition and Typing},
|
|
url = {https://www.brucker.ch/bibliography/abstract/hess.ea-stateful-2020},
|
|
year = {2020},
|
|
}
|
|
|