theory Scott
begin

builtins: bilinear-pairing

functions: kdf/1, hp/1

section{* Scott: MTI-C0 like identity based key exchange protocol *}

/*
 * Protocol:	Scott
 * Modeler: 	Benedikt Schmidt
 * Date: 	May 2012
 * Source:	Boyd overview identity based key exchange protocols
 *
 * Status: 	Working
 */


// Key generation center

rule KGC_Setup:
  [ Fr( ~msk ) ]
  --[ KGCSetup() ]->
  [ !MSK( ~msk ) ]

rule KGC_request:
  [ !MSK( ~msk ) ]
  -->
  [ !LTK( $ID, pmult( ~msk, hp($ID) ) ) ]


// Reveals

rule Reveal_ltk:
  [ !LTK( $ID, skID ) ]
  --[ LtkRev($ID) ]->
  [ Out(skID) ]

rule Reveal_master_key:
  [ !MSK( ~msk ) ]
  --[ MskRev() ]->
  [ Out( ~msk ) ]

rule Reveal_session_key:
  [ !Sessk( ~ey, sek ) ]
  --[ SesskRev( ~ey ) ]->
  [ Out( sek ) ]

rule Reveal_ephmeral_key:
  [ !Ephk( ~ey ) ]
  --[ EphkRev( ~ey ) ]->
  [ Out( ~ey ) ]


// Protocol

rule Init_1:
  let skA = pmult( ~s, hp($A) )
      X   = em( skA, hp($B) )^~ex
  in 
  [ Fr( ~ex )
  , !LTK( $A, skA )
  ]
  -->
  [ Init( ~ex, $A, $B, X )
  , Out( X )
  , !Ephk( ~ex )
  ]

rule Init_2:
  let sessKey = kdf( Y^~ex, $A, $B, X, Y )
  in
  [ Init( ~ex, $A, $B, X )
  , In( Y )
  ]
  --[ Accept( ~ex, $A, $B, sessKey )
    , Sid( ~ex, <'Init',$A,$B,X,Y> )
    // a matching session for ~ex has the following sid
    , Match( ~ex, <'Resp',$B,$A,X,Y> )
    ]->
  [ !Sessk( ~ex, sessKey ) ]


rule Resp_1:
  let skB     = pmult( ~s, hp($B))
      Y       = em(hp($A), skB)^~ey
      sessKey = kdf(X^~ey, $A, $B, X, Y)
  in
  [ Fr( ~ey )
  , !LTK( $B, skB )
  , In( X )
  ]
  --[ Accept( ~ey, $B, $A, sessKey )
    , Sid( ~ey, <'Resp',$B,$A,X,Y> )
    // a matching session for ~ey has the following sid
    , Match( ~ey, <'Init',$A,$B,X,Y> )
    ]->
  [ Out( Y )
  , !Sessk( ~ey, sessKey )
  , !Ephk( ~ey) 
  ]


lemma key_agreement_reachable:
  exists-trace
  "Ex #i #j A B SID t1 t2 k.
        Accept(t1, A, B, k)  @ i
      & Match(t1,  SID) @ i
      & Accept(t2, B, A, k)   @ j
      & Sid(t2, SID)   @ j"



lemma key_secrecy:
  /* 
   * We allow ephemeral key reveals here.
   * There is a simple attack where another session of
   * A is used to get em(hp(A), hp(B))^s which is then sent
   * to A as Y. Then A uses X = em(hp(A), hp(B))^(s*ex) as
   * input for the kdf.
   * 
   * If there exists a Test session whose key k is known to the
   * Adversary, then...
   */
  "(All #i1 #i2 test A B k.
    Accept(test, A, B, k) @ i1 & K( k ) @ i2
    ==> ( 
    // ... the test session must be "not clean".
    // test is not clean if one of the following has happened:
    //
    // session-key-reveal of test thread.
      (Ex #i3. SesskRev( test ) @ i3 )
    
    // more than one KGC
    | (Ex #i3 #i4. KGCSetup() @ i3 & KGCSetup() @ i4 & not (#i3 = #i4))
    
    // Ephemeral Key reveal and long-term key reveal for test session
    | (Ex #i5. EphkRev( test ) @ i5 & Ex #i6. LtkRev( A ) @ i6)

    // there is a matching session
    | (Ex matching #i3 #i4 sid.
    	   // matching's 'sid' info matches with test
           ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)
	   & ( 
             // matching's session key was revealed
	       (Ex #i5. SesskRev( matching ) @ i5 )

             // Ephemeral Key reveal and long-term key reveal for test session
            | (Ex #i5. EphkRev( matching ) @ i5 & Ex #i6. LtkRev( B ) @ i6)
	   )
      )

    // there is no matching session
    | (  (not (Ex matching #i3 #i4 sid.
    	   // matching's 'sid' info matches with test
           ( Sid ( matching, sid ) @ i3 & Match( test, sid ) @ i4)))

        & (  
          // the longterm key of test.peer was revealed
            (Ex #i5. LtkRev( B ) @ i5 )

          // the longterm key of test.actor was revealed
          | (Ex #i3. LtkRev(A) @ i3 )
          
          // the master key was revealed
          | (Ex #i3. MskRev() @ i3)
          )
      )

    )
  )"

end