How can process algebra help to design security protocols? Would you please tell me how process algebra could help me to design security protocols? 

More specifically, can I use it for proving the security of protocols? 

Is process algebra used for any security protocol or specific types of protocol such as network protocols?
More specifically, can I use it for proving the security of protocols?


Sort-of.
Using process algebras you can model or describe your protocol using a language that has a formally defined syntax and semantic (= meaning) just like you can describe a protocol using code or text. The advantage of process algebras is that the formal syntax and semantics can be used by tools to do one of the following:


Find a counter-example to a claimed property.
Prove that the protocol satisfies a claimed property (not always possible).
Reduce the proof of the complete protocol to some more easily manually achieved proofs.