New inter-realm authentication protocol and its formalization verification

In order to access resources in different areas on Internet in a security way, authentication is the first key step. Kerberos au- thentication protocol is widely used. But Kerberos protocol doesn't authenticate the client that requests the resources on Internet, so a new inter-realm authentication protocol and a generation schemes aboutnonceare presented. Then we used the Spi calculus to analyze the authentication protocol, and proved the security of protocol. The proposed scheme can solve the problem of security information transferring between networks.