Formalizing and Analyzing Sender Invariance