theory UM_three_pass_combined
begin

/*
    The three-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
*/

builtins: diffie-hellman, hashing, multiset
functions: MAC/2, first/1, second/1, concat/2
equations: concat(first(x), second(x)) = x

/* 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 


/* UM3 Initiator */

// UM3 session creation for initiator:
//     choose ephemeral private key, compute ephemeral public key X, and send
rule I_Activate:
  let X   = 'g'^~ex             // the ephemeral public key
      sid = <'UM3', $A, $B, X>  // the session id is unique
  in
  [ Fr( ~ex ) ]                    // select random ephemeral private key
  --[ Activate( sid )
    , Sid( sid )
    , Agents($A,$B) ]->          // 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
  , Out( X )                       // send message
  ]

// UM3 session update for initiator:
//    receive key confirmation and Y, compute key, check key confirmation.
rule I_Complete:
  let X       = 'g'^~ex                    // recompute X                                           
      pB      = 'g'^~eb                    // we do not model key registration by adversary,
                                           // hence key always of this form
      kstring = h(Y^~ex, pB^~ea, $A, $B, X, Y, 'UM3')   // we do not include the public string Lambda
      key     = second(kstring)
      conf    = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1
      confB   = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2
      sidOld  = <'UM3',$A, $B, <'1',X>>
      sid     = <'UM3',$A, $B, <'1',X> + <'2', <Y,confB>> + <'3', conf> >  // new sid
  in
  [ I_Act( ~ex, $A, $B )                   // this session was activated
  , In( <Y, confB> )
  , !Ltk( $A, ~ea )                        // lookup own longterm private key
  , !Pk( $B, pB ) ]                        // lookup peer's public key
  --[ Complete( sid, 'I', key )            // sid is 'Complete'd after this step
    , SidUpdated( sidOld )
    , Sid( sid ) ]->                      
  [ I_Comp( sid )                          // state of this session
  , Out( conf )
  , !SessionKey( sid, $A, key ) ]          // the session key of sid with actor $A, available
                                           // for reveals
// UM3 session expiration
rule I_Expire:
  [ I_Comp( sid ) ]
  --[ Expire( sid ) ]->  // sid is expired after this step
  [ ]


/* UM3_Responder */
// Session creation:
rule R_Activate:
  let pA  = 'g'^~ea                      // we do not model key registration by adversary,
                                         // hence key always of this form
      Y   = 'g'^~ey
      kstring = h(X^~ey, pA^~eb, $A, $B, X, Y, 'UM3')
      key     = second(kstring)
      conf    = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2
      sid = <'UM3', $B, $A, <'1',X> + <'2',<Y, conf>> >  // sid is unique


  in
  [ Fr( ~ey )
  , In( X )
  , !Ltk( $B, ~eb )
  , !Pk( $A, pA ) ]
  --[ Activate(sid)
    , Sid( sid )
    , Agents($A,$B) ]-> 
  [ Out( <Y,conf>)
  , R_Act( ~ey, $B, $A, X )
  , !SessionState( sid, $A, ~ey )
  ]

// Session update:
rule R_Complete:
  let pA  = 'g'^~ea
      Y   = 'g'^~ey
      kstring = h(X^~ey, pA^~eb, $A, $B, X, Y, 'UM3' )
      key     = second(kstring)
      confA   = MAC(first(kstring), <'R', $B, $A, Y, X>) // we do not include Lambda_1
      conf    = MAC(first(kstring), <'I', $A, $B, X, Y>) // we do not include Lambda_2
      sidOld  = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>>> // sid is unique
      sid = <'UM3', $B, $A, <'1',X> + <'2', <Y, conf>> + <'3', confA> > // sid is unique
  in
  [ R_Act( ~ey, $B, $A, X )
  , In( confA )
  , !Ltk( $B, ~eb )
  , !Pk( $A, pA )
  ]
  --[ Complete( sid, 'R', key )             // sid is 'Complete'd after this step
    , SidUpdated( sidOld )
    , Sid( sid ) ]->
  [ R_Comp( sid )
  , !SessionKey( sid, $B, key ) ]          // the session key of sid with actor $B, available
                                           // for reveals
