theory STS_MAC_fix1
begin

builtins: diffie-hellman, signing

functions: mac/2
functions: KDF/1

section{* The Station-To-Station Protocol (MAC version, fix UKS attack with proof-of-possession of exponent) *}

/*
 * Protocol:	Station-To-Station, MAC variant: fix with CA Proof-of-Possession check
 * Modeler: 	Cas Cremers
 * Date: 	January 2012
 * Source:	"Unknown Key-Share Attacks on the Station-to-Station (STS) Protocol"
 *		Blake-Wilson, Simon and Menezes, Alfred
 * 		PKC '99, Springer, 1999
 *
 * Status: 	working
 */

// Public keymat infrastructure
/**
 * The !Pk facts can be regarded as certificates
 */
rule Register_pk_normal:
  [ Fr(~ltk) ] 
  --> 
  [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)), Out(pk(~ltk)) ]

// Can register a key, but only if we know the exponent
// Models proof-of-possession check.
rule Register_pk_evil:
  [ In(ltk) ] 
  --[ Corrupt($E) ]-> 
  [ !Ltk($E, ltk), !Pk($E, pk(ltk)), Out(pk(ltk)) ]

// Protocol
rule Init_1:
  let epkI = 'g'^~ekI
  in
  [ Fr(~ekI), !Ltk($I, ~ltkI) ]
  -->
  [ Init_1( $I, $R, ~ltkI, ~ekI )
  , Out( <$I, $R, epkI> ) ]

rule Init_2:
  let epkI = 'g'^~ekI
      sigI = sign{ epkI, Y }~ltkI
      sigR = sign{ Y, epkI }~ltkR
      keymat = Y^~ekI
      key = KDF(keymat)
  in
    [ Init_1( $I, $R, ~ltkI, ~ekI )
    , !Pk($R, pk(~ltkR))
    , In( <$R, $I, Y, sigR, mac( keymat, sigR)
      > ) ]
  --[ AcceptedI(~ekI,$I,$R,epkI,Y, key) ]->
    [ Out( <$I, $R, sigI, mac( keymat, sigI) > ),
      !SessionKey(~ekI,$I,$R, key)
    ]

rule Resp_1:
  let epkR = 'g'^~ekR
      sigI = sign{ X, epkR }~ltkI
      sigR = sign{ epkR, X }~ltkR
      keymat = X^~ekR
      key = KDF(keymat)
  in
    [ !Ltk($R, ~ltkR)
    , Fr(~ekR)
    , In( <$I, $R, X > ) ]
  -->
    [ Resp_1( $I, $R, ~ltkR, ~ekR, X )
    , Out(< $R, $I, epkR, sigR, mac( keymat, sigR ) >) 
    ]


rule Resp_2:
  let epkR = 'g'^~ekR
      sigI = sign{ X, epkR }~ltkI
      sigR = sign{ epkR, X }~ltkR
      keymat = X^~ekR
      key = KDF(keymat)
  in
    [ !Pk($I, pk(~ltkI))
    , Resp_1( $I, $R, ~ltkR, ~ekR, X )
    , In( <$I, $R, sigI, mac( keymat, sigI ) >)
    ]
  --[ AcceptedR(~ekR,$I,$R,X,epkR, key ) ]->
    [ !SessionKey(~ekR,$I,$R, key) ]



rule Sessionkey_Reveal:
    [ !SessionKey(~tid, $I,$R,k) ]
  --[ SesskRev(~tid) ]->
    [ Out(k) ]



lemma KI_Perfect_Forward_Secrecy_I:
  "not (Ex ttest I R sessKey #i1 #k hki hkr.
     AcceptedI(ttest,I,R,hki,hkr,sessKey) @ i1 &
     not (Ex #r. Corrupt(I) @ r) &
     not (Ex #r. Corrupt(R) @ r) &
     K(sessKey) @ k &
     // No session keymat reveal of test
     not (Ex #i3. SesskRev(ttest) @ i3) &
     // No session keymat reveal of partner
     not (Ex #i3 #i4 tpartner kpartner. SesskRev(tpartner) @ i3
          & AcceptedR(tpartner,I,R,hki,hkr,kpartner) @ i4
         ) 
     )
  "

lemma KI_Perfect_Forward_Secrecy_R:
  "not (Ex ttest I R sessKey #i1 #k hki hkr.
     AcceptedR(ttest,I,R,hki,hkr,sessKey) @ i1 &
     not (Ex #r. Corrupt(I) @ r) &
     not (Ex #r. Corrupt(R) @ r) &
     K(sessKey) @ k &
     // No session keymat reveal of test
     not (Ex #i2. SesskRev(ttest) @ i2) &
     // No session keymat reveal of partner
     not (Ex #i2 #i3 tpartner kpartner. SesskRev(tpartner) @ i2
          & AcceptedI(tpartner,I,R,hki,hkr,kpartner) @ i3
         ) 
     )
  "

end