UM_one_pass_attack.spthy

theory UM_one_pass_attack
begin

/*
    The one-pass UM protocol. See
    "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"
    Sanjit Chatterjee, Alfred Menezes and Berkant Ustaoglu

    The last property is not valid for the model since there
    is a flaw in the definition of the model and the proof.
    
    The problem is that the session id does not contain the
    role and since this is a one-pass protocol, this means
    that a responder session <A,B,X> can match another
    responder session <B,A,X> if X is replayed.
*/

builtins: diffie-hellman, hashing

/* Key registration */

rule Register_key_honest:
  let pkA = 'g'^~ea
  in
  [ Fr( ~ea )           // select random longterm private
  ] 
  --[ KeyReg( $A ) ]->  // a key for A has been registered
  [ !Ltk( $A, ~ea )     // ~ea is the longterm private key of A
  , !Pk( $A, pkA )      // pkA = 'g'^~ea is the longterm public key of A
  , Out( pkA ) ]        // the adversary can learn the public key 

/* Initiator */


// Activate the session: choose ephemeral private key, compute ephemeral public key X.
rule I_Activate:
  let X   = 'g'^~ex        // the ephemeral public key
      sid = <$A, $B, X>    // the session id, not unique because there might
                           // be responder session with actor B and peer A
                           // which receives X
  in
  [ Fr( ~ex ) ]                    // select random ephemeral private key
  --[ Activate( sid ) ]->          // sid is 'Activate'd after this step
  [ I_Act( ~ex, $A, $B )           // the state of this session, identified by ex (unique)
  , !SessionState( sid, $A, ~ex )  // the session state of sid with actor $A consists only of ex,
                                   // available for reveals
  ]

// Complete the session: send X, and compute key.
rule I_Complete:
  let X  = 'g'^~ex                         // recompute X
      sid = <$A, $B, X>                    // recompute sid
      pB = 'g'^~eb                         // we do not model key registration by adversary,
                                           // hence key always of this form
      k  = h(pB^~ex, pB^~ea, $A, $B)       // we do not include the public string
  in
  [ I_Act( ~ex, $A, $B )                   // this session was activated
  , !Ltk( $A, ~ea )                        // lookup own longterm private key
  , !Pk( $B, pB ) ]                        // lookup peer's public key
  --[ Complete( sid, 'I', k ) ]->          // sid is 'Complete'd after this step
  [ I_Comp( sid )                          // state of this session
  , Out( <$B, $A, X> )                     // send message
  , !SessionKey( sid, $A, k ) ]            // the session key of sid with actor $A, available
                                           // for reveals
// Expire the session
rule I_Expire:
  [ I_Comp( sid ) ]
  --[ Expire( sid ) ]->  // sid is expired after this step
  [ ]


/* Responder */

// R has no Activated state since there is no ephemeral key.
rule R_Complete:
  let pA  = 'g'^~ea                      // we do not model key registration by adversary,
                                         // hence key always of this form
      sid = <$B, $A, X>                  // sid is not unique because of initiator sessions with
                                         // same sid and replay
      k   = h(X^~eb, pA^~eb, $A, $B)
  in
  [ In( X )
  , !Ltk( $B, ~eb )
  , !Pk( $A, pA ) ]
  --[ Activate(sid), Complete( sid, 'R', k ) ]-> // sid is 'Complete'd and 'Activate'd after this step
  [ R_Comp( sid )
  , !SessionKey( sid, $B, k )
  ]

rule R_Expire:
  [ R_Comp( sid ) ]
  --[ Expire( sid ) ]-> // sid is expired after this step
  [ ]

/* Corrupt an agent:
   We model corruption by three different rules.
   We do not model static key selection for corrupted agents.
*/

// Corrupt and obtain longterm key
rule Corrupt_Ltk:
  [ !Ltk( $A, ~ea ) ]
  --[ Corrupt( $A ) ]->
  [ Out( ~ea ) ]

// Corrupt and obtain session state. Must occur before complete which
// we ensure with BeforeComplete action and axiom.
rule Corrupt_SessionState:
  [ !SessionState( sid, ~x, $A ) ]
  --[ Corrupt( $A ), BeforeComplete( sid ) ]->
  [ Out( ~x ) ]

