{"entities":{"Q7361444":{"pageid":31519871,"ns":120,"title":"Item:Q7361444","lastrevid":105365879,"modified":"2026-10-07T13:36:19Z","type":"item","id":"Q7361444","labels":{"en":{"language":"en","value":"Compositional BD Security"}},"descriptions":{"en":{"language":"en","value":"AFP entry BD_Security_Compositional"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a3c28d4d50c6c5dab64ed33783769013184903a","datavalue":{"value":"https://isa-afp.org/entries/BD_Security_Compositional.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361444$8172B384-6574-46EF-B410-5D9A7C69B00A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"509f91048bfebeb2e3809071f1ccdd7172b43404","datavalue":{"value":{"time":"+2021-08-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361444$F7F182DB-9542-4204-A646-17F0602E9542","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"8c7403eacb8a704e0835924c65f70230d72a3d00","datavalue":{"value":"Thomas Bauereiss","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361444$071D38F2-7F8D-4780-B040-954FBB527DD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f94288ed91377510811411084214ae1d548d5352","datavalue":{"value":"Andrei Popescu","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361444$E08228CC-538E-48CE-AE91-4575133B8AB3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"433e2d45b9579592197eb2be7806a201101fa976","datavalue":{"value":{"text":"Compositional BD Security","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361444$426E747C-967E-4DC1-9523-A0E9432834AA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"aff314e02e3c8ec7c3751b00d35d322abefe137f","datavalue":{"value":"Building on a previous AFP entry that formalizes the Bounded-Deducibility Security (BD Security) framework [1] , we formalize compositionality and transport theorems for information flow security. These results allow lifting BD Security properties from individual components specified as transition systems, to a composition of systems specified as communicating products of transition systems. The underlying ideas of these results are presented in the papers [1] and [2] . The latter paper also describes a major case study where these results have been used: on verifying the CoSMeDis distributed social media platform (itself formalized as an AFP entry that builds on this entry).","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361444$0F41605C-CA77-4E3A-A33B-7762C94EC69B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8897cef3b5dbaa7fee186b5a3285858895dd349","datavalue":{"value":{"entity-type":"item","numeric-id":6157243,"id":"Q6157243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$A20F9DEB-D01B-4A17-B295-32F9A7C2DD4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"814fc2ca443592f0bbb786f393ee75a2d3c0432f","datavalue":{"value":{"entity-type":"item","numeric-id":2031419,"id":"Q2031419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$5689B5AC-E121-492C-90B0-3B7A27FE77D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e797aea5e7f8eb1db1a44340ba3d2896f82724f9","datavalue":{"value":{"entity-type":"item","numeric-id":2829248,"id":"Q2829248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$4B661EC5-7D1A-4CC8-9B9B-992B1BEE5F47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a29c5b1c25eb83699c48c019aa48478fe275a45","datavalue":{"value":{"entity-type":"item","numeric-id":1663221,"id":"Q1663221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$249016DA-7818-4276-8CDD-52684FB08B8C","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$BFC160CE-25E4-41DE-A9B8-8A3E03FABD12","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"3a7131a3860b6c8c8f535818ec86e97f90162fd0","datavalue":{"value":{"entity-type":"item","numeric-id":7361744,"id":"Q7361744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$D8AB66C4-F14C-4BD2-94B5-20ABE5672EDB","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ed082e42011d2ebbcbf36c06241a36f1d357174f","datavalue":{"value":{"entity-type":"item","numeric-id":7360801,"id":"Q7360801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$5A3F0898-BCE7-4A2B-8DE0-A2132135DACA","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361444$60DFB371-6026-44F0-BFCA-7654AA0233FB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Compositional BD Security","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Compositional_BD_Security"}}}}}