We present a formal analysis technique for probabilistic security properties of peer-to-peer communication systems based on random message routing among members. The behavior of g...
We extend definitions of information flow so as to quantify the amount of information passed; in other words, we give a formal definition of the capacity of covert channels. Ou...
Privacy is an increasing concern in the marketplace. Although enterprises promise sound privacy practices to their customers, there is no technical mechanism to enforce them inter...
The strand spaces model and the rank functions model have both been used successfully to analyse and verify security protocols running on unbounded networks. At first sight, thes...
We describe a protocol design process, and illustrate its use by creating ATSPECT, an Authentication Test-based Secure Protocol for Electronic Commerce Transactions. The design pr...
We formalize aspects of the Kerberos 5 authentication protocol in the Multi-Set Rewriting formalism (MSR) on two levels of detail. The more detailed formalization reflects the in...
Frederick Butler, Iliano Cervesato, Aaron D. Jagga...
We present the first type and effect system for proving authenticity properties of security protocols based on asymmetric cryptography. The most significant new features of our ...
We carry forward the work described in our previous papers [3, 14, 12] on the application of data independence to the model checking of cryptographic protocols using CSP [13] and ...