// Corrupt and obtain session key. Must occur before expire which
// we ensure with BeforeExpire action and axiom.
rule Corrupt_SessionKey:
  [ !SessionKey( sid, $A, k ) ]
  --[ Corrupt( $A ), BeforeExpire( sid ) ]->
  [ Out( k ) ]

/* Reveals for session state and session key */

rule Reveal_SessionState:
  [ !SessionState( sid, ~x, $A ) ]
  --[SessionStateReveal( sid ), BeforeComplete( sid ) ]->
  [ Out( ~x ) ]

rule Reveal_SessionKey:
  [ !SessionKey( sid, $A, k) ]
  --[ SessionKeyReveal( sid ), BeforeExpire( sid ) ]->
  [ Out( k ) ]

/* We only consider traces which satisfy these axioms */

// we enforce unique sids since the paper states that "At any point in time a session is
// in exactly one of the following states: active, completed, aborted, expired."
axiom sid_unique:
   "All #i #j sid. Activate(sid) @ i & Activate(sid) @ j ==> #i = #j"

// every agent has at most one registered key
axiom keyreg_unique:
   "All #i #j A. KeyReg(A) @ i & KeyReg(A) @ j ==> #i = #j"

// The reveals and the corrupt rules that reveal session state and session key are not performed
// too late.
axiom corrupt_and_reveal_not_too_early:
   "  (All #i #j s role_ k_. BeforeComplete( s ) @ i & Complete(s, role_, k_ ) @ j ==> #i < #j)
    & (All #i #j s.          BeforeExpire( s )   @ i & Expire( s ) @ j ==> #i < #j)"

// Key agreement for initiator and responder is reachable without any adversary interaction.
lemma key_agreement_reachable:
  exists-trace
  "Ex #i #j sid sidm k.
       Complete( sid , 'I', k ) @ i
     & Complete( sidm, 'R', k ) @ j
     & (not (Ex #j C. Corrupt( C ) @ j))
     & (not (Ex #j s. SessionKeyReveal( s ) @ j))
     & (not (Ex #j s. SessionStateReveal( s ) @ j))"


lemma CK_secure:
  "(All #i #j role A B X k s sp.
       /* The key of a complete session 's' is known (whose partner is 'sp') */
       Complete( <A,B,X> , role,  k ) @ i & K( k ) @ j & s = <A,B,X> & sp = <B,A,X>
       /* then one of the following must have happened */
       ==>
       /* 1. (a) The session key of s was revealed */
         (Ex #k. SessionKeyReveal( s ) @ k)

       /*    (b) the session key of some s* was revealed */
       | (Ex #i1. SessionKeyReveal( sp ) @ i1)

       | (/* 2. s is an initiator session */ 
          (role = 'I') &
     
          ( /* (a) A was corrupted before expire*/ 
            (Ex #k. Corrupt(A) @ k &
                       (  (Ex #l. Expire(s) @ l & k < l)
                       |  not (Ex #l. Expire(s) @ l )))

          | /* (b) A was corrupted and s's session state was revealed */
            (Ex #k #l. SessionStateReveal(s) @ k & Corrupt(A) @ l)

          | /* (c) B was corrupted */
            (Ex #k. Corrupt(B) @ k )))

       | (/* 2. s is a responder session */ 
          (role = 'R') &

          ( /* (a) A was corrupted */
            Ex #k. Corrupt(A) @ k )

          | /* (b) There is a matching session and */
            (Ex #k k_ role_. Complete( sp, role_, k_ ) @ k
                 
               /* there is a corrupt B before expire s* */
               & (  (Ex #k. Corrupt(B) @ k & 
                       (  (Ex #l. Expire(sp) @ l & k < l)
                       |  not (Ex #l. Expire(sp) @ l )))

                 /* or both session state reveal s* and corrupt B */
                 |  (Ex #k #l. SessionStateReveal(sp) @ k & Corrupt(B) @ l )))

          | /* (c) There is no matching session and */
            (  (not (Ex #k k_ role_. Complete( sp, role_, k_) @ k))
            /* there is corrupt B */
             & (Ex #k. Corrupt(B) @ k))))"

end