hashed-3way-katz-yung.spthy

theory Hashed_3way_Katz_Yung
begin

builtins: diffie-hellman, signing, hashing

// PKI Provisioning
rule RegisterPK:
  [ Fr(~ltk) ]
  -->
  [
    !Ltk($A, ~ltk),
    !Pk($A, pk(~ltk)),
    Out(pk(~ltk))
  ]

rule RevealLTK:
  [ !Ltk(A, ltk) ]
  --[ LtkReveal(A) ]->
  [ Out(ltk) ]


// B->A: B, g^y, Sig_A(B | g^x)
// A->B: A, g^x, Sig_A(h(A | B), h(g^x | g^y))
// C->A: C, g^z, Sig_C(C | g^z)
// A->B: C, g^z, Sig_A(h(h(A | B) | C) | h(h(g^x | g^y) | g^g^xy | g^z))
// A->C: h(A | B), h(g^x | g^y), g^g^xy, Sig_A(h(h(A | B) | C) | h(h(g^x | g^y) | g^g^xy | g^z))

rule PostInitKey:
  let
    gx = 'g'^~x
    msg = <A, gx>
    sig = sign(msg, ltkA)
  in
  [
    !Ltk(A, ltkA),
    Fr(~x)
  ]
  --[ PostedInitKey(A, gx) ]->
  [
    InitKeyPriv(A, ~x, ltkA),
    InitKey(A, gx, sig),
    Out(<A, gx, sig>)
  ]

// First user joins
rule AddFirstUser:
  let
    gx = 'g'^~x
    msgIn = <B, gy>
    roster0 = h(<A, B>)
    transcript0 = h(<gx, gy>)
    msgOut = <roster0, transcript0>
    sigOut = sign(msgOut, ltkA)
    k0 = h(<gy^~x, roster0>)
  in
  [
    In(<B, gy, sigIn>),
    InitKey(B, gy, sigIn),
    !Ltk(A, ltkA),
    !Pk(B, pkB),
    Fr(~x)
  ]
  --[ Neq(A, B),
      Eq(verify(sigIn, msgIn, pkB), true),
      TwoUserA(A, B, k0) ]->
  [
    JoinedTwoUserA(A, B, roster0, transcript0, k0),
    Out(<gx, A, sigOut>)
  ]

rule ReceiveFirstAdd:
  let
    gy = 'g'^y
    roster0 = h(<A, B>)
    transcript0 = h(<gx, gy>)
    msg = <roster0, transcript0>
    k0 = h(<gx^y, roster0>)
  in
  [
    In(<gx, A, sig>),
    InitKeyPriv(B, y, ltkB),
    !Pk(A, pkA)
  ]
  --[ Neq(A, B),
      Eq(verify(sig, msg, pkA), true),
      TwoUserB(A, B, k0) ]->
  [
    JoinedTwoUserB(A, B, roster0, transcript0, k0)
  ]

// Second user joins
rule AddSecondUser:
  let
    gk0 = 'g'^k0
    msgIn = <C, gz>
    roster1 = h(<roster0, C>)
    transcript1 = h(<transcript0, gk0, gz>)
    msgOut = <roster1, transcript1>
    sigOut = sign(msgOut, ltkA)
    k1 = h(<gz^k0, roster1>)
  in
  [
    In(<C, gz, sigIn>),
    InitKey(C, gz, sigIn),
    JoinedTwoUserA(A, B, roster0, transcript0, k0),
    !Ltk(A, ltkA),
    !Pk(C, pkC)
  ]
  --[ Neq(A, C),
      Neq(B, C),
      Eq(verify(sigIn, msgIn, pkC), true),
      ThreeUserA(A, B, C, k1) ]->
  [
    JoinedThreeUserA(A, B, C, k1),
    Out(<gz, gk0, roster1, transcript1, C, sigOut>)
  ]

rule ReceiveSecondAddExisting:
  let
    gk0 = 'g'^k0
    roster1 = h(<roster0, C>)
    transcript1 = h(<transcript0, gk0, gz>)
    msg = <roster1, transcript1>
    k1 = h(<gz^k0, roster1>)
  in
  [
    In(<gz, C, sig>),
    JoinedTwoUserB(A, B, roster0, transcript0, k0),
    !Pk(A, pkA)
  ]
  --[ Neq(B, C),
      Eq(verify(sig, msg, pkA), true),
      ThreeUserB(A, B, C, k1) ]->
  [
    JoinedThreeUserB(A, B, C, k1)
  ]

