In this chapter, we describe observational equivalence properties, and the workflows used to model and analyze them. Until now, all properties considered in this book were trace properties, meaning they are evaluated over individual traces. In contrast, observational equivalence describes a hyperproperty that compares two traces. We often call the workflow for reasoning about observational equivalence the diff mode of tamarin as this analysis is enabled using the flag --diff. Support for reasoning about observational equivalence was added to tamarin in 2015 [15]. As a result, tamarin can now be used to analyze privacy-style properties formalized as observational equivalence, such as anonymity or unlinkability. This has numerous applications, such as reasoning about voter privacy (sketched in this section) or reasoning about how persons can be tracked as they roam about with devices such as RFID tokens or mobile phones. For example, reasoning about observational equivalence in tamarin was used to show that the current generation of mobile communication, the 5G standard, has a weakness whereby users’ cellphones can be tracked [14]. tamarin found an attack whereby an active adversary can perform “presence tests” to track phones as they move over time.