break-golf

एक बोर्ड क्रिप्टैनालिसिस परिणामों के लिए जो सिद्ध हैं, चलाए नहीं गए।

एक चैलेंज दो दुनियाएँ और उस कथन को स्थिर करता है जिसे आपको सिद्ध करना है। आप एक adversary और एक प्रमाण लिखते हैं कि वह उन्हें अलग करता है। जीत प्रमाण है: कुछ भी निष्पादित, नमूना या पुनः चलाया नहीं जाता, और कोई मनुष्य यह तय करने के लिए सबमिशन नहीं पढ़ता कि वह मान्य है या नहीं।

स्थिति: proof-of-concept। साइट स्थिर है, सबमिशन एक GitHub issue खोलते हैं, और एक मनुष्य निर्णय करता है। इसके पीछे अभी कोई Lean verifier नहीं है।

Layout

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rewrite the ledger with scores and frontier
python3 tools/lint_challenges.py   # configs are complete
python3 tools/check_site.py        # the site can render what the tools generate

printf '%s' "$BODY" | python3 tools/verify.py spoc128    # one submission

CI

verify.yml push और pull request पर चलता है: --check गेट्स, config lint, साइट जाँच, और सबमिशनों की एक बैटरी जिन्हें verifier को स्वीकार और अस्वीकार करना ही चाहिए — एक sorry, एक native_decide, एक अज्ञात challenge, शून्य advantage, और एक body जिसमें कोई Lean block नहीं है। workflow_dispatch बिना issue खोले माँग पर एक सबमिशन सत्यापित करता है।

submission.yml एक verify: issue को दो jobs में संभालता है। पहली अविश्वसनीय इनपुट को parse करती है और कोई write scope नहीं रखती; दूसरी उसका verdict डाउनलोड करती है और टिप्पणी पोस्ट करती है। यह विभाजन lean-golf का है और यही कारण है कि issue body किसी token तक नहीं पहुँच सकती।

The submitter never writes the statement

यह पूरी प्रणाली है, और यह वही है जो trailofbits/lean-golf proof golf के लिए उपयोग करता है। Verifier Challenge.lean की अपनी प्रति बनाता है। एक सबमिशन केवल ये देता है:

def strategy : game.Param → PFunDDS.DDE game.Query game.Response
def verdict  : List (game.Query × Option game.Response) → Bool
theorem attackWins : attack.Wins score.budget score.advantage

फ़ॉर्म पर budget और advantage के अतिरिक्त। attack और score उन संख्याओं से Challenge.lean में जोड़े जाते हैं, इसलिए एक सबमिशन उससे बड़ा budget खर्च नहीं कर सकता जितने के लिए उसे scored किया जाता है, या जितना वह दावा करता है उससे कमज़ोर bound सिद्ध नहीं कर सकता — इसलिए नहीं कि हम जाँचते हैं, बल्कि इसलिए कि उसके पास कभी इन दोनों वस्तुओं पर कलम नहीं होती।

चार अस्वीकृतियाँ जो verifier बिना कुछ पढ़े करता है:

native_decide, maxHeartbeats और maxRecDepth भी अस्वीकार किए जाते हैं: एक प्रमाण जो केवल बढ़ाई गई सीमा के साथ बंद होता है, वह प्रमाण है जिसे verifier वहन नहीं कर सकता।

Scoring

पहले से कुछ निश्चित नहीं है। एक योजना पर जिसका किसी ने अध्ययन नहीं किया है, किस लागत पर कौन सा advantage प्राप्त करने योग्य है, यही शोध प्रश्न है, इसलिए कोई भी लक्ष्य एक अनुमान है — और बहुत ऊँचा रखा गया लक्ष्य एक वास्तविक 2⁻³⁰ distinguisher को शून्य score करता है। इसके बजाय board परिणाम को मापता है:

score = log₂( budget / advantage^e )

प्रति इकाई advantage पर queries; इसका log आधार दो वह सुरक्षा स्तर बिट्स में है जिसे आक्रमण खंडित करता है। कम बेहतर है। अपने advantage को कम बताना score को बढ़ाता है, इसलिए जितना आप सिद्ध कर सकते हैं उससे कम दावा करने में कोई लाभ नहीं है।

