Extended protocol model to support composition of more than two protocols…
66d4e5d44d29
Actions

Description

Extended protocol model to support composition of more than two protocols without
the need of re-labeling them, additional automated checks, tighter integration
of the stateful protocol model and the automated verification (PSPSP) tool.

Extended protocol model to support composition of more than two protocols…66d4e5d44d29Actions

Description

Details

Event Timeline

Changes (64)

rAFP66d4e5d44d29

thys/Automated_Stateful_Protocol_Verification/Eisbach_Protocol_Verification.thy

thys/Automated_Stateful_Protocol_Verification/Examples.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/KeyserverEx.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/introduction.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/manual.thy

thys/Automated_Stateful_Protocol_Verification/PSPSP.thy

thys/Automated_Stateful_Protocol_Verification/ROOT

thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy

thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy

thys/Automated_Stateful_Protocol_Verification/Term_Abstraction.thy

thys/Automated_Stateful_Protocol_Verification/Term_Implication.thy

thys/Automated_Stateful_Protocol_Verification/Term_Variants.thy

thys/Automated_Stateful_Protocol_Verification/Transactions.thy

thys/Automated_Stateful_Protocol_Verification/document/jedit-keyserver.png

thys/Automated_Stateful_Protocol_Verification/document/jedit-select-session.png

thys/Automated_Stateful_Protocol_Verification/document/lh-listings.sty

thys/Automated_Stateful_Protocol_Verification/document/root.bib

thys/Automated_Stateful_Protocol_Verification/document/root.tex

thys/Automated_Stateful_Protocol_Verification/examples/Keyserver.thy

thys/Automated_Stateful_Protocol_Verification/examples/Keyserver2.thy

thys/Automated_Stateful_Protocol_Verification/examples/Keyserver_Composition.thy

thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model03.thy

thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model07.thy

thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model09.thy

thys/Automated_Stateful_Protocol_Verification/trac/Makefile

thys/Automated_Stateful_Protocol_Verification/trac/bin/ml-lex-isa

thys/Automated_Stateful_Protocol_Verification/trac/bin/ml-yacc-isa

thys/Automated_Stateful_Protocol_Verification/trac/ml_yacc_lib.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac_fp_parser.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sig

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex

thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex.sml

thys/Automated_Stateful_Protocol_Verification/trac/trac_protocol_parser.thy

thys/Automated_Stateful_Protocol_Verification/trac/trac_term.thy

thys/Stateful_Protocol_Composition_and_Typing/Examples.thy

thys/Stateful_Protocol_Composition_and_Typing/Intruder_Deduction.thy

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Strands.thy

thys/Stateful_Protocol_Composition_and_Typing/Lazy_Intruder.thy

thys/Stateful_Protocol_Composition_and_Typing/Messages.thy

thys/Stateful_Protocol_Composition_and_Typing/Miscellaneous.thy

thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy

thys/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy

thys/Stateful_Protocol_Composition_and_Typing/ROOT

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Strands.thy

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy

thys/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy

thys/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy

thys/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy

thys/Stateful_Protocol_Composition_and_Typing/document/root.tex

thys/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy

thys/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy

Extended protocol model to support composition of more than two protocols…
66d4e5d44d29
Actions