theory MTI_C0_eCK
begin

builtins: diffie-hellman 

functions: kdf/1

section{* The MTI/C0 protocol *}

/*
 * Protocol:	MTI/C0 in the eCK model
 * Modeler: 	Benedikt Schmidt
 * Date: 	February 2012
 * Source:	"About the Security of MTI/C0 and MQV"
 *	        Sebastien Kunz-Jacques, David Pointcheval
 * 		SCN'06, Springer, 2006
 *
 * Status:      complete
 */

// Public key infrastructure
rule Register_pk:

  [ Fr(~ltk) ] 
 --> 
  [ !Ltk($A, ~ltk), !Pk($A, 'g'^~ltk), Out('g'^~ltk) ]

// Initiator
rule I1:
	let Rkey ='g'^~ltkR in
  [ Fr( ~ekI )
  , !Pk( $R, 'g'^~ltkR)  ]
 --[ SidI_1(  ~ekI, $I, $R, ('g'^~ltkR)^~ekI ),
	LogI1($I,$R,~ekI,Rkey)]->
  [ Init_1( $I, $R, 'g'^~ltkR, ~ekI )
  , Out( ('g'^~ltkR)^~ekI )
  , !EphK(~ekI) ]

   
// Responder
rule R2:
	let Ikey ='g'^~ltkI in
    [ Fr( ~ekR )
    , !Ltk( $R, ~ltkR )
    , !Pk( $I, 'g'^~ltkI )
    , In( X ) ]
  --[ AcceptedR( ~ekR, $I, $R, X, ('g'^~ltkI)^~ekR
               , kdf(  $I, $R, X, ('g'^~ltkI)^~ekR, X^(inv(~ltkR))^~ekR ) )
	, LogR2($I,$R,~ekR,~ltkR,Ikey) 
  ]->
    [ Out( ('g'^~ltkI)^~ekR )
    , !SessionKey( ~ekR
                 , kdf( $I, $R, X, ('g'^~ltkI)^~ekR, X^(inv(~ltkR))^~ekR ) )
    , !EphK(~ekR)
    ]

rule I3:
	let Rkey ='g'^~ltkR in
  [ Init_1( $I, $R, 'g'^~ltkR, ~ekI )
  , !Ltk( $I, ~ltkI)
  , In( Y ) ]
 --[ AcceptedI( ~ekI, $I, $R, ('g'^~ltkR)^~ekI, Y
              ,  kdf( $I, $R, ('g'^~ltkR)^~ekI, Y, Y^(inv(~ltkI))^~ekI ) )
	, LogI3($I,$R,~ekI,Rkey) 
 ]->
  [ !SessionKey( ~ekI , kdf( $I, $R, ('g'^~ltkR)^~ekI, Y, Y^(inv(~ltkI))^~ekI ) ) ]

           


// Reveal actions
rule Sessionkey_Reveal:
    [ !SessionKey(~tid, k) ]
  --[ SesskRev(~tid) ]->
    [ Out(k) ]

// Longterm Key reveal
rule Ltk_Reveal:
    [ !Ltk(~A, k) ]
  --[ LtkRev(~A) ]->
    [ Out(k) ]

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 ekI I R k hkI hkR.
            AcceptedI(ekI, 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( ekI ) @ i4)

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

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

            /* Not both long-term-key-reveal and ephemeral-key-reveal
	     * for matching session */
            & not(Ex #i3 #i4 #i5 ekR kpartner.
                  AcceptedR( ekR,I,R,hkI,hkR,kpartner ) @i3
		  & LtkRev( R ) @ i4
		  & EphkRev( ekR ) @ 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 ==>
                  /* (i1 < i3) | */
	          (Ex #i4 ekR kpartner.
                      AcceptedR( ekR,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 ekR I R k hkI hkR.
            AcceptedR(ekR, 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( ekR ) @ i4)

            /* Not session-key-reveal of test thread. */
            & not(Ex #i3. SesskRev( ekR ) @ 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 ekI kpartner.
                   AcceptedI( ekI,I,R,hkI,hkR,kpartner ) @i3
		   & SesskRev( ekI ) @ i4 )

            /* If there is a partner thread, then not long-term-key-reveal and ephemeral-key-reveal. */
            & not(Ex #i3 #i4 #i5 ekI.
                  SidI_1( ekI,I,R,hkI ) @i3
		  & LtkRev( I ) @ i4
		  & EphkRev( ekI ) @ 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 ==>
                  /* (i1 < i3) | */
	          (Ex #i4 ekI.
                       SidI_1( ekI,I,R,hkI ) @i4)))"


end