Changes

Summary

merged
Network_Security_Policy_Verification: new material by C. Diekmann

Changeset 8118:ba7944e84ef2 by lars hupel _lars.hupel@mytum.de_: merged
Changeset 8117:69e72fe773e6 by lars hupel _lars.hupel@mytum.de_: Network_Security_Policy_Verification: new material by C. Diekmann
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Distributed_WebApp.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Example.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Example_Forte14.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/I8_SSH_Landscape.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Imaginary_Factory_Network.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Impl_List_Playground.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Impl_List_Playground_ChairNetwork.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Impl_List_Playground_ChairNetwork_statefulpolicy_example.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Network_Security_Policy_Verification.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/SINVAR_Examples.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/Analysis_Tainting.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/METASINVAR_SystemBoundary.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPbasic.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPbasic_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPstrict.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPtrusted.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPtrusted_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_NoRefl_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_SecGwExt.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_SecGwExt_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Interface.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Library.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_generateCode.thy` (diff)