theory DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching
begin

builtins: diffie-hellman, multiset

/*
 * Protocol:	NAXOS-C
 * Modeler: 	Cas Cremers, Benedikt Schmidt
 * Date: 	January 2012/April 2012/September 2012
 * Source:	"Reusing Static Keys in Key Agreement Protocols"
 * 		Chatterjee, Menezes, Ustaoglu
 * Property: 	eCK-PFS security
 *
 * Status: 	Working
 */

functions: h1/1, h2/1, h/1
functions: first/1, second/1, concat/2
equations: concat(first(x), second(x)) = x

/* Protocol rules */

/* In the description in the paper, we omitted the sorts. 
 * In this description they are made explicit.
 * '$A' is equivalent to 'A:pub'
 * '~x' is equivalent to 'x:fresh'
 */

/* Generate long-term keypair */
rule generate_ltk:
   let pkA = 'g'^~ea 
   in
   [ Fr(~ea) ] 
   --[ RegKey($A), Honest($A) ]->
   [ !Ltk( $A, ~ea ), !Pk( $A, pkA ), Out( pkA ) ]

/* Keyreg dishonest */
rule generate_ltk_dishonest:
   [ In(pkA) ]
   --[ RegKey($A) ]->
   [ !Pk( $A, pkA ) ]

/* NAXOS Initiator */
rule Init_NAXOS_1:
  let X = 'g'^h1(<~ex, ~ea >)
  in
  [   Fr( ~ex ), !Ltk( $A, ~ea ) ]
  --[ Sid( ~ex, < $A, $B, <'1',X> , 'Init', 'NAXOS_C' >)]->
  [ Init_1( ~ex, $A, $B, ~ea, X )
  , !Ephk(~ex, ~ex)
  , Out( X ) ]

rule Init_NAXOS_2:
  let exp     = h1( < ~ex, ~ea > )
      kstring = h( < Y^~ea, KB^exp, Y^exp, $A, $B, X, Y, 'NAXOS_C' > )
      key     = second( kstring )
      conf    = h2( < first( kstring ), 'I', $A, $B, X, Y, 'NAXOS_C' > )
      confB   = h2( < first( kstring ), 'R', $B, $A, Y, X, 'NAXOS_C' > )
  in
  [ Init_1( ~ex, $A, $B, ~ea, X), !Pk( $B, KB )
  , In( <$B, Y, confB> ) ]
  --[ Accept( ~ex, key)
    , Sid( ~ex, < $A, $B, (<'1',X> + <'2',Y> + <'3',<$A, conf>>), 'Init' , 'NAXOS_C'>)
    ]->
  [ Out( <$A, conf> )
  , !Sessk( ~ex, key) ]

/* NAXOS Responder */
rule Resp_NAXOS_1:
  let exp     = h1( < ~ey, ~eb > )
      Y       = 'g'^exp
      kstring = h( < KA^exp, X^~eb, X^exp, $A, $B, X, Y, 'NAXOS_C' > )
      key     = second( kstring )
      conf    = h2( < first( kstring ), 'R', $B, $A, Y, X, 'NAXOS_C' > )
      confA   = h2( < first( kstring ), 'I', $A, $B, X, Y, 'NAXOS_C' > )
  in
   [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA)
   , In( X ) ]
   --[ Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>), 'Respo', 'NAXOS_C' > ) ]->
   [ Out( <$B,Y,conf> )
   , Resp_1( ~ey, $B, $A, Y , X, confA, key )
   , !Ephk(~ey, ~ey) ]

rule Resp_NAXOS_2:
     [ Resp_1( ~ey, $B, $A, Y, X, confA, key )
     , In( <$A, confA> ) ]
     --[ Accept( ~ey, key )
       , Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>+ <'3',<$A,confA>>), 'Respo', 'NAXOS_C' > )
       ]->
       [ !Sessk( ~ey, key) ]


/* DHKEA Initiator */

rule Init_DHKEA_1:
  let X = 'g'^h1(<~ex, ~ea >)
  in
  [   Fr( ~ex ), !Ltk( $A, ~ea ) ]
  --[ Sid( ~ex, < $A, $B, <'1',X>, 'Init', 'DHKEA' >)
  ]->
  [ Init_DHKEA_1( ~ex, $A, $B, ~ea, X )
  , !Ephk(~ex, ~ex)
  , Out( X ) ]

rule Init_DHKEA_2:
  let KB      = 'g'^~eb
      exp     = h1( < ~ex, ~ea > )
      kstring = h( < Y^exp, $A, $B, X, Y, 'DHKEA' > )
      key     = second( kstring )
      conf    = h2( < first( kstring ), Y^~ea,  'I', $A, $B, X, Y, 'DHKEA' > )
      confB   = h2( < first( kstring ), KB^exp, 'R', $B, $A, Y, X, 'DHKEA' > )
  in
  [ Init_DHKEA_1( ~ex, $A, $B, ~ea, X), !Pk( $B, KB )
  , In( <$B, Y, confB> ) ]
  --[ Accept( ~ex, key)
    , Sid( ~ex, < $A, $B, (<'1',X> + <'2',Y> + <'3',<$A, conf>>), 'Init', 'DHKEA' >)
    ]->
  [ Out( <$A, conf> )
  , !Sessk( ~ex, key) ]

