theory Naxos
begin

builtins: diffie-hellman, symmetric-encryption


functions: h1/1
functions: h2/1

/* Protocol rules 

I -> R :   I, g^h1(ex, x)
R -> I :   g^h1(ey, y), nR
I -> R :   senc(nR, k)

where:
* x - long-term private key of I
* ex - ephemeral key generated by I (once per session)
* y - long-term private key of R
* ey - ephemeral key generated by R (once per session)
* k = ( g^(x* h1(ey, y)), g^(y* h1(ex, x)), g^(h1(ex, x)*h1(ey, y)) )

 */

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

/* Initiator */
rule Init_1:
  let hexI = h1(<~exI, ~xI >)
      hkI = 'g'^hexI
  in
   [   Fr( ~exI ), !Ltk( $I, ~xI ) ]
   -->
   [   Init_1( ~exI, $I, $R, ~xI, hkI )
     , Out( <$I, hkI> ) ]

rule Init_2:
  let
      hexI = h1(< ~exI, ~xI >)
      kI  = h2(< Y^~xI, pkR^hexI, Y^hexI, $I, $R >)
      c = senc(nR, kI)
  in
   [   Init_1( ~exI, $I, $R, ~xI , hkI), !Pk( $R, pkR ), In( <Y, nR>  ) ]
   --[ Accept( $I, $R, kI),  I_think($I, $R, <$I, $R, kI>), Finish_I( $I, $R, kI)
     ]->
   [  !Sessk( ~exI, kI), Out(c) ]



/* Responder */
rule Resp_1:
  let 
      hexR = h1(< ~exR, ~xR >)
      hkr = 'g'^hexR
      kR  = h2(< pkI^hexR, X^~xR, X^hexR, I, $R >) 
  in
   [   Fr(~nR), Fr( ~exR ), !Ltk($R, ~xR), !Pk(I, pkI), In( <I, X> ) ]
   --[  Accept($R, I, kR )
     ]->
   [   Resp_1( ~exR, I, $R, ~xR, hkr, ~nR, kR, X),
       Out( <hkr, ~nR> ) ]

rule Resp_2:
  let
   c = senc(nR, kR)
  in
   [   Resp_1( ~exR, I, $R, ~lkR, hkr, nR, kR, X),   In(c) ]
   --[ Accept_R($R, I, kR ), I_am_convinced(I, $R, <I, $R, kR>), Finish_R($R, I, kR )
     ]->
   [  !Sessk( ~exR, kR) ]

/* Key Reveals for the eCK model */

rule Ltk_reveal:
   [ !Ltk($A, lkA) ] --[ LtkRev($A) ]-> [ Out(lkA) ]


restriction OnlyOnce:
" 
  All x #i #j. OnlyOnce(x) @i & OnlyOnce(x) @j ==> #i = #j
"

// Executable lemma

lemma executable:
  exists-trace
  "Ex I R k #i #j. Finish_I(I, R, k) @ #i & Finish_R(R, I, k) @ #j & not (#i = #j) &  not(Ex  X #r. LtkRev(X) @ r) "


/* Security properties */

 /* 
   * If there exists a  session whose key k is known to the
   * Adversary, then the long term key of one of the two participants involved in that session was reveled
   */
   
lemma secrecy_claim:
  "All  A B v #i. Accept(A, B, v) @i ==>
       (not(Ex #j. K(v) @j) | (Ex  #r. LtkRev(A) @ r) | (Ex #r.  LtkRev(B)@r ) )
"
 /* 
   * If there exists a  session whose key k is known to the
   * Adversary, then the long term key of one of the two participants involved in that session was reveled before that session
   */

lemma PFS_secrecy_claim:
  "All   A B v #i. Accept(A, B, v) @i ==>
       (not(Ex #j. K(v) @j) | (Ex  #r. LtkRev(A) @ r & r<i) | (Ex #r.  LtkRev(B)@r & r<i) )
"
/* 
   * If there exists a  session where the receiver has accepted a key k, and k is known to the
   * Adversary, then the long term key of one of the two participants involved in that session was reveled before that session
   */

lemma PFS_secrecy_claim_R:
  "All A  B v #i. Accept_R(A, B, v) @i ==>
       (not(Ex #j. K(v) @j) | (Ex  #r. LtkRev(A) @ r & r<i) | (Ex #r.  LtkRev(B)@r & r<i) )
"



// Injective agreement from the perspective of both the initiator and the responder.
/*
lemma noninjective_agree:
  " /* Whenever somebody commits to running a session, then*/
    All actor peer params #i.
        Commit(actor, peer, params) @ i
      ==>
        /* there is somebody running a session with the same parameters */
          (Ex #j. Running(peer, actor, params) @ j
          )
        /* or the adversary perform a long-term key reveal on assumed honest participant */
        | (Ex X #r. Reveal(X) @ r & Honest(X) @i)
  "
*/

// Injective agreement from the perspective of the responder.
lemma injective_agree:
  " /* Whenever somebody commits to running a session, then*/
    All A B params #i.
        I_am_convinced(A, B, params) @ i
      ==>
        /* there is somebody running a session with the same parameters */
          (Ex #j. I_think(A, B, params) @ j & j < i
            /* and there is no other commit on the same parameters */
            & not(Ex C D #i2.
                    I_am_convinced(C, D, params) @ i2 & not(#i = #i2)
                 )
          )
        /* or the adversary perform a long-term key reveal on assumed honest participant */
        | (Ex  #r. LtkRev(A) @ r)  | (Ex  #r. LtkRev(A) @ r) 
  "



end