Andrew M. Mironov
This paper presents a new, significantly simpler proof of one of the main results of applied pi-calculus: the theorem that the concepts of observational and labeled equivalence of extended processes in applied pi-calculus coincide.
Andrew M. Mironov
Cryptographic Protocols (CP) are distributed algorithms intended for secure communication in an insecure environment. They are used, for example, in electronic payments, electronic voting procedures, systems of confidential data processing, etc. Errors in CPs can bring to great financial and social damage, therefore it is necessary to use mathematical methods to substantiate the correctness and safety of CPs. In this paper, a distributed process model of CPs is presented, which allows one to formally describe CPs and their properties. It is shown how to solve the problems of verification of CPs on the base of this model.
Andrew M. Mironov
In the paper we introduce a process model of security protocols, where processes are graphs with edges labelled by actions, and present a new method of specification and verification of security protocols based on this model.