scyther/gui/Protocols/IKE/scanner.py

#!/usr/bin/env python

import sys

ALLPROTS = set()
ALLCLAIMS = set()   # prot x role x claim
PREFIX = None       # Required prefix
FFUNC = (lambda p: True)        # Filter function

def reset():

    global ALLPROTS
    global ALLCLAIMS
    global PREFIX
    global FFUNC

    ALLPROTS = set()
    ALLCLAIMS = set()
    PREFIX = None
    FFUNC = (lambda p: True) 

def skipLine(l):
    if len(l) == 0:
        return True

    skippable = ["%","\\begin","\\end","Protocol"]
    for skstr in skippable:
        if l.startswith(skstr):
            return True

    return False

def stripRowEnd(l):
    # Assume ends with \\, split by dtl
    endstr = "\\\\"
    if not l.endswith(endstr):
        print("Error: some line does not end with \\\\")
        print(">>%s<<" % (l))
        sys.exit(-1)

    return l[:-len(endstr)]

def splitStrip(l,sp):

    dtl = l.split(sp)
    for i in range(0,len(dtl)):
        dtl[i] = dtl[i].strip()
    return dtl

def roleClaim(dtl):
    rcdt = dtl.split()
    assert(rcdt[0].endswith(":"))
    role = rcdt[0][:-1]
    claim = rcdt[1]
    return (role,claim[:20])

def scanAttackFile(fn):

    global ALLPROTS

    fp = open("gen-%s-mpaattacks.tex" % (fn),"r")
    attackmap = {}
    prot = None
    role = None
    claim = None
    for rawline in fp:

        l = rawline.strip()

        if skipLine(l):
            continue

        l = stripRowEnd(l)

        dtl = splitStrip(l,"&")

        # New protocol
        if len(dtl[0]) > 0:
            prot = dtl[0]

        # New role
        if len(dtl[1]) > 0:
            (role,claim) = roleClaim(dtl[1])

        # Claims list
        # Assume starts with '[' and ends with ']'
        assert(dtl[2].startswith("["))
        assert(dtl[2].endswith("]"))
        attl = ((dtl[2])[1:-1]).split(",")
        for i in range(0,len(attl)):
            x = attl[i].strip()
            assert(x.startswith("'"))
            assert(x.endswith("'"))
            attl[i] = x[1:-1]

        ak = (prot,role,claim)
        if ak not in list(attackmap.keys()):
            attackmap[ak] = set()
        attackmap[ak].add(tuple(attl))

        # Add to allprots set
        ALLPROTS.add(prot)
        for p in attl:
            ALLPROTS.add(prot)

    fp.close()

    return attackmap


def shorten(prot):
    """
    Shorten protocol name
    """
    cutting = ["isoiec-","9798-"]
    for ct in cutting:
        if prot.startswith(ct):
            prot = prot[len(ct):]
    return prot.replace("-udkey","-ud")


def prettyclaim(cl):
    """
    Rewrite if needed
    """
    return cl.replace("Commit","Agreement")


def mpaTable(attackmap):
    """
    construct table for MPA attacks
    """
    counter = 1
    s = ""

    s += "\\begin{longtable}{|l|lll|l|}\n" 
    s += "\\hline\n"
    for kk in sorted(ALLCLAIMS):
        if kk not in list(attackmap.keys()):
            continue
        (prot,role,claim) = kk

        ats = str(attackmap[kk])
        sl = "%i & %s & %s & %s & %s \\\\ \n" % (counter,prot,role,claim,ats)

        s += sl
        counter = counter + 1

    s += "\\hline\n"
    s += "\\end{longtable}\n"

    return s


def rotated(headl):
    """
    Add rotated headers
    """
    for i in range(0,len(headl)):
        headl[i] = "\\begin{sideways} %s \\end{sideways}\n" % (headl[i])
    return " & ".join(headl)


def baseprot(prot):
    return shorten(prot)[:5]


