The correctness of security protocols has become more and more important lately, as the aspects of real life being in control of computer systems increased. As operations like money transfers or military communications are being ported to computer networks, any flaw in security of the systems can lead to extremely large amount of loss. The discovery of flaws in protocols that were considered safe shows that the formal verification of such protocols is essential. My talk first addresses different aspects of security and gives a brief introduction to cryptography techniques. Then, I shall present a well-known security protocol (CCITT X.509), describe a logic designed to analyse authentication, and show how we can verify the protocol by means of Model Checking. The model of the protocol will be presented in the "Rebeca" modeling language. I will also describe how we can model an intruder for the protocol and a flaw in the protocol, which can be found by the Model Checking.