| """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): |
| |
| 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) |
|
|
|
|
