Typed Spi-calculus with Key Compromise

Message tagging is a common technique for avoiding type confusion attacks [8,3] and is often treated explicitly in typed spi-calculi for authenticity [5,6,4], although some systems obtain message tagging as a derived form from "encryption" with public keys [7] and some type systems for secrecy omit message tagging and instead assume a fixed format for all messages encrypted by the same key [1,2]. Here we choose to include message tagging explicitly instead of obtaining it as a derived form, because that directly leads to intuitive typing rules.