Weakening the Dolev-Yao model through probability

peer-reviewedThe Dolev-Yao model has been widely used in protocol verificaion and has been implemented in many protocol verifiers. There are strong assumptions underlying this model, such as perfect cryptography: the aim of the present work is to propose an approach to weaken this hypothesis, by means of probabilistic considerations on the strength of crypto- graphic functions. Such an approach may effectively be implemented in actual protocol verifiers. The Yahalom proto- col is used as an easy example to show this approach