rule ReceiveSecondAddNew:
  let
    gz = 'g'^z
    roster1 = h(<roster0, C>)
    transcript1 = h(<transcript0, gk0, gz>)
    msg = <roster1, transcript1>
    k1 = h(<gk0^z, roster1>)
  in
  [
    In(<gk0, B, roster0, transcript0, sig>),
    InitKeyPriv(C, z, ltkC),
    !Pk(A, pkA)
  ]
  --[ Neq(A, C),
      Neq(B, C),
      Eq(h(<A, B>), roster0),
      Eq(verify(sig, msg, pkA), true),
      ThreeUserC(A, B, C, k1) ]->
  [
    JoinedThreeUserC(A, B, C, k1)
  ]


// Restrictions
restriction Equality:
  "All x y #i. Eq(x,y) @i ==> x = y"

restriction Inequality:
  "All x y #i. Neq(x,y) @i ==> not(x = y)"

// Functionality test
lemma TwoPartyExecutable:
  exists-trace
  "
    Ex A B key #i #j.
        TwoUserA(A, B, key) @ #i
      & TwoUserB(A, B, key) @ #j
      & not(Ex X #k. LtkReveal(X) @ #k)
  "

lemma ThreePartyExecutable:
  exists-trace
  "
    Ex A B C key #i #j #k.
        ThreeUserA(A, B, C, key) @ #i
      & ThreeUserB(A, B, C, key) @ #j
      & ThreeUserC(A, B, C, key) @ #k
      & not(Ex X #r. LtkReveal(X) @ #r)
  "


// If three clients have established a key,
// ... it is not known to the attacker
// ... unless one of the long-term keys was compromised
lemma KeySecrecy:
  "
  not(Ex A B C key #i #j #k #l.
        ThreeUserA(A, B, C, key) @ #i
      & ThreeUserB(A, B, C, key) @ #j
      & ThreeUserC(A, B, C, key) @ #k
      & K(key) @ #l
      & not(Ex #ra. LtkReveal(A) @ #ra)
      & not(Ex #rb. LtkReveal(B) @ #rb)
      & not(Ex #rc. LtkReveal(C) @ #rc)
  )
  "

// If an existing user and a new joiner both think that someone
// added them, it's because someone did.  Unless that person's key
// has been compromised.
lemma AdderLiveness:
  "
  All A B C key #i #j.
    ( ThreeUserB(A, B, C, key) @ #i
    & ThreeUserC(A, B, C, key) @ #j
    )
    ==> ( (Ex #k. ThreeUserA(A, B, C, key) @ #k)
        | (Ex #l. LtkReveal(A) @ #l)
        )
  "

// If an existing user and a new joiner both see an add and arrive
// at the same key, then they agree on the roster.
//
// Note that there's no exception here for compromise of the adding
// member's key, so this holds even if the adding user is malicious.
//
// Note that this implies injective agreement.
lemma RosterConsistency:
  "
  All A B1 B2 C1 C2 key #i #j.
    ( ThreeUserB(A, B1, C1, key) @ #i
    & ThreeUserC(A, B2, C2, key) @ #j
    )
    ==> ( (B1 = B2)
        & (C1 = C2)
        )
  "

// ... injective agreement
lemma InjectiveAgreement:
  "
  All A1 A2 B1 B2 C1 C2 key #i1 #j1 #i2 #j2.
    ( ThreeUserB(A1, B1, C1, key) @ #i1
    & ThreeUserC(A1, B1, C1, key) @ #j1
    & ThreeUserB(A2, B2, C2, key) @ #i2
    & ThreeUserC(A2, B2, C2, key) @ #j2
    )
    ==> ( ( (A1 = A1)
          & (B1 = B2)
          & (C1 = C2)
          )
        | (Ex #r1. LtkReveal(A1) @ #r1)
        | (Ex #r2. LtkReveal(A2) @ #r2)
        )
  "

end