rule R_Expire:
  [ R_Comp( sid ) ]
  --[ Expire( sid ) ]->
  [ ]


/* UM1 Initiator */
// We prefix all facts with UM1

// Activate the session: choose ephemeral private key, compute ephemeral public key X.
rule UM1_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
  --[ UM1_Activate( sid ) ]->          // sid is 'Activate'd after this step
  [ UM1_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 UM1_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, X, pB, 'UM1') // we do not include the public string
  in
  [ UM1_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
  --[ UM1_Complete( sid, 'I', k ) ]->          // sid is 'Complete'd after this step
  [ UM1_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 UM1_I_Expire:
  [ UM1_I_Comp( sid ) ]
  --[ UM1_Expire( sid ) ]->  // sid is expired after this step
  [ ]


/* UM1 Responder */

// R has no Activated state since there is no ephemeral key.
rule UM1_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, X, 'g'^~eb, 'UM1' )
  in
  [ In( X )
  , !Ltk( $B, ~eb )
  , !Pk( $A, pA ) ]
  --[ UM1_Activate(sid)
    , UM1_Complete( sid, 'R', k )
    ]-> // sid is 'Complete'd and 'Activate'd after this step
  [ UM1_R_Comp( sid )
  , !SessionKey( sid, $B, k )
  ]

rule UM1_R_Expire:
  [ UM1_R_Comp( sid ) ]
  --[ UM1_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. UM1_Activate(sid) @ i & UM1_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"

// this assumption is used in the proof. Without this restriction, a completed
// session with actor and peer A is its own matching session.
axiom actor_ineq_peer:
   "not (Ex #i A. Agents(A,A) @ i)"

// 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_UM3:
  "(All #i #j role A B k s comm.
       /* The key of a complete session 's' is known */
       Complete( <'UM3',A,B,comm> , role,  k ) @ i & K( k ) @ j & s = <'UM3',A,B,comm>
       /* then one of the following must have happened */
       ==>
       /* 1. (a) The session key of s was revealed  (see 4. for 1. (b)) */
         (Ex #k. SessionKeyReveal( s ) @ k)

      /* 2. Corrupt(A) before Expire(s) */
      |  (Ex #k. Corrupt(A) @ k &
                 ( not (Ex #l. Expire(s) @ l & l < k)))
      
      /* 3. SessionStateReveal(s) and either Corrupt(A) or Corrupt(B) */
      |  (Ex #k. SessionStateReveal(s) @ k
          & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))

      /* 4. s* exists and */
      |  (Ex #l ms matchingComm.
           Sid(<'UM3',B,A,matchingComm>) @ l
           & ms = <'UM3',B,A,matchingComm>
           & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)
           // the session has not been updated
           & not (Ex #v. SidUpdated(ms) @ v)

         & (
           /* SessionKeyReveal(s*) (see 1. (b)) */
             (Ex #k. SessionKeyReveal( ms ) @ k)
           /* (a) Corrupt(B) before Expire(s*) */
           | (Ex #k. Corrupt(B) @ k &
                 (not (Ex #l. Expire(ms) @ l & l < k)))
           /* (b) SessionStateReveal(s*) and either Corrupt(A) or Corrupt(B) */
           | (Ex #k. SessionStateReveal(ms) @ k
              & ((Ex #l. Corrupt(A) @ l) | (Ex #l. Corrupt(B) @ l)))))

      /* 5. s* does not exist and Corrupt(B) before Expire(s) */
      |  ((not (Ex #l matchingComm.
                Sid(<'UM3',B,A,matchingComm>) @ l
                & ((Ex rest. matchingComm + rest = comm) | matchingComm = comm)
                // the session has not been updated
                & not (Ex #v. SidUpdated(<'UM3',B,A,matchingComm>) @ v)))
                
          & (Ex #k. Corrupt(B) @ k &
               (not (Ex #l. Expire(s) @ l & l < k)))))"

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') */
       UM1_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 initiator session and */
            (Ex #k k_. UM1_Complete( sp, 'I', 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 initiator session and */
            (  (not (Ex #k k_ . UM1_Complete( sp, 'I', k_) @ k))
            /* there is corrupt B */
             & (Ex #k. Corrupt(B) @ k))))"       
end