theory ALIVEvsWEAKAGREE
begin

builtins: asymmetric-encryption

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

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


/* We formalize the following protocol
  protocol {
    1. A -> B: A,{na}pk(B)
    2. A <- B: na
  }
*/

rule Init_A:
  [ Fr(~id)
  , !Ltk(R, ltkR)
  ]
--[ Create_A($I, ~id) ]->
  [ St_A_1($I, ~id, pk(ltkR), R)
  ]

rule Init_B:
  [ Fr(~id)
  , !Ltk(R, ltkR)
  ]
--[ Create_B(R, ~id) ]->
  [ St_B_1(R, ~id, ltkR)
  ]

/*   1. A -> B: A,{na}pk(B)   */
    
rule A_1_send:
  [ St_A_1(I, ~id, pkltkR, R) 
  , Fr(~ni)
  ]
--[ Send(I, <I, aenc{~ni}pkltkR>) 
  , Running(I, R) // this may not be necessary
  , OUT_I_1(aenc{~ni}pkltkR)
  ]->
  [ St_A_2(I, ~id, pkltkR, R, ~ni) 
  , Out(<I, aenc{~ni}pkltkR>)
  ]

rule B_1_receive:
  [ St_B_1(R, ~id, ltkR)
  , In(<I, aenc{ni}pk(ltkR)>)
  ]
--[ Recv(R, <I, aenc{ni}pk(ltkR)>) 
//  , Honest(R), Honest(I)
  , IN_R_1_ni(ni, aenc{ni}pk(ltkR))
  ]->
  [ St_B_2(R, ~id, ltkR, I, ni)
  ]

/* 2. A <- B: na */
rule B_2_send:
  [ St_B_2(R, ~id, ltkR, I, ni)
  ]
--[ Send(R, ni)
  , Running(R, I)
  ]->
  [ St_B_3(R, ~id, ltkR, I, ni)
  , Out(ni)
  ]

rule A_2_receive:
  [ St_A_2(I, ~id, pkltkR, R, ~ni) 
  , In(~ni)
  ]
--[ Recv(I, ~ni)
  , Commit(I, R), Honest(R), Honest(I)
  , Finish()
  ]->
  [ St_A_3(I, ~id, pkltkR, R, ~ni) 
  ]


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)
       )
    )"

//protocol is executable
lemma executable:
  exists-trace
    "Ex #i. Finish() @i & not (Ex X #j. Reveal(X) @j) "

// succeeds
lemma aliveness:
  all-traces
    "All A B #i. Commit(A,B) @ i
      ==> (Ex #j id. Create_B(B,id) @j) | (Ex #j id. Create_A(B,id)@j)
          | (Ex X #r. Reveal(X) @ r & Honest(X) @i)"

// fails as expected
lemma weakagree:
  all-traces
   "All A B #i. Commit(A,B) @i
     ==> (Ex #j. Running(B,A) @j)
         | (Ex X #r. Reveal(X) @ r & Honest(X) @i)"

end