UM_one_pass_private.spthy

theory UM_one_pass_private
begin

/*
 * Protocol:	UM one-pass protocol using a private channel, derived from UM_one_pass_eCK_like
 *              See
 *              "Combined Security Analysis of the One- and Three-Pass Unified Model Key Agreement Protocols"
 *               Sanjit Chatterjee, Alfred Menezes, and Berkant Ustaoglu
 *
 * Modeler: 	Benedikt Schmidt
 * Date: 	October 2012
 * Source:	"Ph.D. Thesis: Formal Analysis of
 *               Key Exchange Protocols and Physical
 *               Protocols"
 *
 * Status: 	Working
 * Comment:     This is the P_UM' example that is used as a running example for my thesis.
 */


builtins: diffie-hellman, hashing

rule Generate_key:
  let pkA = 'g'^~ea
  in
  [ Fr( ~ea ) ] 
  --[ ]-> 
  [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]

rule Initiator:
  let pB = 'g'^~eb
      X  = 'g'^~ex
      sid = <$A, $B, X, 'I'>
      key  = h(pB^~ex, pB^~ea, $A, $B, X)
  in
  [ Fr( ~ex ), !Ltk( $A, ~ea ), !Pk( $B, pB ) ]
  --[ Accept( sid, key ) ]->
  [ PChan( X ), !Ephk( sid, ~ex ) ]

rule Responder:
  let pA  = 'g'^~ea
      sid = <$B, $A, X, 'R'>
      key  = h(X^~eb, pA^~eb, $A, $B, X)
  in
  [ PChan( X ), !Ltk( $B, ~eb ), !Pk( $A, pA ) ]
  --[ Accept( sid, key ) ]->
  []

rule Ephemeral_Reveal:
  [ !Ephk( sid, ~x ) ]
  --[ RevealEphk( sid ) ]->
  [ Out( ~x ) ]

rule Ltk_Reveal:
  [ !Ltk( $A, ~ea ) ]
  --[ RevealLtk( $A ) ]->
  [ Out( ~ea ) ]

lemma UM_executable:
  exists-trace
  "Ex #i #j A B X key.
     // An initiator and session
       Accept( <A,B,X,'I'>, key ) @ i
     // and a matching responder session accept key
     & Accept( <B,A,X,'R'>, key ) @ j
     // and the the adversary did not perform any reveals.
     & (not (Ex #j C. RevealLtk( C ) @ j))
     & (not (Ex #j s. RevealEphk( s ) @ j))"

end