sig_verify_transcript.spthy

#ifdef ForwardSecrecy
rule Verify_Transcript_C:
let
    pkT = cert_pk(certT)
    sid = <certT, certC, r2, cip, pkCe, cipe>
    k = decaps(cip, skC)
    ke = decaps(cipe, skCe)
    kCNF_c = kdf(<'CNF', sid>, <k, ke>)
in
    [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(skCe), !Ltk(C, skC, 'chip') ]
  --[ Eq(C, cert_id(certC)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
    [  ]
#else
rule Verify_Transcript_C:
let
    pkT = cert_pk(certT)
    sid = <certT, certC, r2, cip>
    kKDF = decaps(cip, skC)
    kCNF_c = kdf(<'CNF', sid>, kKDF)
in
    [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), !Ltk(C, skC, 'chip') ]
  --[ Eq(C, cert_id(certC)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_c), ValidTrans(C, 'chip', cert_id(certT)) ]->
    [  ]
#endif

#ifdef PFS
rule Verify_Transcript_T:
let
    sid = <certT, certC, r2, cip, pkCe, cipe>
    kCNF_t = kdf(<'CNF', sid>, <k, ke>)
in
    [ In(<certT, IDc, r1, sT, certC, r2, pkCe, cip, sC, cipe, kCNF>), In(<k, ke>), !Pk(T, pkT, 'terminal') ]
  --[ Eq(T, cert_id(certT)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
    [  ]
#else
rule Verify_Transcript_T:
let
    sid = <certT, certC, r2, cip>
    kCNF_t = kdf(<'CNF', sid>, kKDF)
in
    [ In(<certT, IDc, r1, sT, certC, r2, cip, sC, kCNF>), In(kKDF), !Pk(T, pkT, 'terminal') ]
  --[ Eq(T, cert_id(certT)), Eq(verify_cert(certT, 'terminal'), true), Eq(verify_cert(certC, 'chip'), true), Eq(verify(sT, <'TA', IDc, r1>, pkT), true), Eq(verify(sC, <'CA', sid>, pkT), true), Eq(kCNF, kCNF_t), ValidTrans(T, 'terminal', cert_id(certC)) ]->
    [  ]
#endif