Using the framework presented in previous sections, we have specified the protocol in LOTOS. Abstract data types were designed for all the cryptographic operations involved including the abstract model of the GQ algorithm. The user and the TTP are two trusted principals and the intruder is the untrusted one. The user always tries to perform a valid registration. The intruder's initial knowledge is adjusted to allow him to act as a second untrusted user and simultaneously as a second untrusted TTP. It includes:
et 
and the public key of the TTP
After the step-by-step simulation stage, the labelled transition system (LTS) of the protocol has been generated. It is composed of 487446 states and 2944856 transitions and has required one hour of computation on a SUN Ultra-2 workstation running Solaris 2.5.1 with 2 CPUs and 832 Mb of RAM. The reduction factor of the minimization modulo the strong bisimulation was very important. The minimized LTS of the protocol is made of 3968 states and 37161 transitions. The reduction modulo the safety equivalence was not mandatory because the graph was small enough to carry out the verification.