theory KEA_plus_AdvKey
begin

builtins: hashing, diffie-hellman

section{* KEA+ with adversarial key registration *}
/*
 * Protocol:	KEA+
 * Modeler: 	Cas Cremers
 * Date: 	January 2012, June 2013
 * Source:	"Security Analysis of KEA Authenticated Key Exchange Protocol"
 * 		Lauter, Mityagin, 2006
 *
 * 		Adapted the security model in the context of the ASICS
 * 		work, in order to be able to model the attack previously
 * 		found manually by Michele Feltz on KEA+. 
 *
 * Status: 	Working
 */


/* Protocol rules */

rule generate_ltk:
   let pk = 'g'^~lk
   in
   [ Fr(~lk) ] -->
   [ !Ltk( $A, ~lk ), !Pk( $A, pk ), Out( pk ) ]

rule generate_ltk_adv:
   [ In(< $A, pk> ) ]
   --[ AdvKey(pk), LtkRev(pk) ]->
   [ !Pk( $A, pk ) ]

rule Init_1:
   let epkI = 'g'^~ekI
   in
   [ Fr( ~ekI ), !Ltk( $I, ~lkI ) ]
   --[ SidI_1(~ekI,$I,$R, epkI ) ]->
   [ Init_1( ~ekI, $I, $R, ~lkI, epkI ),
     !Ephk(~ekI),
     Out( epkI ) ]

rule Init_2:
   let epkR = 'g'^~ekR
       pkI  = 'g'^~lkI
       sesk = h( <Y^~lkI, (pkR)^~ekI, $I, $R > )
   in
   [ Init_1( ~ekI, $I, $R, ~lkI , hkI), In( Y ), !Pk( $R,pkR ) ]
   --[SidI_2( ~ekI, $I, $R, hkI, Y, sesk, pkI, pkR ) ]->
   [ !Sessk( ~ekI, sesk ) ]

rule Resp_1:
   let pkR  = 'g'^~lkR
       sesk = h( <(pkI)^~ekR, X^~lkR, $I, $R > )
   in
   [ In( X ), Fr( ~ekR ), !Ltk($R, ~lkR), !Pk($I, pkI) ]
   --[ SidR_1( ~ekR, $I, $R, X, 'g'^~ekR, sesk, pkI, pkR ) ]->
   [ Out( 'g'^~ekR ), !Ephk(~ekR), !Sessk( ~ekR, sesk) ]

rule Sessk_reveal: 
   [ !Sessk(~tid, k) ]
   --[ SesskRev(~tid) ]->
   [ Out(k) ]

rule Ephk_reveal:
   [ !Ephk(~ekI) ]
   --[ EphkRev(~ekI) ]->
   [ Out(~ekI) ]

rule Ltk_reveal:
   [ !Ltk($A, k) ]
   --[ LtkRev('g'^k) ]->
   [ Out(k) ]


/* 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)"
*/

/* Security notion.
 *
 * This is the "core" KEA+ security definition without (w)PFS or KCI.
 *
 * We model ephemeral key reveals for non-partner threads.  This
 * corresponds to a session-state-reveal analysis where the
 * session-state is defined as the randomness generated by the parties.
 * This property is not implied by the proof (sketch) in the KEA+ paper.
 */

/* An attack is valid in the security notion if the session key of the test session is deduced and
   the test session is clean.
*/
lemma keaplus_initiator_key:
  "not (Ex #i1 #i2 ttest I R k hkI hkR kI kR.
            SidI_2(ttest, I, R, hkI, hkR, k, kI, kR ) @ i1 & K( k ) @ i2

            /* No ephemeral-key-reveal of test thread */
            & (All #i3. EphkRev( ttest ) @ i3 ==> F)

            /* Not session-key-reveal of test thread. */
            & (All #i3. SesskRev( ttest ) @ i3 ==> F)

            /* Not ephemeral-key-reveal of partner thread. */
            & (All #i3 #i4 tpartner kpartner kI2 kR2 .
                   SidR_1( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3
		   & EphkRev( tpartner ) @ i4 ==> F)

            /* Not session-key-reveal of partner thread. */
            & (All #i3 #i4 tpartner kpartner kI2 kR2 .
                   SidR_1( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3
		   & SesskRev( tpartner ) @ i4 ==> F)

            /* Not longterm-key-reveal of actor or intended peer. */
            & (All #i3. LtkRev( kI ) @ i3 ==> F)
            & (All #i3. LtkRev( kR ) @ i3 ==> F)
    )"

/* An attack is valid in the security notion if the session key of the test session is deduced and
   the test session is clean.
*/
lemma keaplus_responder_key:
  "not (Ex #i1 #i2 ttest I R k hkI hkR kI kR.
            SidR_1(ttest, I, R, hkI, hkR, k, kI, kR) @ i1 & K( k ) @ i2

            /* Not ephemeral-key-reveal of test thread. */
            & (All #i3. EphkRev( ttest ) @ i3 ==> F)

            /* Not session-key-reveal of test thread. */
            & (All #i3. SesskRev( ttest ) @ i3 ==> F)

            /* Not ephemeral-key-reveal of partner thread. */
	    /* Note we distinguish explicitly between an incomplete
	     * and complete partner thread case.
	     */
            & (All #i3 #i4 tpartner lki.
                   SidI_1( tpartner,I,R,lki ) @i3
		   & EphkRev( tpartner ) @ i4 ==> F) 
            & (All #i3 #i4 tpartner kpartner kI2 kR2 .
                   SidI_2( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3
		   & EphkRev( tpartner ) @ i4 ==> F)

            /* Not session-key-reveal of partner thread. Note that we use SidI_2 here.
	       A session key reveal can only happen after SidI_2 is logged anyways.
	    */
            & (All #i3 #i4 tpartner kpartner kI2 kR2 .
                   SidI_2( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3
		   & SesskRev( tpartner ) @ i4 ==> F)

            /* Not longterm-key-reveal of actor or intended peer. */
            & (All #i3. LtkRev( kR ) @ i3 ==> F)
            & (All #i3. LtkRev( kI ) @ i3 ==> F)
    )"

end