{"entities":{"Q7361464":{"pageid":31519931,"ns":120,"title":"Item:Q7361464","lastrevid":105366656,"modified":"2026-10-07T13:36:41Z","type":"item","id":"Q7361464","labels":{"en":{"language":"en","value":"Automated Stateful Protocol Verification"}},"descriptions":{"en":{"language":"en","value":"AFP entry Automated_Stateful_Protocol_Verification"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4678fa40702807ba69573fa3946650a445898b8d","datavalue":{"value":"https://isa-afp.org/entries/Automated_Stateful_Protocol_Verification.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361464$B58D9E64-1E72-4F0B-BA1A-7DE8DEAEF942","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"26a75e2b82c7d52d04b09f73d9891a6078a1dc17","datavalue":{"value":{"time":"+2020-04-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361464$17E38A74-73B2-4E93-A215-88AA514530B7","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"0a04e91ca61d1f9430825f7e0638f0af88b90da3","datavalue":{"value":"Andreas V. Hess","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361464$2EAD3BFF-B4DD-4D2C-9B5E-F4D3C0800783","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"03836af65b01548df2a93de1057414c8215101e4","datavalue":{"value":"Sebastian M\u00f6dersheim","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361464$A8442603-4565-4B5A-B282-821B419587D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c321b6732f723699ff379c28a4499e7172aa303c","datavalue":{"value":"Achim D. Brucker","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361464$3398AC87-0E13-4A07-9F76-EE6F2052B185","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f19e42813e41b1b694ee6662dce0e445e8e41f4b","datavalue":{"value":"Anders Schlichtkrull","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361464$8BF1E2DF-6B57-443C-830F-DE29A672D6CF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b0061bfd3ffab8d79b875d88a315e9698a21cee5","datavalue":{"value":{"text":"Automated Stateful Protocol Verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361464$27F007A1-E159-4AD1-B5CA-08FDFBBA70DE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"29b10c0872e11b4b792353d61786d9e9ef088c4d","datavalue":{"value":"In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. In this AFP entry, we present a fully-automated approach for verifying stateful security protocols, i.e., protocols with mutable state that may span several sessions. The approach supports reachability goals like secrecy and authentication. We also include a simple user-friendly transaction-based protocol specification language that is embedded into Isabelle.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361464$1A9BC12C-6604-408C-B8AD-3699D5A69620","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d2506b3c837bc37c736af04d5b09c4242c35622","datavalue":{"value":{"entity-type":"item","numeric-id":2167741,"id":"Q2167741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361464$EB8DF951-FFE4-4ABF-8B5C-1BD0F3003886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361464$62F5AFBE-6CC5-4D43-9E7E-E89D09341732","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":"Q7361464$F731164C-4BC3-4534-94B8-51473261157D","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"538d96a7f010ab756164fbf1c36ca6c941d61f3a","datavalue":{"value":{"entity-type":"item","numeric-id":7361430,"id":"Q7361430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361464$376EB3D2-E8A9-4516-BB73-719DBE4099EF","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":"Q7361464$5B0F9E75-C34E-4CF5-9227-36EBA262F7D3","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":"Q7361464$B69CF9AF-E6E8-4252-BF9E-D16D665F473C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated Stateful Protocol Verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_Stateful_Protocol_Verification"}}}}}