[Avispa-users] i ve doubt

[Laurent Vigneron]

Dear Saleh,

This is a basic question, indeed, but this is always useful to recall 
such things.

The syntax for encryption is the same: {M}_K, whatever is the type of K 
(symmetric key, public key, private key).

However, when you specify transitions in a role, what you write has to 
reflect the semantics:
- if a message {M}_K is received, but the key for decryption is not 
known by the agent, you will have to write: RCV(X')
where X is of type {text}_symmetric_key or {text}_public_key or 
{text}_inv(public_key), depending on the type of K;
- if K is a symmetric key known by the agent, you will write: RCV({M'}_K)
(if M is learned by the agent; if it is already known, drop the ');
- if K is a public key, you will write: RCV({M'}_K)
if the agent know the corresponding private key;
- if K is a private key inv(L), you will write: RCV({M'}_inv(L))
if the agent know the corresponding public key L;
- last case: if the agent cannot decrypt the message, but can compose it 
(he knows M and K), you will write: RCV({M}_K)

Best regards,
Laurent.


SALEH AL-SHADLY a écrit :
> Dear all,
> 
> i really ve doubt about these things:
> 
> 1. encryption using symmetry key
> 2. encryption using public key
> 3. signature and certificates
> 
> is these are same implemented in AVISPA or there is a difference?
> 
> please give me some hints .
> 
> with many regards
> Saleh