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

[PVS-Help] Type problem.


I am trying especify operations in a cryptografy protocol. However, all the operations are defined by a operator and a user, except by the operation called "delName".

e. g.

% The user can:

cryptStampType : TYPE = {decrypt, % decrypt using his private key;
                     encrypt, % encrypt using any public key;
         appendName, % append his name into mensage;
                     nameMatch, % verify and delete who is the sender;
                     delName}      % delete name without verify who.

 opStamp : TYPE = [# opStampTyp : cryptStampType , % a user's action in protocol;
                               user   : U  #]     % by any other user.

I would like that the "delName" be an element of opStamp, but without a user.

Could you help me, please?

Thiago Mendonca Ferreira Ramos
undergraduated in Computer Science
University of Brasilia
Brasilia, Brasil