/* DHKEA Responder */
rule Resp_DHKEA_1:
  let KA      = 'g'^~lkI
      exp     = h1( < ~ey, ~eb > )
      Y       = 'g'^exp
      kstring = h( < X^exp, $A, $B, X, Y, 'DHKEA' > )
      key     = second( kstring )
      conf    = h2( < first( kstring ), X^~eb,  'R', $B, $A, Y, X, 'DHKEA' > )
      confA   = h2( < first( kstring ), KA^exp, 'I', $A, $B, X, Y, 'DHKEA' > )
  in
   [ Fr( ~ey ), !Ltk($B, ~eb), !Pk($A, KA)
   , In( X ) ]
   --[ Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>), 'Respo', 'DHKEA' > )
   ]->
   [ Out( <$B,Y,conf> )
   , Resp_DHKEA_1( ~ey, $B, $A, Y , X, confA, key )
   , !Ephk(~ey, ~ey) ]

rule Resp_DHKEA_2:
     [ Resp_DHKEA_1( ~ey, $B, $A, Y, X, confA, key )
     , In( <$A, confA> ) ]
     --[ Accept( ~ey, key )
       , Sid( ~ey, < $B, $A, (<'1',X> + <'2',Y>+ <'3',<$A,confA>>), 'Respo', 'DHKEA' > )
       ]->
       [ !Sessk( ~ey, key) ]


/* Key Reveals for the eCK model */
rule Sessk_reveal: 
   [ !Sessk(~s, k) ] --[ RevealSessk(~s) ]-> [ Out(k) ]

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

rule Ephk_reveal:
   [ !Ephk(~s, ~ek) ] --[ RevealEphk(~s) ]-> [ Out(~ek) ]



axiom RegKeyUnique:
      "All #i #j A. RegKey(A) @ i & RegKey(A) @ j ==> #i = #j"


/* Security properties */

lemma execution_match_same_key_NAXOS:
  exists-trace
  "Ex #i1 #i2 s1 s2 k A B com role1 role2.
       Accept( s1, k) @ i1
     & Accept( s2, k) @ i2
     & Sid( s1, <A,B,com,role1, 'NAXOS_C'> ) @ i1
     & Sid( s2, <B,A,com,role2, 'NAXOS_C'> ) @ i2
     & not (role1 = role2)"


lemma eCK_key_secrecy:
  /* 
   * The property specification is a (logically equivalent) simplified
   * version of the one in the original eCK (ProvSec) paper:
   *
   * If there exists a test session whose key k is known to the
   * Adversary with some session-id, then...
   */
  "(All #i1 #i2 #i3 #i4 test A B k com role proto.
    Accept(test, k) @ i1 & K( k ) @ i2
    & Sid(test, < A, B, com, role, proto> ) @ i1 // we want the last Sid at the same time as Accept
    & Honest(A) @ i3 & Honest(B) @ i4
    ==> ( 
    /* ... the test session must be "not clean".
     * test is not clean if one of the following has happened:
     */
    /* 1. The adversary has revealed the session key of the test session. */
      (Ex #i3. RevealSessk( test ) @ i3 )
    
    /* 2. The adversary has revealed both the longterm key of A and the
          ephemeral key of the test session */
    |  (Ex #i5 #i6. RevealLtk  ( A ) @ i5  & RevealEphk ( test  ) @ i6 )

    /* 3. There is a matching session and */
    | (Ex matchingSession #i3 matchingRole matchingCom.
           (   Sid ( matchingSession, < B, A, matchingCom, matchingRole, proto > ) @ i3 
             & not ( matchingRole = role )
             & ((Ex rest. matchingCom + rest = com) | (matchingCom = com))
             & not (Ex #i4 sid. Sid ( matchingSession, sid) @ i4 & #i3 < #i4))
	   & (
             /* (a) the adversary has revealed the session key of the matching session, or */
	       (Ex #i5. RevealSessk( matchingSession ) @ i5 )

             /* (b) the adversary has revealed the longterm key of B and the ephemeral
                    key of the matching session. */
             | (Ex #i5 #i6. RevealLtk  ( B ) @ i5  & RevealEphk ( matchingSession ) @ i6 )
	   )
      )
    /* 4. There is no matching session and */
    | ( ( not (Ex matchingSession #i3 matchingRole matchingCom.
                  Sid ( matchingSession, < B, A, matchingCom, matchingRole, proto > ) @ i3 
                  & not ( matchingRole = role )
                  & ((Ex rest. matchingCom + rest = com) | (matchingCom = com))
                  & not (Ex #i4 sid. Sid ( matchingSession, sid) @ i4 & #i3 < #i4)))

           /* the adversary has revealed the longterm key of B. */
	   & (Ex #i5. RevealLtk (B) @ i5 & #i5 < #i1)
      )
    )
  )"

end