{"entities":{"Q7361695":{"pageid":31520624,"ns":120,"title":"Item:Q7361695","lastrevid":105423782,"modified":"2026-10-08T13:45:46Z","type":"item","id":"Q7361695","labels":{"en":{"language":"en","value":"Game-based cryptography in HOL"}},"descriptions":{"en":{"language":"en","value":"AFP entry Game_Based_Crypto"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6b3c43e312f23f110faa4696c779dc31c2715494","datavalue":{"value":"https://isa-afp.org/entries/Game_Based_Crypto.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361695$CA4F56D6-ADF3-4A72-A8FC-586EA10D5982","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"480a99c095fd0e6e30ce40dd951da46a627a2bb9","datavalue":{"value":"Andreas Lochbihler","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361695$B1EA8DB6-3B5A-4121-A898-61A30F268B42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"bd7c6c31d61f45a261be518c8f677cec7b19e4de","datavalue":{"value":"S. Reza Sefidgar","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361695$1170FC81-1A29-4C65-87A9-6972BCB86B51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"be09d456c3ac361d9a176ac1683505eecebc79f4","datavalue":{"value":"Bhargav Bhatt","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361695$775E1492-F840-4845-9F1F-78E4BB96E5C3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4fc7a21964269d79698239d3f98239cacf9c1ca9","datavalue":{"value":"In this AFP entry, we show how to specify game-based cryptographic security notions and formally prove secure several cryptographic constructions from the literature using the CryptHOL framework. Among others, we formalise the notions of a random oracle, a pseudo-random function, an unpredictable function, and of encryption schemes that are indistinguishable under chosen plaintext and/or ciphertext attacks. We prove the random-permutation/random-function switching lemma, security of the Elgamal and hashed Elgamal public-key encryption scheme and correctness and security of several constructions with pseudo-random functions. Our proofs follow the game-hopping style advocated by Shoup and Bellare and Rogaway, from which most of the examples have been taken. We generalise some of their results such that they can be reused in other proofs. Thanks to CryptHOL's integration with Isabelle's parametricity infrastructure, many simple hops are easily justified using the theory of representation independence.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361695$DECDCBF0-0DAB-4BFB-81C6-3217EBB719AC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$4ED96974-F55B-4A4C-8007-A8BAFCAA4C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bea8e9846e13a8715ab50748c9877999c599ec7","datavalue":{"value":{"entity-type":"item","numeric-id":3374913,"id":"Q3374913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$6A950DDC-F301-45E9-ADE6-B909A13CBB0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1e3b4249b8398eaf62ca99e3ad99ebe270af8ed","datavalue":{"value":{"entity-type":"item","numeric-id":3593109,"id":"Q3593109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$966D74FE-46EA-42CF-BAE6-B8FDD21960D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e40651885e589ae16736b2ed26430168a8207418","datavalue":{"value":{"entity-type":"item","numeric-id":3875826,"id":"Q3875826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$286D69AA-D575-453D-8764-BAB375182C70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc4c2f534223ec34c41fed80e42cbca489663773","datavalue":{"value":{"entity-type":"item","numeric-id":3689092,"id":"Q3689092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$26F946F9-D4A5-464A-8886-7EFAFAEEC789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b548fb76f8ef8a56f9223030f407f1a96f0c7ba1","datavalue":{"value":{"entity-type":"item","numeric-id":1057832,"id":"Q1057832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$1CB30064-D6D9-4D75-AC23-67DB32BF1AC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$23622BDB-5CCF-4BEA-8D1F-E39FFC363249","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a334f4e96bc67eac9a5d7b987fa6f5d79a92b99","datavalue":{"value":{"entity-type":"item","numeric-id":2802495,"id":"Q2802495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$E3739B93-0183-43D1-807A-ED2E2EDE46A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f20bac6c3ed3ef71949319d1d7ba761b14c1bade","datavalue":{"value":{"entity-type":"item","numeric-id":3722164,"id":"Q3722164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$0B7FAE67-5CAB-4A3A-8599-E68C99288A1B","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":"Q7361695$D60FAA6A-B134-4991-95AE-9BEF86C237DB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2521123b5dbe8709daed0db214711d9c66f9f8cf","datavalue":{"value":{"time":"+2017-05-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361695$07999A69-C52E-4020-9CE7-F4C0E3F17B76","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"531d6e8195d6a39122192c85edfe43abf84dba0b","datavalue":{"value":{"text":"Game-based cryptography in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361695$79E8201B-F5F2-47C0-B0D0-03074F8C25FD","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":"Q7361695$D9D838A0-33E7-458C-AB30-2F66A896E42C","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"ade26dda0279fbc4dc5dce2aaa38eba4ae21c47f","datavalue":{"value":{"entity-type":"item","numeric-id":7361923,"id":"Q7361923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$64036B8E-2482-4722-B0AA-BE0C00CC55D6","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"67cfe7e765f8f36de5d26ce854526f3fec39cd26","datavalue":{"value":{"entity-type":"item","numeric-id":7360802,"id":"Q7360802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$47A64EFC-3E88-4609-94A0-F23232B5E41B","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":"Q7361695$9557BF0B-44AA-45E4-957D-D091DE281B55","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"08ea8a6196315e34bfef724788ea4d9f09069c62","datavalue":{"value":"38015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361695$75E8565F-F883-4EE2-86AD-064A95167E38","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361695$5BB4DA7C-E67E-4F89-8C3A-0501E7A596A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca6833d3c12e329e13f5f7a45eb21803ac988009","datavalue":{"value":"91.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361695$04A11B79-27C3-4773-838F-551142A8530F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fb7b2d196cb181e838b342f41804d522dff44830","datavalue":{"value":"94.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361695$D84C676E-371C-44C1-88F5-928EE75D9218","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"3a9edbd2c1b6a0c50c92b404a365a164e64c40f5","datavalue":{"value":{"entity-type":"item","numeric-id":53713,"id":"Q53713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$B2B6320A-B165-4DCB-BDDE-CAC286E4DCD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"63dfdf554f26dc046bc1cc284387a8f2b7ee925b","datavalue":{"value":{"entity-type":"item","numeric-id":39279,"id":"Q39279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$4B2E3D66-7566-4586-BFE9-0140DC591C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"826b53166301e7f2710fbb9ac0613992a63d1b43","datavalue":{"value":{"entity-type":"item","numeric-id":30463,"id":"Q30463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$2A5597C4-7067-4145-ADF2-456FFD599D37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"244ebbac6461f60bed6d50e50ce8194b0e233968","datavalue":{"value":{"entity-type":"item","numeric-id":40296,"id":"Q40296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$B3087490-DA66-49D5-80DB-5E0951DB73DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$1F76D828-545A-4F43-8E3E-BCCA55B12DEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$D0B89F3C-8030-4263-90FD-DE87651C4505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"da71442535724374fba994798fe2e776a105b283","datavalue":{"value":{"entity-type":"item","numeric-id":40255,"id":"Q40255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$FCF3415E-9B77-4754-AA38-EA2175B88338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$9947B8B4-AB02-49DE-9B1D-C5CDC334A2CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"475b592b7f3c7573e79f818da959e13eb74264b6","datavalue":{"value":{"entity-type":"item","numeric-id":32994,"id":"Q32994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$E2837BAD-6577-418D-9408-0952299B475B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9e7a1624ebcfc86cb11ccad80d0985ed6ed992b9","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$B53BA0BA-2A01-446D-AD74-E1566CAB7CC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$A743E943-0E54-46B5-B28D-B692437A9CD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4eea1e5549472c93f3282a38917960fdec6b61a1","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$F1CB0B6D-D89E-4AAC-A02B-5E94F9DB755D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"74b3e1a53a717ca62a629eb480944df7ee3187d4","datavalue":{"value":{"entity-type":"item","numeric-id":53714,"id":"Q53714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$32F14F30-6E72-4D9C-BA17-9473BC01907E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a3f9d192df50f24767772f5b218635cb7747b820","datavalue":{"value":{"entity-type":"item","numeric-id":21717,"id":"Q21717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$4E884FA8-E05F-4533-A3BC-B968CBC23C0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$C4C31CD8-71DB-4621-A355-C27E84678F28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361695$6B07F4D4-CBD8-41E1-8B3C-E6DAC35A35A4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Game-based cryptography in HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Game-based_cryptography_in_HOL"}}}}}