theory STS_MAC_FIX1
begin

builtin: diffie-hellman, hashing, signing

functions: mac/2

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 key 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:
  [ Fr(~ekI), !Ltk($I, ~ltkI) ]
  -->
  [ Init_1( $I, $R, ~ltkI, ~ekI )
  , Out( <$I, $R, 'g' ^ ~ekI> ) ]

rule Init_2:
    [ Init_1( $I, $R, ~ltkI, ~ekI )
    , !Pk($R, pk(~ltkR))
    , In( <$R, $I, Y, 
          sign{ Y, 'g'^~ekI }~ltkR,
        mac(Y^~ekI,
            sign{ Y, 'g'^~ekI }~ltkR
	)
      > ) ]
  --[ AcceptedI(~ekI,$I,$R,'g'^~ekI,Y, h(Y ^ ~ekI)) ]->
    [ Out( <$I, $R, 
          sign{ 'g' ^ ~ekI, Y }~ltkI,
	mac( Y^~ekI,
             sign{ 'g' ^ ~ekI, Y }~ltkI
	)
      > ),
      !SessionKey(~ekI,$I,$R, h(Y ^ ~ekI))
    ]

rule Resp_1:
    [ !Ltk($R, ~ltkR)
    , Fr(~ekR)
    , In( <$I, $R, X > ) ]
  -->
    [ Resp_1( $I, $R, ~ltkR, ~ekR, X )
    , Out( <$R, $I, 'g' ^ ~ekR,
          sign{ 'g' ^ ~ekR, X }~ltkR,
	  mac( X^~ekR,
             sign{ 'g' ^ ~ekR, X }~ltkR
          )
      > ) ]

rule Resp_2:
    [ !Pk($I, pk(~ltkI))
    , Resp_1( $I, $R, ~ltkR, ~ekR, X )
    , In( <$I, $R, 
          sign{ X, 'g'^~ekR }~ltkI,
  	  mac(X^~ekR,
              sign{ X, 'g'^~ekR }~ltkI
	  )
      > ) ]
  --[ AcceptedR(~ekR,$I,$R,X,'g'^~ekR, h(X ^ ~ekR)) ]->
    [ !SessionKey(~ekR,$I,$R, h(X ^ ~ekR) ) ]

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 key reveal of test
     not (Ex #i3. SesskRev(ttest) @ i3) &
     // No session key 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 key reveal of test
     not (Ex #i2. SesskRev(ttest) @ i2) &
     // No session key reveal of partner
     not (Ex #i2 #i3 tpartner kpartner. SesskRev(tpartner) @ i2
          & AcceptedI(tpartner,I,R,hki,hkr,kpartner) @ i3
         ) 
     )
  "

end