We investigate the composition of protocols that share a common secret. This situation
arises when users employ the same password on different services. More precisely we study
whether resistance against guessing attacks composes when the same password is used.
We model guessing attacks using a common definition based on static equivalence in a
cryptographic process calculus close to the applied pi calculus. We show that resistance
against guessing attacks composes in the presence of a passive attacker. However …

Formal and symbolic techniques are extremely useful for modelling and analysing security
protocols. They have helped to improve our understanding of such protocols, allowed us to
discover flaws, and they also provide support for protocol design. However, such analyses
usually consider that the protocol is executed in isolation or assume a bounded number of
protocol sessions. Hence, no security guarantee is provided when the protocol is executed
in a more complex environment. In this paper, we study whether password protocols can be …