A new method of formalizing anonymity based on protocol composition logic
Tao Feng, Shining Han, Guo Xian, Donglin Ma · Security and Communication Networks · 2014
Abstract In order to make protocol composition logic (PCL) model satisfy the special needs of anonymous analysis, based on observational equivalence theory, this paper extended PCL to be anonymity PCL (APCL). In anonymity PCL, equivalent messages and equivalent traces were proposed. On the basis of equivalent traces, three kinds of anonymity were defined: sender anonymity, recipient anonymity, and relation anonymity. Finally, taking direct anonymous attestation (DAA) as an example, we formalized the anonymity of DAA by the new framework, the result of which demonstrates that DAA satisfies anonymity and verifies the correctness and feasibility of the new framework. Copyright © 2014 John Wiley & Sons, Ltd.