def mpaTable2(attackmap,tabtype="tabular",options=""):
    """
    construct table for MPA attacks

    Second attempt
    """

    # To find the number of columns, we first need to find all protocols involved in two-protocol attacks
    involved = set()
    for kk in list(attackmap.keys()):
        for atl in attackmap[kk]:
            # convert tuple back to list
            att = list(atl)
            if len(att) == 1:
                # This attack involves one *additional* protocol, so is a two-protocol attack
                involved.add(att[0])
    colheads = sorted(involved)
    attcols = ""
    last = None
    for hd in colheads:
        prm = baseprot(hd)
        if last == prm:
            attcols += "@{\hspace{2mm}}c"
        else:
            last = prm
            attcols += "|c"


    #attcols = "c" * len(involved)

    counter = 1
    s = ""

    #s += "\\clearpage \n"

    s += "\\begin{%s}%s{|l|ll|%s|}\n" % (tabtype,options,attcols)
    s += "\\hline\n"
    s += rotated(["No","Prot","Claim"])
    for hd in colheads:
        s += "& \\begin{sideways}%s\\end{sideways} " % (shorten(hd))
    s += "\\\\ \n"

    s += "\\hline\n"
    last = None
    for kk in sorted(ALLCLAIMS):
        if kk not in list(attackmap.keys()):
            continue
        (prot,role,claim) = kk
        
        prm = baseprot(prot)
        if last != prm:
            last = prm
            s += "\\hline\n"

        sl = ""
        sl += "%i & %s & %s %s " % (counter,shorten(prot),role,claim)
        for ch in colheads:
            se = tuple([ch])
            if se in attackmap[kk]:
                sl += "& $\\bullet$ "
            else:
                sl += "& $\\circ$  "

        sl += "\\\\ \n"

        s += sl
        counter = counter + 1

    s += "\\hline\n"
    s += "\\end{%s}\n" % (tabtype)

    return s


def mpaTable3(attackmaps,tabtype="tabular",options=""):
    """
    construct table for MPA attacks

    attmaps = sequence of (attackmap, symbol)

    Symbol of the first matching is displayed

    Second attempt
    """

    global FFUNC
    # To find the number of columns, we first need to find all protocols involved in two-protocol attacks
    # Also populate "allkeys"
    involved = set()
    allkeys = set()
    for (attackmap,symbs) in attackmaps:
        for kk in list(attackmap.keys()):
            allkeys.add(kk)
            for atl in attackmap[kk]:
                # convert tuple back to list
                att = list(atl)
                if len(att) == 1:
                    # This attack involves one *additional* protocol, so is a two-protocol attack
                    if FFUNC:
                        if not FFUNC(att[0]):
                            continue

                    involved.add(att[0])

    colheads = sorted(involved)
    attcols = ""
    last = None
    for hd in colheads:
        prm = baseprot(hd)
        if last == prm:
            attcols += "@{\hspace{2mm}}c"
        else:
            last = prm
            attcols += "|c"


    #attcols = "c" * len(involved)

    counter = 1
    s = ""

    #s += "\\clearpage \n"

    s += "\\begin{%s}%s{|l|ll|%s|}\n" % (tabtype,options,attcols)
    s += "\\hline\n"
    s += rotated(["No","Prot","Claim"])
    for hd in colheads:
        s += "& \\begin{sideways}%s\\end{sideways} " % (shorten(hd))
    s += "\\\\ \n"

    s += "\\hline\n"
    last = None
    for kk in sorted(ALLCLAIMS):
        if kk not in list(attackmap.keys()):
            continue
        (prot,role,claim) = kk
        
        prm = baseprot(prot)
        if last != prm:
            last = prm
            s += "\\hline\n"

        sl = ""
        sl += "%i & %s & %s %s " % (counter,shorten(prot),role,prettyclaim(claim))
        for ch in colheads:
            se = tuple([ch])
            sl += "& "
            for (attackmap,symb) in attackmaps:
                if kk in list(attackmap.keys()):
                    if se in attackmap[kk]:
                        sl += symb
                        break

        sl += "\\\\ \n"

        s += sl
        counter = counter + 1

    s += "\\hline\n"
    s += "\\end{%s}\n" % (tabtype)

    return s


