theory JKL_TS3_2004_KI_wPFS
begin

builtin: hashing, diffie-hellman

section{* Jeong, Katz, Lee : TS3 (2004) *}
/*
 * Protocol:	JKL-TS3-2004
 * Modeler: 	Cas Cremers
 * Date: 	January 2012
 * Source:	"One-Round Protocols for Two-Party Authenticated Key Exchange"
 * 		Jeong, Katz, Lee, 2004
 *
 * Status: 	working
 */

/* Protocol rules */

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

rule Init_1:
   [ Fr( ~ekI ), !Ltk( $I, ~lkI ), !Pk($R,'g'^~lkR) ]
   --[ SidI_1(~ekI,$I,$R, 'g'^~ekI ), Roles($I, $R) ]->
   [ Init_1( ~ekI, $I, $R, ~lkI, 'g'^~ekI ),
     !Ephk(~ekI),
     Out( < 'g'^~ekI, h( ('g'^~lkR)^~lkI,$I,$R,'g'^~ekI ) > ) ]

rule Init_2:
   [ Init_1( ~ekI, $I, $R, ~lkI , hkI), !Pk($R,'g'^~lkR), 
     In( < Y, h(('g'^~lkI)^~lkR,$R,$I,Y )>  ) ]
   --[SidI_2( ~ekI, $I, $R, hkI, Y,
       Y^~ekI ), Roles($I, $R) ]->
   [ !Sessk( ~ekI, 
       Y^~ekI ) ]

rule Resp_1:
   [ In( < X, h( ('g'^~lkR)^~lkI,$I,$R,X ) > ), Fr( ~ekR ), !Ltk($R, ~lkR), !Pk($I, 'g'^~lkI) ]
   --[ SidR_1( ~ekR, $I, $R, X, 'g'^~ekR ,
       X^~ekR ), Roles($I, $R) ]->
   [ Out( < 'g'^~ekR, h( ('g'^~lkI)^~lkR,$R,$I,'g'^~ekR ) > ),
     !Ephk(~ekR),
     !Sessk( ~ekR, 
       X^~ekR ) ]

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($A) ]->
   [ Out(k) ]


/* Security properties */

/* Only non-reflected executions */
/*
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
       
          & (All #tid A. Roles(A, A) @ tid ==> F )
        )"
*/

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

            /* Only non-reflected executions */
            & (All #tid A. Roles(A, A) @ tid ==> F )

            /* Not ephemeral-key-reveal */
            & (All #i3 t. EphkRev( t ) @ i3 ==> F)

            /* Not longterm-key-reveal */
            & (All #i3 a. LtkRev( a ) @ i3 ==> F)

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

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

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

            /* Only non-reflected executions */
            & (All #tid A. Roles(A, A) @ tid ==> F )

            /* Not ephemeral-key-reveal */
            & (All #i3 t. EphkRev( t ) @ i3 ==> F)

            /* Not longterm-key-reveal */
            & (All #i3 a. LtkRev( a ) @ i3 ==> F)

            /* Not session-key-reveal of test thread. */
            & (All #i3. SesskRev( ttest ) @ i3 ==> 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.
                   SidI_2( tpartner,I,R,hkI,hkR,kpartner ) @i3
		   & SesskRev( tpartner ) @ i4 ==> F)
    )"

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

            /* Only non-reflected executions */
            & (All #tid A. Roles(A, A) @ tid ==> F )

            /* Not ephemeral-key-reveal */
            & (All #i3 t. EphkRev( t ) @ i3 ==> F)

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

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

	    /* If there is no partner thread, then there is no longterm-key-reveal for
	       the intended partner.
	       (We model wpfs, for pfs, add i1 < i3 to conclusion) */
            & (All #i3. LtkRev( I ) @ i3 ==>
	          (Ex #i4 tpartner kpartner.
                      /* (i1 < i3) | */
                      SidR_1( tpartner,I,R,hkI,hkR,kpartner ) @i4))
            & (All #i3. LtkRev( R ) @ i3 ==>
	          (Ex #i4 tpartner kpartner.
                      /* (i1 < i3) | */
                      SidR_1( tpartner,I,R,hkI,hkR,kpartner ) @i4))
    )"

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

            /* Only non-reflected executions */
            & (All #tid A. Roles(A, A) @ tid ==> F )

            /* Not ephemeral-key-reveal */
            & (All #i3 t. EphkRev( t ) @ i3 ==> F)

            /* Not session-key-reveal of test thread. */
            & (All #i3. SesskRev( ttest ) @ i3 ==> 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.
                   SidI_2( tpartner,I,R,hkI,hkR,kpartner ) @i3
		   & SesskRev( tpartner ) @ i4 ==> F)

	    /* If there is no partner thread, then there is no longterm-key-reveal for
	       the actor or intended partner.
	       (We model wpfs, for pfs, add i1 < i3 to conclusion)
	       */
            & (All #i3. LtkRev( I ) @ i3 ==>
	          (Ex #i4 tpartner.
                       /* (i1 < i3) | */
                       SidI_1( tpartner,I,R,hkI ) @i4))
            & (All #i3. LtkRev( R ) @ i3 ==>
	          (Ex #i4 tpartner.
                       /* (i1 < i3) | */
                       SidI_1( tpartner,I,R,hkI ) @i4))
    )"
*/
end