Formalizing Anonymity

• CSP renaming (Schneider and Sidiropoulos):

• process P strongly anonymous on a set of events A

  • fA-1 ( fA (P) ) = P
  • A is a set of events of form i.a,
  • for given action a, principal i performed a
  • fA (t) replaces events in A with a (impossible event).