def scanClaimList(fn):
    """
    Simply gather claims
    """

    global ALLPROTS
    global ALLCLAIMS
    global FFUNC

    fp = open("gen-%s-claims.txt" % (fn),"r")

    claimmap = {}
    for rawline in fp:

        l = rawline.strip()

        if skipLine(l):
            continue

        dtl = splitStrip(l,"; ")

        filename = dtl[0]
        prot = dtl[1]
        if FFUNC:
            if not FFUNC(prot):
                continue

        label = dtl[2]
        (role,claim) = roleClaim(dtl[3])

        ALLCLAIMS.add((prot,role,claim))
        ALLPROTS.add(prot)

    fp.close()

    return claimmap

def scanClaimFile(fn):
    """
    Construct claimmap

    prot -> roles -> claims
    """

    global ALLPROTS
    global ALLCLAIMS
    global FFUNC

    fp = open("gen-%s-correctclaims.tex" % (fn),"r")

    claimmap = {}
    for rawline in fp:

        l = rawline.strip()

        if skipLine(l):
            continue

        l = stripRowEnd(l)

        dtl = splitStrip(l,"&")

        prot = dtl[0]
        if FFUNC:
            if not FFUNC(prot):
                continue

        if prot not in list(claimmap.keys()):
            claimmap[prot] = {}

        cll = splitStrip(dtl[1],";")

        for dt in cll:
            (role,claim) = roleClaim(dt)

            if role not in list(claimmap[prot].keys()):
                claimmap[prot][role] = set()

            claimmap[prot][role].add(claim)

            ALLCLAIMS.add((prot,role,claim))

        ALLPROTS.add(prot)

    fp.close()

    return claimmap

def getRoleClaims(rcmap):

    rc = set()
    for role in list(rcmap.keys()):
        for claim in rcmap[role]:
            rc.add((role,claim))

    return rc

def typeScanMatrix(cml,onlyChanged = False):

    global ALLPROTS

    """
    Scan for the influence of typing.

    Input:

    [(txt1,cm1),(txt2,cm2),...]

    """
    s = ""

    s += "\\begin{longtable}{|l|lll|%s|}\n" % ("c" * len(cml))
    s += "\\hline\n"

    s += "No & Prot & Role & Claim "
    for (txt,cm) in cml:
        s += "& %s " % (txt)
    s += "\\\\\n"
    s += "\\hline\n"

    goodverdict = "$\\circ$"
    badverdict = "$\\bullet$"

    counter = 1
    for (prot,role,claim) in sorted(ALLCLAIMS):
        # Header
        sl = "%i & %s & %s & %s " % (counter,prot,role,claim)
        alltrue = True
        for (txt,cm) in cml:
            verdict = badverdict
            if prot in list(cm.keys()):
                if role in list(cm[prot].keys()):
                    if claim in cm[prot][role]:
                        verdict = goodverdict
            if verdict == badverdict:
                alltrue = False

            sl += "& %s " % (verdict)
        sl += "\\\\\n"

        if alltrue == True:
            if onlyChanged == True:
                continue

        s += sl
        counter = counter + 1

    s += "\\hline\n"
    s += "\\end{longtable}\n"
    return s

def typeScanMatrix2(cml,onlyChanged = False,additive = False):

    global ALLPROTS

    """
    Scan for the influence of typing.

    Input:

    [(txt1,cm1),(txt2,cm2),...]

    """
    s = ""

    s += "\\begin{longtable}{|l|lll||c|}\n" 
    s += "\\hline\n"

    s += "No & Prot & Claim & Attacks"
    s += "\\\\\n"
    s += "\\hline\n"
    s += "\\hline\n"

    goodverdict = "$\\circ$"
    badverdict = "$\\bullet$"

    last = None
    counter = 1
    for (prot,role,claim) in sorted(ALLCLAIMS):
        if baseprot(prot) != last:
            last = baseprot(prot)
            s += "\\hline\n"

        # Header
        sl = "%i & %s & %s %s " % (counter,prot,role,prettyclaim(claim))
        alltrue = True
        res = ""
        for (txt,cm) in cml:
            verdict = badverdict
            if prot in list(cm.keys()):
                if role in list(cm[prot].keys()):
                    if claim in cm[prot][role]:
                        verdict = goodverdict
            if verdict == badverdict:
                alltrue = False
                if additive:
                    res += txt
                else:
                    res = txt

        sl += "& %s " % (res)
        sl += "\\\\\n"

        if alltrue == True:
            if onlyChanged == True:
                continue

        s += sl
        counter = counter + 1

    s += "\\hline\n"
    s += "\\end{longtable}\n"
    return s

