hashed-incremental-katz-yung.spthy

theory Hashed_Incremental_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) ]


// C->S: C, g^x, Sig_C(C | g^x)
// S->C: S, g^y, Sig_S(h(C | S), h(g^x | g^y))

// Client logic
rule ClientInit:
  let
    gx = 'g'^~x
    msg = <C, gx>
    sig = sign(msg, ltkC)
  in
  [
    !Ltk(C, ltkC),
    Fr(~x)
  ]
  --[ ClientSentInitKey(C, gx) ]->
  [
    ClientWait(C, $S, ~x, ltkC),
    Out(<C, gx, sig>)
  ]

rule ClientFinish:
  let
    gx = 'g'^x
    msg = <h(<C, S>), h(<gx, gy>)>
    k = gy^x
  in
  [
    In(<gy, S, sig>),
    ClientWait(C, S, x, ltkC),
    !Pk(S, pkS)
  ]
  --[ Eq(verify(sig, msg, pkS), true),
      ClientDone(C, S, gx, gy, k) ]->
  []

// Server logic
rule ServerInit:
  let
    gy = 'g'^~y
    msgIn = <C, gx>
    msgOut = <h(<C, S>), h(<gx, gy>)>
    sigOut = sign(msgOut, ltkS)
    k = gx^~y
  in
  [
    In(<C, gx, sigIn>),
    !Ltk(S, ltkS),
    !Pk(C, pkC),
    Fr(~y)
  ]
  --[ Neq(C, S),
      Neq(gy, gx),
      Eq(verify(sigIn, msgIn, pkC), true),
      ServerDone(S, C, gx, gy, k) ]->
  [
    Out(<gy, S, sigOut>)
  ]

// 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 HonestTrace:
  exists-trace
  "
    Ex C S gx gy k #i #j.
        ClientDone(C, S, gx, gy, k) @ #i
      & ServerDone(S, C, gx, gy, k) @ #j
      & not(Ex A #k. LtkReveal(A) @ #k)
  "

// If a client has established a session key,
// ... then the server has the same key,
// ... and it is not known to the attacker
// ... unless one of the long-term keys was compromised
lemma KeySecrecy:
  "
  not(Ex C S gx gy k #i #j #k.
        ClientDone(C, S, gx, gy, k) @ #i
      & ServerDone(S, C, gx, gy, k) @ #j
      & K(k) @ #k
      & not(Ex #rc. LtkReveal(C) @ #rc)
      & not(Ex #rs. LtkReveal(S) @ #rs)
  )
  "

// If a client has established a session key
// ... then it's based on a response from a server
lemma ServerLiveness:
  "
  All C S gx gy k #i.
    ClientDone(C, S, gx, gy, k) @ #i
    ==> ( (Ex #j. (ServerDone(S, C, gx, gy, k) @ #j) & (#j < #i))
        | (Ex #rc. LtkReveal(C) @ #rc)
        | (Ex #rs. LtkReveal(S) @ #rs)
        )
  "

// If a server has established a session key
// ... then it's based on a request from a client
lemma ClientLiveness:
  "
  All C S gx gy k #i.
    ServerDone(S, C, gx, gy, k) @ #i
    ==> ( (Ex #j. (ClientSentInitKey(C, gx) @ #j) & (#j < #i))
        | (Ex #rc. LtkReveal(C) @ #rc)
        | (Ex #rs. LtkReveal(S) @ #rs)
        )
  "

// ... injective agreement
lemma InjectiveAgreement:
  "
  All C S gx gy k #i.
    ServerDone(S, C, gx, gy, k) @ #i
    ==> ( not(Ex C2 S2 gx2 gy2 #i2.
              ServerDone(S2, C2, gx2, gy2, k) @ #i2
             & not(#i2 = #i)
             )
        | (Ex #rc. LtkReveal(C) @ #rc)
        | (Ex #rs. LtkReveal(S) @ #rs)
        )
  "

end