3way-katz-yung.spthy

theory 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: B, g^x, Sig_A(A | g^x | B | g^y)
// C->A: C, g^z, Sig_C(C | g^z)
// A->B: C, g^z, Sig_A(<A, B> | g^g^xy | C | g^z)
// A->C: A, B, g^g^xy, Sig_A(<A, B> | g^g^xy | C | 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>
    msgOut = <A, gx, B, gy>
    sigOut = sign(msgOut, ltkA)
    k = gy^~x
  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, k) ]->
  [
    JoinedTwoUserA(A, B, k),
    Out(<gx, A, sigOut>)
  ]

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

// Second user joins
rule AddSecondUser:
  let
    gk = 'g'^k
    msgIn = <C, gz>
    msgOut = <A, B, gk, C, gz>
    sigOut = sign(msgOut, ltkA)
    k1 = h(<gz^k, A, B, C>)
  in
  [
    In(<C, gz, sigIn>),
    InitKey(C, gz, sigIn),
    JoinedTwoUserA(A, B, k),
    !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, gk, A, B, C, sigOut>)
  ]

rule ReceiveSecondAddExisting:
  let
    gk = 'g'^k
    msg = <A, B, gk, C, gz>
    k1 = h(<gz^k, A, B, C>)
  in
  [
    In(<gz, A, B, C, sig>),
    JoinedTwoUserB(A, B, k),
    !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
    msg = <A, B, gk, C, gz>
    k1 = h(<gk^z, A, B, C>)
  in
  [
    In(<gz, gk, A, B, C, sig>),
    InitKeyPriv(C, z, ltkC),
    !Pk(A, pkA)
  ]
  --[ Neq(A, C),
      Neq(B, C),
      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