Newer
Older
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
#!/usr/bin/python3.8
import re
import os
import sys
debug = True
lines = sys.stdin.readlines()
lemma = sys.argv[1]
# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL
vk=dict()
rank = [] # list of list of goals, main list is ordered by priority
maxPrio = 110
for i in range(0,maxPrio):
rank.append([])
if lemma!="AnyLemma":
print("applying lemma")
for line in lines:
num = line.split(':')[0]
if re.match('.*!Pk\(.*', line): rank[106].append(num)
elif re.match('.*!Ltk\(.*', line): rank[106].append(num)
elif re.match('.*!PkCPS\(.*', line): rank[106].append(num)
elif re.match('.*!LtkCPS\(.*', line): rank[106].append(num)
elif re.match('.*TPM_EK_QPD.*', line): rank[108].append(num)
elif re.match('.*CertRes\( req.*', line): rank[105].append(num)
elif re.match('.*CertRes.*', line): rank[107].append(num)
elif re.match('.*CertReq.*', line): rank[107].append(num) #?
elif re.match('.*!KU\( ~cps.*', line): rank[108].append(num)
elif re.match('.*!KU\( ~res.*', line): rank[51].append(num)
elif re.match('.*!KU\( ~.*', line): rank[100].append(num)
elif re.match('.*!KU\( KDF.*', line): rank[100].append(num)
elif re.match('.*!KU\( curlyK.*', line): rank[100].append(num)
elif re.match('.*!KD\(.*', line): rank[99].append(num)
elif re.match('.*~~>.*', line):
if re.match('.*\(#i.*', line): rank[94].append(num)
elif re.match('.*\(#vk\..*', line):
i=re.search('.*\(#vk\.(\d+),.*', line).group(1)
vk[int(i)]=num
rank[95]=[vk[key] for key in sorted(vk.keys())]
elif re.match('.*\(#vk.*', line): rank[96].append(num)
else: rank[93].append(num) # 86?
elif re.match('.*!KU\( sign\(.*\'join_Issuer', line): rank[82].append(num)
elif re.match('.*!KU\( \$\w+ .*', line): rank[81].append(num)
elif re.match('.*!KU\( \'.*', line): rank[81].append(num)
elif re.match('.*TPM_Public.*', line): rank[70].append(num) #?
elif re.match('.*!KU\( H_SHA256\(.*\'Host_JoinComplete\'.*', line): rank[60].append(num)
elif re.match('.*!KU\( KDF_a\(', line): rank[51].append(num)
elif re.match('.*!KU\( KDF_e\(', line): rank[51].append(num)
elif re.match('.*!KU\( pk\(', line): rank[50].append(num)
elif re.match('.*!KU\( MAC\(', line): rank[50].append(num)
elif re.match('.*!KU\( senc\(', line): rank[50].append(num)
elif re.match('.*!KU\( curlyK\(', line): rank[50].append(num)
elif re.match('.*!KU\( H_SHA256\(.*', line): rank[50].append(num)
elif re.match('.*!KU\( multp\(.*', line): rank[50].append(num)
elif re.match('.*!KU\( sign\(', line): rank[49].append(num)
elif re.match('.*!KU\( aenc\(~s', line): rank[49].append(num)
elif re.match('.*!KU\( aenc\(', line): rank[45].append(num)
elif re.match('.*!KU\( x.*', line): rank[5].append(num)
elif re.match('.*!KU\( n.*', line): rank[4].append(num)
elif re.match('.*', line): rank[10].append(num)
else:
exit(0)
# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
for goal in listGoals:
sys.stderr.write(goal)
print(goal)