[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Questions about pvs proofs


I am a Tunisian student .
My search  concerns the check property of cryptographic authentification protocols
( Iso Symmetric Key Tow-Pass Unilateral Autentification Protocol), by using
the tool PVS for the proof.
     (1)  B-->A : Rb,Text1
     (2)  A-->B : Text3,  { Rb,B,Text2}Kab

In fact there are some steps which are not clear for me. I really need your
help to understand some details.

-One of my questions is to know how to specify a key shared (Kab) between 2
agents (A and B), knowing that in the tool PVS I found only shr ( A ) that is
the shared key between server and A. 
- My second questions is to know  what’s the  TYPE     of  Text1,Text2, Text3.

-I want also to know if you have examples of protocols proofs (with PVS where
it use a key shared between 2 agents) who can help me in my searches.

Many thanks.