e प्रति challenge है और इसका कोई डिफ़ॉल्ट नहीं है। एक decision game के लिए e = 2 — एक advantage α को प्रवर्धित (amplify) होने के लिए लगभग α⁻² पुनरावृत्तियों की आवश्यकता होती है — और search-प्रकृति वाले के लिए e = 1। दोनों प्रथाएँ साहित्य में हैं और यह असंगति ज्ञात है (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), इसलिए एक challenge बताता है कि वह किसका उपयोग करता है।

Par डिज़ाइनर का अपना दावा है, विशिष्टता से लिया गया, इसलिए आक्रमण कठिनाई के बारे में कोई अनुमान कहीं नहीं दिखता। Par से नीचे दावे का भंजन है।

frontier प्राथमिक रिकॉर्ड है: एक परिणाम इसमें तब शामिल होता है जब कोई अन्य चीज़ उसे queries और advantage दोनों पर एक साथ नहीं हराती। bit score उसके बगल में ranked स्तंभ है, और Lean परत में दो जाँचे गए lemmas (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) गारंटी देते हैं कि ranking कभी उस परिणाम को नहीं दबाता जो दोनों अक्षों पर जीतता है।

Challenges

spoc128 — SpoC-128 जैसा NIST LWC Round 2 में प्रस्तुत किया गया। टूटा हुआ: तीन queries, advantage 1, 1.58 bits। load key n nonce को rate में रखता है और tagInput tagControl को उसी rate में XOR करता है, इसलिए tagInput (load key n) = load key (n ^^^ tagControl)। एक permutation इनपुट दो queries से प्राप्त करने योग्य है, और चूँकि permutation सार्वजनिक और व्युत्क्रमणीय है, इसका आधा एक tag में और आधा एक ciphertext block में लीक होता है; जोड़ें, व्युत्क्रम करें, capacity लें, और वही key है।

spoc128-ds — वही mode जिसमें चार control bits nonce में आरक्षित हैं, इसलिए n ^^^ tagControl एक वैध nonce नहीं है। खुला: कोई आक्रमण ज्ञात नहीं है। यह प्रतिबंध एक query के type में रहता है, इसलिए प्रकाशित आक्रमण यहाँ केवल असफल नहीं है — इसे एक adversary के रूप में प्रस्तुत ही नहीं किया जा सकता (SpoC128DS.attack_second_query_illegal)।

यह जानबूझकर mode की दूसरी प्रति नहीं है। DDC.lean को कठोर बनाने का अर्थ एक समानांतर मॉडल होता जिसे संगत रखना पड़ता; query क्षेत्र को प्रतिबंधित करना एक predicate है, और mode के बारे में हर मौजूदा प्रमेय अब भी लागू होता है।

यहाँ कुछ भी यह दावा नहीं करता कि यह प्रकार सुरक्षित है। किसी mode में एक प्रकाशित मार्ग को बंद करना यह तर्क नहीं है कि कोई दूसरा मार्ग मौजूद नहीं है — यही इसे प्रस्तुत करने का उद्देश्य है।

एक चैलेंज जोड़ना

Lean परत में एक Golf.Game प्रदान करें — एक सार्वजनिक parameter type, एक query और response type, और दो दुनियाएँ — फिर यहाँ एक config.json। सामान्य परत RandomSystems/Golf/Game.lean में रहती है; RandomSystems/Golf/Instances/SpoC128/ काम का उदाहरण है, और यह जाँच भी है कि abstraction विश्वसनीय है: इसकी adequacy receipts rfl हैं और इसका संदर्भ सबमिशन मौजूदा attack_distinguishing_advantage द्वारा बिना किसी पुनःकथन के निपटाया जाता है।

यह क्या score नहीं करता

• Offline कार्य, निर्णय द्वारा। adversary एक प्रतीकात्मक वस्तु है और board query complexity को score करता है, वह सूचना-सैद्धांतिक परिवेश जिसमें indifferentiability और PRP/PRF switching lemma पहले से रहते हैं। एक challenge जिसे computational व्यवहार्यता चाहिए, उसे यह कहना चाहिए और लागत-वहन करने वाला रूप पिन करना चाहिए।
• Amplification उपलब्ध माना जाता है: q/α^e किसी आक्रमण को confidence तक दोहराने की लागत है।
• बराबरी समतुल्यता नहीं है। समान bit स्तर बहुत भिन्न परिणाम धारण कर सकता है, यही कारण है कि frontier ranking के बगल में बैठता है न कि उसके द्वारा प्रतिस्थापित होता है।