securedrop-protocol-models/oracle.py at main · freedomofpress/securedrop-protocol-models · GitHub

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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
#!/usr/bin/env python3

from sys import argv, stdin, exit
import re

def splitter(line):
  splitted = line.split(':')
  return (splitted[0], splitted[1].strip())

lines = list(map(splitter, stdin.readlines()))
if not lines:
  exit(0)

def subToken(token, line):
  (num, goal) = line
  if isinstance(token, str):
    return num if token in goal else None
  else:
    return num if token.search(goal) is not None else None

def matchAgainstList(priorityList, lines):
  for token in priorityList:
    try:
      return next(filter(bool, map(lambda line: subToken(token, line), lines)))
    except StopIteration:
      pass

re_keys = re.compile(r'^!?[\w_]+_Key\(')
re_signed_keys = re.compile(r'!KU\( sign\(<\'[\w-]+\'')
re_illegal_submission = re.compile(r'!Submission\(.+\'g\'(,|>)')

match = None
if argv[1] == 'Auto_SecureChannelSources':
  match = matchAgainstList([
    '~~>',
    re.compile(r'^\(∃'),
    re.compile(r'Client_Out\( ~sess(\.\d*), \$Server(\.\d*), ~id(\.\d*)'),
    re.compile(r'^\(last'),
    re.compile(r'^(Client|Server)Source'),
    '!Submission',
    'KU( senc',
  ], lines)
elif argv[1] == 'Auto_FetchingSharedSecretSecrecySourceSubmission':
  match = matchAgainstList([
    re_illegal_submission,
    re.compile(r'∃.+Reveal'),
    '!KU( ~r',
    '!KU( ~j',
    '!KU( ~x',
    '!KU( ~ltk',
    re.compile(r'!Submission\(.+\) ▶. #t1'),
    '!KU( sign(<\'j-sig-ltk\', j_fetch_pk, j_apke_pk>, ~',
    '!KU( sign(<\'nr-sig\',',
    '!KU( \'g\'^(~j_fetching_sk*~r*~x) ) @ #t4',
    'splitEqs(4)',
  ], lines)
elif argv[1] == 'Auto_FetchingSharedSecretSecrecyJournalistSubmission':
  match = matchAgainstList([
    re_illegal_submission,
    re.compile(r'∃.+Reveal'),
    '!KU( \'g\'^(~r*~x*kdf(<\'fetch\', ~passphrase>)) ) @ #t5',
    'splitEqs(4)',
  ], lines)
elif argv[1] == 'Auto_FetchingChallengeSecrecy':
  match = matchAgainstList([
    re_illegal_submission,
    '∃',
    'senc(~chall,',
    re.compile(r'Client_Out\(.+~chall'),
    re.compile(r'!Submission.+ ▶. #t1'),
    '!KU( ~chall',
    '!KU( kdf(<$NR, \'g\'^(~r*',
  ], lines)
elif argv[1] == 'Secrecy_SourceSubmission':
  match = matchAgainstList([
    re_illegal_submission,
    'Reveal_Newsroom_Key',
    'Reveal_Journalist_SIG_Key',
    '!LongTerm',
    '!Public',
    '!KU( sign(<\'nr-sig\'',
    '!KU( sign(<\'j-sig-eph\'',
    '!KU( sign(<\'j-sig-ltk\'',
    '!Submission',
    '!KU( ~msg',
    '∀',
    re.compile(r'Client_Out\(.+~chall'),
    '∃',
  ], lines)
elif argv[1] == 'Secrecy_JournalistSubmission':
  match = matchAgainstList([
    '!Journalist_Enrolled',
    '!LongTerm_Journalist_APKE_Key',
    re_illegal_submission,
    '!KU( ~msg )',
    'Fetched( ~id ) @ #x',
    re.compile(r'Client_Out\(.+~chall \)'),
    re.compile(r'!Submission\( \$Server'),
    '!LongTerm_Source',
    re.compile(r'^\(*∃'),
    re.compile(r'^\(*∀'),
  ], lines)
elif argv[1] == 'Agreement_Source' or argv[1] == 'Agreement_Journalist':
  match = matchAgainstList([
    re_illegal_submission,
    re.compile(r'∃.+Reveal'),
    re_keys,
    'APKE_Enc',
    re_signed_keys,
    re.compile(r'(Source|Journalist)Responded'),
  ], lines)
elif argv[1] == 'Easy_SessionSecrecy':
  match = matchAgainstList([
    re.compile(r'(Source|Journalist)(Queried|Responded)'),
    '!KU( ~sess )',
  ], lines)
elif argv[1] == 'Easy_EphemeralDHSecrecy':
  match = matchAgainstList([
    'ClassicSecret',
    '!KU( ~',
  ], lines)
elif argv[1] == 'Easy_SubmissionEquality':
  match = matchAgainstList([
    'Submi',
  ], lines)

if match is not None:
  print(match)