theory InjvsNoninjAgreement
begin

builtins: signing

// Public key infrastructure
rule Register_pk:
  [ Fr(~ltkA) ]
  -->
  [ !Ltk($A, ~ltkA),  Out(pk(~ltkA)) ] 

rule Reveal_ltk:
  [ !Ltk(A, ltkA) ] --[ Reveal(A) ]-> [ Out(ltkA) ]

/* We formalize the following protocol
  protocol {
    1. A -> B: {A,B}sk(A)
  }
*/

rule Init_A:
  [ Fr(~id)
  , !Ltk(I, ltkI)
  ]
--[ Create_A(I, ~id) ]->
  [ St_A_1(I, ~id, ltkI)
  ]

rule Init_B:
  [ Fr(~id)
  , !Ltk(I, ltkI)
  ]
--[ Create_B($R, ~id) ]->
  [ St_B_1($R, ~id, pk(ltkI), I)
  ]

rule A_1_send:
  let mA1 = sign{I, $R}ltkI
  in
  [ St_A_1(I, ~id, ltkI) 
  ]
--[ Send(I, mA1) 
  , Running(I, $R, mA1)
//  , OUT_I_1(mA1)
  ]->
  [ St_A_2(I, ~id, ltkI, $R) 
  , Out(mA1)
  ]

rule B_1_receive:
  let mB1 = sign{I,R}ltkI
  in
  [ St_B_1(R, ~id, pk(ltkI), I)
  , In(mB1)
  ]
--[ Recv(R, mB1) 
  , Finish()
  , Commit(R, I, mB1), Honest(R), Honest(I)
//  , IN_R_1_ni( ni, mB1 )
  ]->
  [ St_B_2(R, ~id, pk(ltkI), I)
  ]


/*
lemma types [typing]:
  " (All ni m1 #i.
       IN_R_1_ni( ni, m1) @ i
       ==>
       ( (Ex #j. KU(ni) @ j & j < i)
       | (Ex #j. OUT_I_1( m1 ) @ j)
       )
    )
  & (All nr m2 #i.
       IN_I_2_nr( nr, m2) @ i
       ==>
       ( (Ex #j. KU(nr) @ j & j < i)
       | (Ex #j. OUT_R_1( m2 ) @ j)
       )
    )
  "
*/

lemma executable:
  exists-trace
    "Ex #i. Finish() @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 both the initiator and the responder.
lemma injective_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 & j < i
            /* and there is no other commit on the same parameters */
            & not(Ex actor2 peer2 #i2.
                    Commit(actor2, peer2, params) @ i2 & not(#i = #i2)
                 )
          )
        /* or the adversary perform a long-term key reveal on assumed honest participant */
        | (Ex X #r. Reveal(X) @ r & Honest(X) @i)
  "



end