theory KAS2_eCK
begin

builtins: hashing, asymmetric-encryption

section{* KAS2 *}

/*
 * Protocol:	KAS2
 * Modeler: 	Cas Cremers
 * Date: 	April 2012
 * Source:	"A Generic Variant of NISTS's KAS2 Key Agreement Protocol"
 * 		Chatterjee, Menezes, Ustaoglu, 2011
 * Model:	eCK
 *
 * Status: 	working
 */

functions: KDF/1
functions: MAC/2

/* Protocol rules */

/* Generate long-term keypair */
rule Register_pk:
  let pkA = pk(~ltkA)
  in
  [ Fr(~ltkA) ] 
  --> 
  [ !Ltk($A, ~ltkA), !Pk($A, pkA), Out(pkA) ]

/* Initiator */
rule Init_1:
  let c1 = aenc{ ~m1 }pkR
  in
   [ Fr( ~m1 ), !Ltk( $I, ~lkI ), !Pk($R,pkR) ]
   --[ Sid( ~m1, $I, $R, <$I, $R, 'Init', c1>) ]->
   [ Init_1( ~m1, $I, $R, ~lkI, ~m1, c1), !Ephk( ~m1,~m1 ), Out( c1 ) ]

rule Resp_1:
  let m1 = adec(c1, ~lkR)
      c2 = aenc{ ~m2 }pkI
      key = KDF(< m1, ~m2, $I, $R, c1, c2 >)
      tagR = MAC(key, (< 'Resp', $R, $I, c2, c1 >) )
  in
   [ Fr( ~m2 ), In( c1 ), !Ltk( $R, ~lkR ), !Pk($I,pkI) ]
   --[  Sid  ( ~m2, $R, $I, <$R, $I, 'Resp', c2, c1>)
     ,  Match( ~m2, <$I, $R, 'Init', c1>)
     ,  Match( ~m2, <$I, $R, 'Init', c1, c2>)
     ]->
   [ Resp_1( ~m2, $I, $R, ~lkR, m1, ~m2, c1, c2 ), !Ephk( ~m2,~m2 ), Out(< c2 , tagR >) ]

rule Init_2:
  let m2 = adec(c2, ~lkI)
      key = KDF(< ~m1, m2, $I, $R, c1, c2 >)
      tagR = MAC( key, (< 'Resp', $R, $I, c2, c1 >) )
      tagI = MAC( key, (< 'Init', $I, $R, c1, c2 >) )
  in
   [ Init_1( ~m1, $I, $R, ~lkI, ~m1, c1 ) , In(< c2, tagR >) ]
   --[ Sid  ( ~m1, $I, $R, <$I, $R, 'Init', c1, c2> )
     , Match( ~m1, <$R, $I, 'Resp', c2, c1> )
     , Accept( ~m1, $I, $R, key) 
     ]->
   [ Out( tagI ), !Sessk( ~m1, key ) ]

rule Resp_2:
  let 
      key = KDF(< m1, ~m2, $I, $R, c1, c2 >)
      tagI = MAC( key, (< 'Init', $I, $R, c1, c2 >) )
  in
   [ Resp_1( ~m2, $I, $R, ~lkR, m1, ~m2, c1, c2), In( tagI ) ]
   --[ Accept( ~m2, $R, $I, key) ]->
   [ !Sessk( ~m2, key ) ]



/* Key Reveals for the eCK model */
rule Sessk_reveal: 
   [ !Sessk(~tid, k) ]
   --[ SesskRev(~tid) ]->
   [ Out(k) ]

rule Ltk_reveal:
   [ !Ltk($A, lkA) ]
   --[ LtkRev($A) ]->
   [ Out(lkA) ]

rule Ephk_reveal:
   [ !Ephk(~s, ~ek) ]
   --[ EphkRev(~s) ]->
   [ Out(~ek) ]


/* Security properties */

/*
lemma key_agreement_reachable:
  "not (Ex #i1 #i2 ekI ekR I R k hkI hkR.
          SidI_2(ekI, I, R, hkI, hkR, k) @ i1 & SidR_1(ekR, I, R, hkI, hkR, k) @ i2)"
*/
lemma eCK_key_secrecy:
  "not (Ex #i1 #i2 s A B k .
	    Accept(s, A, B, k) @ i1 & K( k ) @ i2 

            /* No session-key-reveal of test thread. */
            & not(Ex #i4. SesskRev( s ) @ i4 )

	    /* If matching session exists (for all matching sessions...) */
	    & (All ss #i4 #i5 C D ms.
	           ( Sid ( ss, C, D, ms ) @ i4 & Match( s, ms ) @ i5)
		     ==>
		   ( not(Ex #i6    . SesskRev( ss ) @ i6 )
		   & not(Ex #i6 #i7. LtkRev  ( A ) @ i6  & EphkRev ( s  ) @ i7 )
		   & not(Ex #i6 #i7. LtkRev  ( B ) @ i6  & EphkRev ( ss ) @ i7 )
		   )
	      )

	    /* No matching session exists */
	    & ( ( not(Ex ss #i4 #i5 C D ms.
	           Sid ( ss, C, D, ms ) @ i4 & Match( s, ms ) @ i5 ) )
		     ==>
		   ( not(Ex #i6    . LtkRev (B) @ i6 )
		   & not(Ex #i6 #i7. LtkRev (A) @ i6 & EphkRev ( s ) @ i7 )
		   )
	      )
  )"

end