theory KeyRenegotiation_Minimal begin

/*
   Protocol:    A minimal version of a key renegotiation protocol.
   Modeler:     Simon Meier
   Date:        May 2012

   Status:      working

   Minimal example of the verification of a protocol with repeated key
   re-negotiation.

*/

builtins: symmetric-encryption

rule Setup:
    [ Fr(~k) ]
  -->
    [ Sender(~k), Receiver(~k) ]

rule Send:
    [ Sender(k0), Fr(~k) ]
  --[ Secret(~k) ]->
    [ Sender(~k), Out( senc{~k}k0 ) ]


rule Receive:
    [ Receiver(k0), In(senc{k}k0) ]
  --[ Secret(k) ]->
    [ Receiver(k) ]

lemma Secret_reachable [use_induction]:
  exists-trace
  "Ex k #i. Secret(k) @ i"

// TODO: Investigate the form of the property and its proof when key
// compromise is allowed.
lemma secrecy [use_induction]:
  "All k #i #j. Secret(k) @ i & KU(k) @ j ==> F"

end