theory SignedDH_eCK
begin

builtins: diffie-hellman, signing

section{* The Signed Diffie-Hellman Protocol in the eCK model *}

/*
 * Protocol:	Signed Diffie-Hellman
 * Modeler: 	Simon Meier, Benedikt Schmidt
 * Date: 	January 2012
 * Property:	eCK model
 * 		"Stronger Security of Authenticated Key Exchange"
 * 		LaMacchia, Lauter, Mityagin, 2007
 *
 * Status: 	working
 */

// Public key infrastructure
rule Register_pk:
    [ Fr(~ltk) ] 
  --> 
    [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)), Out(pk(~ltk)) ]

// Protocol
/* Initiator */
rule Init_1:
    [ Fr(~ekI), !Ltk($I, ltkI) ]
  --[ SidI_1(~ekI, $I, $R, 'g'^~ekI) ]->
    [ Init_1( ~ekI, $I, $R, ~ekI, 'g' ^ ~ekI )
    , !Ephk(~ekI)
    , Out( <$I, $R, 'g' ^ ~ekI, sign{'1', $I, $R,'g' ^ ~ekI }ltkI> ) ]

rule Init_2:
    [ Init_1( ~ekI, $I, $R, ~ekI, hkI )
    , !Pk($R, pk(ltkR))
    , In( <$R, $I, Y, sign{'2', $R, $I, Y }ltkR> ) 
    ]
  --[ SidI_2(~ekI, $I, $R, hkI, Y, Y ^ ~ekI ) ]->
    [ !Sessk(~ekI, Y ^ ~ekI) ]

/* Responder */
rule Resp:
    [ !Pk($I, pk(ltkI))
    , !Ltk($R, ltkR)
    , Fr(~ekR)
    , In( <$I, $R, X, sign{'1', $I, $R, X }ltkI> ) 
    ]
  --[ SidR_1(~ekR, $I, $R, X, 'g' ^ ~ekR, X ^ ~ekR) ]->
    [ !Ephk(~ekR)
    , !Sessk(~ekR, X ^ ~ekR)
    , Out( <$R, $I, 'g' ^ ~ekR, sign{'2', $R, $I, 'g' ^ ~ekR }ltkR> ) 
    ]

/* 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(~ekA) ]
   --[ EphkRev(~ekA) ]->
   [ Out(~ekA) ]

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

            /* Not both longterm-key-reveal _and_ ephemeral-key-reveal
	     * for test thread. */
            & not(Ex #i3 #i4. LtkRev( I ) @ i3 & EphkRev( ttest ) @ i4)

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

            /* No session-key-reveal for matching session. */
            & not(Ex #i3 #i4 tpartner kpartner.
                   SidR_1( tpartner,I,R,hkI,hkR,kpartner ) @i3
		   & SesskRev( tpartner ) @ i4 )

            /* Not both long-term-key-reveal and ephemeral-key-reveal
	     * for matching session */
            & not(Ex #i3 #i4 #i5 tpartner kpartner.
                  SidR_1( tpartner,I,R,hkI,hkR,kpartner ) @i3
		  & LtkRev( R ) @ i4
		  & EphkRev( tpartner ) @ i5 )

	    /* Longterm-key-reveal of partner only if there is a
	     * matching session. */
	    /* (We model eCK-wpfs, for eCK-pfs, add i1 < i3 to conclusion) */
            & (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 eCK if the session key of the test session is deduced and
   the test session is clean.
*/
lemma eCK_responder_key:
  "not (Ex #i1 #i2 ttest I R k hkI hkR.
            SidR_1(ttest, I, R, hkI, hkR, k) @ i1 & K( k ) @ i2

            /* Not longterm-key-reveal _and_ ephemeral-key-reveal of actor . */
            & not(Ex #i3 #i4. LtkRev( R ) @ i3 & EphkRev( ttest ) @ i4)

            /* Not session-key-reveal of test thread. */
            & not(Ex #i3. SesskRev( ttest ) @ i3 )

            /* 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.
	    */
            & not(Ex #i3 #i4 tpartner kpartner.
                   SidI_2( tpartner,I,R,hkI,hkR,kpartner ) @i3
		   & SesskRev( tpartner ) @ i4 )

            /* If there is a partner thread, then not long-term-key-reveal and ephemeral-key-reveal. */
            & not(Ex #i3 #i4 #i5 tpartner.
                  SidI_1( tpartner,I,R,hkI ) @i3
		  & LtkRev( I ) @ i4
		  & EphkRev( tpartner ) @ i5 )

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

end