Diffusion afp-devel 398749a3e273

New entry CoSMeDis
398749a3e273
Actions

Tags

None

Subscribers

None

Description

New entry CoSMeDis

Details

Provenance

Authored on

Parents

rAFPe6b510d24af4: New entry CoSMed

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rAFP398749a3e273: New entry CoSMeDis.Aug 18 2021, 6:16 PM

Changes (79)

Path

Size

metadata/

API_Network.thy

Automation_Setup.thy

Friend_Confidentiality

Friend_Intro.thy

Friend_Network.thy

Friend_Observation_Setup.thy

Friend_Openness.thy

Friend_State_Indistinguishability.thy

Friend_Value_Setup.thy

Friend_Request_Confidentiality

Friend_Request.thy

Friend_Request_All.thy

Friend_Request_Intro.thy

Friend_Request_Network.thy

Friend_Request_Value_Setup.thy

Outer_Friend_Confidentiality

Outer_Friend_Issuer.thy

Outer_Friend_Issuer_Observation_Setup.thy

Outer_Friend_Issuer_Openness.thy

Outer_Friend_Issuer_State_Indistinguishability.thy

Outer_Friend_Issuer_Value_Setup.thy

Outer_Friend.thy

Outer_Friend_All.thy

Outer_Friend_Intro.thy

Outer_Friend_Network.thy

Outer_Friend_Receiver.thy

Outer_Friend_Receiver_Observation_Setup.thy

Outer_Friend_Receiver_State_Indistinguishability.thy

Outer_Friend_Receiver_Value_Setup.thy

Post_Confidentiality

DYNAMIC_Post_COMPOSE2.thy

DYNAMIC_Post_ISSUER.thy

DYNAMIC_Post_Network.thy

DYNAMIC_Post_Value_Setup_ISSUER.thy

Independent_Posts

Independent_DYNAMIC_Post_ISSUER.thy

Independent_DYNAMIC_Post_Network.thy

Independent_DYNAMIC_Post_Value_Setup_ISSUER.thy

Independent_Post_Observation_Setup_ISSUER.thy

Independent_Post_Observation_Setup_RECEIVER.thy

Independent_Post_RECEIVER.thy

Independent_Post_Value_Setup_RECEIVER.thy

Independent_Posts_Network.thy

Post_COMPOSE2.thy

Post_ISSUER.thy

Post_Network.thy

Post_Observation_Setup_ISSUER.thy

Post_Observation_Setup_RECEIVER.thy

Post_RECEIVER.thy

Post_Unwinding_Helper_ISSUER.thy

Post_Unwinding_Helper_RECEIVER.thy

Post_Value_Setup_ISSUER.thy

Post_Value_Setup_RECEIVER.thy

Safety_Properties.thy

System_Specification.thy

BD_Security_Compositional.html

Fresh_Identifiers.html

statistics.html

rAFP398749a3e273

metadata/metadata

Loading...

thys/CoSMeDis/API_Network.thy

Loading...

thys/CoSMeDis/Automation_Setup.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_All.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_Intro.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_Network.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_Observation_Setup.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_Openness.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_State_Indistinguishability.thy

Loading...

thys/CoSMeDis/Friend_Confidentiality/Friend_Value_Setup.thy

Loading...

thys/CoSMeDis/Friend_Request_Confidentiality/Friend_Request.thy

Loading...

thys/CoSMeDis/Friend_Request_Confidentiality/Friend_Request_All.thy

Loading...

thys/CoSMeDis/Friend_Request_Confidentiality/Friend_Request_Intro.thy

Loading...

thys/CoSMeDis/Friend_Request_Confidentiality/Friend_Request_Network.thy

Loading...

thys/CoSMeDis/Friend_Request_Confidentiality/Friend_Request_Value_Setup.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Issuer/Outer_Friend_Issuer.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Issuer/Outer_Friend_Issuer_Observation_Setup.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Issuer/Outer_Friend_Issuer_Openness.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Issuer/Outer_Friend_Issuer_State_Indistinguishability.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Issuer/Outer_Friend_Issuer_Value_Setup.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Outer_Friend.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Outer_Friend_All.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Outer_Friend_Intro.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Outer_Friend_Network.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Receiver/Outer_Friend_Receiver.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Receiver/Outer_Friend_Receiver_Observation_Setup.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Receiver/Outer_Friend_Receiver_State_Indistinguishability.thy

Loading...

thys/CoSMeDis/Outer_Friend_Confidentiality/Receiver/Outer_Friend_Receiver_Value_Setup.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/DYNAMIC_Post_COMPOSE2.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/DYNAMIC_Post_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/DYNAMIC_Post_Network.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/DYNAMIC_Post_Value_Setup_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_DYNAMIC_Post_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_DYNAMIC_Post_Network.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_DYNAMIC_Post_Value_Setup_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_Post_Observation_Setup_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_Post_Observation_Setup_RECEIVER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_Post_RECEIVER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_Post_Value_Setup_RECEIVER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Independent_Posts/Independent_Posts_Network.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_All.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_COMPOSE2.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Intro.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Network.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Observation_Setup_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Observation_Setup_RECEIVER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_RECEIVER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Unwinding_Helper_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Unwinding_Helper_RECEIVER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Value_Setup_ISSUER.thy

Loading...

thys/CoSMeDis/Post_Confidentiality/Post_Value_Setup_RECEIVER.thy

Loading...

thys/CoSMeDis/Prelim.thy

Loading...

thys/CoSMeDis/ROOT

Loading...

thys/CoSMeDis/Safety_Properties.thy

Loading...

thys/CoSMeDis/System_Specification.thy

Loading...

thys/CoSMeDis/document/root.bib

Loading...

thys/CoSMeDis/document/root.tex

Loading...

thys/ROOTS

Loading...

web/entries/BD_Security_Compositional.html

Loading...

web/entries/CoSMeDis.html

Loading...

web/entries/Fresh_Identifiers.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...