def typeScanMatrix3(hd1,hd2,cml,f,onlyChanged = False,tabletype="longtable"):

    global ALLPROTS

    """
    Scan for the influence of typing.

    Input:

    f is given as input a sequence of Bool (attack = False) of length len(cml), should return string.

    """
    s = ""

    s += "\\begin{%s}{|l|ll||%s|}\n" % (tabletype,hd1)
    s += "\\hline\n"

    s += rotated(["No","Protocol","Claim"]) + " & " + rotated(hd2)
    s += "\\\\\n"
    s += "\\hline\n"
    s += "\\hline\n"

    goodverdict = "$\\circ$"
    badverdict = "$\\bullet$"

    last = None
    counter = 1
    for (prot,role,claim) in sorted(ALLCLAIMS):
        if baseprot(prot) != last:
            last = baseprot(prot)
            s += "\\hline\n"

        # Header
        sl = "%i & %s & %s %s " % (counter,prot,role,prettyclaim(claim))
        alltrue = True
        res = ""
        resl = []
        for cm in cml:
            verdict = badverdict
            if prot in list(cm.keys()):
                if role in list(cm[prot].keys()):
                    if claim in cm[prot][role]:
                        verdict = goodverdict
            if verdict == badverdict:
                alltrue = False
                resl.append(False)
            else:
                resl.append(True)

        sl += "& %s " % (f(resl))
        sl += "\\\\\n"

        if alltrue == True:
            if onlyChanged == True:
                continue

        s += sl
        counter = counter + 1

    s += "\\hline\n"
    s += "\\end{%s}\n" % (tabletype)
    return s

def docWrapper(s,title=None,author=None):

    pref = ""
    pref += "\\documentclass{article}\n"
    pref += "\\usepackage{a4}\n"
    pref += "\\usepackage{geometry}\n"
    pref += "\\usepackage{longtable}\n"
    pref += "\\usepackage{rotating}\n"
    pref += "\\begin{document}\n"
    if title or author:
        if title:
            pref += "\\title{%s}\n" % (title)
        if author:
            pref += "\\author{%s}\n" % (author)
        pref += "\\maketitle\n"
    post = ""
    post += "\\end{document}\n"

    return pref + s + post

def secWrapper(s,title,level=0):
    """
    level : 

    0 section
    1 subsection
    2 subsub...
    """
    pref = "\\" + "sub" * level + "section{" + title + "}\n\n"
    post = "\n"
    return pref + s + post


def sizeWrapper(s, width="!", height="!"):

    if (width != "!") or (height != "!"):
        s = "\\resizebox{%s}{%s}{ \n%s}\n" % (width,height,s)
    return s


def fileWrite(fn,s):

    fp = open("%s.tex" % (fn), "w")
    fp.write(s)
    fp.close()


def docWrite(fn,tex,author=None,title=None):

    fileWrite(fn, docWrapper(tex,author=author,title=title))


def docMake(fn,tex,author=None,title=None):

    import subprocess

    docWrite(fn,tex,author,title)
    cmd = "pdflatex %s" % (fn)
    subprocess.getoutput(cmd)

def f1(resl):
    txtl = []
    for t in resl:
        if t == True:
            txtl.append(" ")
        else:
            txtl.append("$\\bullet$")
    return " & ".join(txtl)

