Formal verification of the universal physical access control system (UPACS)

The Universal Access Control System (UPACS) is a communication protocol designed to provide secure access to remote physical devices over an untrusted communication network, where it could be subjected to eavesdropping, unauthorized modification of its messages, and other forms of tampering by attackers. We modeled the protocol in the typed Pi Calculus and used the formal protocol verification tool Proverif to examine the protocol's security properties. We issued Proverif queries to determine the ability of the protocol to protect the secrecy of terms used by protocol processes, mask any observable changes in the behavior of the protocol as the terms changed in value, and maintain the correct ordering of and causal relationships between events occurring within protocol sessions. We verified that the protocol satisfies all of its intended reachability, observational equivalence and correspondence properties.