setup.spthy

/* Key setup and Certificate model for all EAC models */


functions: cert/3, cert_pk/1, cert_sig/1, cert_id/1, ca_sk/0 [private]
equations: cert_pk(cert(pk, s, id)) = pk, cert_sig(cert(pk, s, id)) = s, cert_id(cert(pk, s, id)) = id

macros: verify_cert(cert, role) = verify(cert_sig(cert), <cert_pk(cert), cert_id(cert), role>, pk(ca_sk))


rule Publish_ca_pk:
    [ ]
  -->
    [ Out(pk(ca_sk)) ]

// Generate long-term key pair for the chip. Classic version needs dh key pair
#ifdef CLASSIC
rule Generate_chip_key_pair:
let
    pk = 'g'^~ltk
in
    [ Fr(~ltk) ]
  --[ TestMe() ]->
    [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
#else
rule Generate_chip_key_pair:
let
    pk = pk(~ltk)
in
    [ Fr(~ltk) ]
  -->
    [ !Pk($A, pk, 'chip'), !Ltk($A, ~ltk, 'chip'), Out(pk) ]
#endif

// Generate static long-term key pair for the terminal.
rule Generate_terminal_key_pair:
let
    pk = pk(~ltk)
in
    [ Fr(~ltk) ]
  -->
    [ !Pk($A, pk, 'terminal'), !Ltk($A, ~ltk, 'terminal'), Out(pk) ]

rule CA_Sign_ltk:
let
    certA = cert(pk, sign(<pk, A, role>, ca_sk), A)
in
    [ !Pk(A, pk, role) ]
  --[ RegisteredRole(A, role) ]->
    [ !Cert(A, certA, role), Out(certA) ]