File size: 4,309 Bytes
1b66555 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 | """Small, total proof checker for passive perfect-encryption deduction.
Input data, never code, are interpreted. This proves only the stated finite
atomic-key deduction problem; it does not verify a deployed crypto protocol.
"""
import json
import re
SCHEMA = ('Return JSON with exactly "secret_unreachable" (boolean), "steps" '
'(list of zero-based public fact indices), and "known" (list of atom names). '
'Start with initial_known. For each step, the indexed [message,key] fact must '
'have an already-known key and add a new message. The final known list must '
'contain exactly the deduced atoms, without duplicates, and be closed: every '
'public fact whose key is known must have its message known. Set '
'secret_unreachable to whether query_secret is absent. Any valid deduction '
'order and known-list order are accepted. No external code or tools.')
def reference(instance):
known = set(instance['initial_known'])
steps = []
changed = True
while changed:
changed = False
for i, (message, key) in enumerate(instance['encrypted_facts']):
if key in known and message not in known:
known.add(message); steps.append(i); changed = True
return dict(secret_unreachable=instance['query_secret'] not in known,
steps=steps, known=sorted(known))
def check(instance, certificate):
"""Return a bounded diagnostic, without consulting a reference target."""
if not isinstance(certificate, dict) or set(certificate) != {'secret_unreachable','steps','known'}:
return 'schema'
if type(certificate['secret_unreachable']) is not bool:
return 'schema'
steps, final = certificate['steps'], certificate['known']
if not isinstance(steps,list) or not isinstance(final,list) or len(steps)>128 or len(final)>128:
return 'schema'
if any(type(i) is not int for i in steps) or any(not isinstance(a,str) for a in final):
return 'schema'
known = set(instance['initial_known']); facts = instance['encrypted_facts']
for i in steps:
if not 0 <= i < len(facts):
return 'fact_index'
message,key = facts[i]
if key not in known:
return 'unavailable_key'
if message in known:
return 'redundant_step'
known.add(message)
if len(set(final)) != len(final) or set(final) != known:
return 'known_mismatch'
if any(key in known and message not in known for message,key in facts):
return 'not_closed'
if certificate['secret_unreachable'] != (instance['query_secret'] not in known):
return 'query_mismatch'
return 'valid'
def parse_final(text):
# One whole final JSON fence is a formatting variant, never extract from prose.
if not isinstance(text,str) or len(text)>50000:
return None
fence = re.fullmatch(r'\s*```(?:json)?\s*\n(.*?)\n```\s*',text,flags=re.S)
try:
def reject_duplicates(pairs):
value = {}
for k,v in pairs:
if k in value:
raise ValueError('duplicate JSON key')
value[k]=v
return value
return json.loads(fence.group(1) if fence else text,
object_pairs_hook=reject_duplicates)
except (ValueError,TypeError,RecursionError):
return None
def prompt(row):
return json.dumps({k:row[k] for k in ['initial_known','encrypted_facts','query_secret']},
separators=(',',':'))
def trace(row, certificate):
known = set(row['initial_known'])
lines = ['Finite symbolic deduction, treating enc as perfect encryption.',
'Initial atoms: '+', '.join(sorted(known))+'.']
for i in certificate['steps']:
message,key=row['encrypted_facts'][i]
lines.append(f'Fact {i}: key {key} is available, so decrypt to obtain {message}.')
known.add(message)
blocked = [str(i) for i,(_,k) in enumerate(row['encrypted_facts']) if k not in known]
lines.append('At the fixed point all other facts are blocked by unknown keys: '+', '.join(blocked)+'.')
lines.append('The query atom is '+('absent.' if certificate['secret_unreachable'] else 'present.'))
return '\n'.join(lines)
|