def pb(tl,width):
    nl = []
    for t in tl:
        nl.append("\\parbox{%s}{%s}" % (width,t))
    return nl

def makeReport(fn,includefiles=False):
    scanClaimList(fn + "-aa-t")

    cISOaat = scanClaimFile(fn + "-aa-t")
    cISOaab = scanClaimFile(fn + "-aa-b")
    cISOaau = scanClaimFile(fn + "-aa-u")
    cISOiut = scanClaimFile(fn + "-iu-t")
    cISOiub = scanClaimFile(fn + "-iu-b")
    cISOiuu = scanClaimFile(fn + "-iu-u")
    cISOext = scanClaimFile(fn + "-ex-t")
    cISOexb = scanClaimFile(fn + "-ex-b")
    cISOexu = scanClaimFile(fn + "-ex-u")

    tex = ""
    #tex += secWrapper(typeScanMatrix([("typed",cISOaat),("basic",cISOaab),("untyped",cISOaau)],onlyChanged = False),title="Normal mode (Alice-Alice communication allowed)")
    #tex += secWrapper(typeScanMatrix([("typed",cISOiut),("basic",cISOiub),("untyped",cISOiuu)],onlyChanged = True),title="Disallow Alice-Alice initiators")
    #tex += secWrapper(typeScanMatrix([("typed",cISOext),("basic",cISOexb),("untyped",cISOexu)],onlyChanged = True),title="Disallow Alice-Alice communications")

    orders = [cISOaab,
              cISOaat,
              cISOiub,
              cISOiut]

    sectex = typeScanMatrix3("c|c|c|c",pb(["No type checks\\\\Alice-talks-to-Alice initators","Type checks\\\\Alice-talks-to-Alice initators","No type checks\\\\No Alice-talks-to-Alice initators","Type checks\\\\No Alice-talks-to-Alice initators"],"49mm"), orders,f1,onlyChanged = True)

    mpatex = sizeWrapper(mpaTable3([
        (scanAttackFile(fn + "-ex-t"),"$\\bullet$"),
        (scanAttackFile(fn + "-aa-b"),"$\\circ$")
        ]),width="\\textwidth")

    if includefiles == True:
        fileWrite("../gen-att-" + fn,sectex)
        fileWrite("../gen-mpa-" + fn,mpatex)

    tex += secWrapper(sectex,title="Attacks found")
    tex += secWrapper(mpatex,title="MPA attacks")
    docMake(fn,tex,author="Cas Cremers",title="test report %s" % (fn))


def filterPrefix(prot):
    """
    Returns true iff the protocol name is okay to be considered
    """
    if PREFIX:
        if not prot.startswith(PREFIX):
            return False
    return True

def filterPrefixBD(prot):
    """
    Returns true iff the protocol name is okay to be considered
    """
    if PREFIX:
        if not prot.startswith(PREFIX):
            return False
    if prot.endswith("-ud"):
        return False
    if prot.endswith("-udkey"):
        return False
    return True


def filterCombo(prot):
    """
    Returns true iff the protocol name is okay to be considered
    """
    if prot.find("-sig-child") >= 0:
        return False
    
    return True


def filterISOsymmBD(prot):
    """
    Returns true iff the protocol name is okay to be considered
    """
    if prot.endswith("-ud"):
        return False
    if prot.endswith("-udkey"):
        return False

    if prot.startswith("isoiec-9798-2"):
        return True
    if prot.startswith("isoiec-9798-4"):
        return True

    return False



if __name__ == "__main__":
    
    #reset()
    #PREFIX = "isoiec-9798-2"
    #makeReport(PREFIX)

    includefiles = True

    reset()
    FFUNC = filterCombo
    PREFIX = "ike1"
    makeReport(PREFIX,includefiles=includefiles)

    reset()
    FFUNC = filterCombo
    PREFIX = "ike2"
    makeReport(PREFIX,includefiles=includefiles)

    reset()
    FFUNC = filterCombo
    PREFIX = "ike0"
    makeReport(PREFIX,includefiles=includefiles)