ObsEquOracle_credential_installation.py

#!/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()
maxPrio = 110
rank = [ [] for i in range(maxPrio)]          # list of list of goals, main list is ordered by priority

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\( <req.*', line): rank[105].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\( true.*', line): rank[20].append(num)
    elif re.match('.*!KU\( PkY\(.*', line): rank[12].append(num)
    elif re.match('.*!KU\( PkX\(.*', line): rank[11].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)
    exit(0)

# exit(0)