Welcome to the first issue of the eighth volume of the journal. In this issue, we publish six regular papers as well as a single page per paper incorporating the translation of the title and abstract in Persian, to be used by Persian indexing centers.Our invited authors in the first paper of this issue review two formal approaches in verification of security protocols; model checking and theorem proving. In this paper, Scyther operational semantics is explained as a model checking approach, and some of the famous security protocols are modelled and verified using this method. Moreover, the notion \Glass Pipe" is discussed to describe the meaning of authentication, and a deduction system is provided to formally define the notion. Finally, using this deduction system, some of famous protocols are verified, and the results are compared with the results of Scyther model checker...