![]() |
This protocol involves two agents A and B. Message
Message
2 : B -> A : {NA,NB}pkAMessage
3 : A -> B : {NB}pkBThese lines describe a correct execution of one session of the protocol. Each line of the protocol corresponds to the emission of a message by an agent (A for the first line) and a reception of this message by another agent (B for the first line).
In line 1, the agent A is the initiator of the session. Agent B is the responder. Agent A sends B her identity and a freshly generated nonce
NA, both encrypted using the public key of B, pkB. Agent B receives the message, decrypts it using his secret key to obtain the identity of the initiator and the nonce NA.In line 2, B sends back to A a message containing the nonce
NA that B just received and a freshly generated nonce NB. Both are encrypted using the public key of A, pkA. The initiator A receives the message and decrypts it, A verifies that the first nonce corresponds to the nonce she sent B in line 1 and obtains nonce NB.In line 3, A sends B the nonce
NB she just received encrypted with the public key of B. B receives the message and decrypts it. Then B checks that the received nonce corresponds to NB.This protocol is declared in SeVe language as:
#Variables
Agents:
a,b;
Nonces: na,nb;
Public_keys: {ka,a},{kb,b};
#Initial
a knows
{na,ka};
b knows {nb,kb};
#Protocol_description
a
-> b : {a,na}kb;
b -> a :
{na,nb}ka;
a -> b :
{nb}kb;
#System
Initiator:
Alice;
Responder: Bob;
#Intruder
Intruder:
Intruder;
//Intruder_knowledge: {};
#Verification
Data_secrecy: {na} of Alice;
Agent_authentication: {Alice is_authenticated_with Bob using
{a}};