Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)



Hi Denis,

Simon: I saw your presentation at FLOC and found the framework very
> interesting; however, for my protocol I had to modify Public.thy and
> Event.thy, so this might be a problem. What do you think?


Hmm, it depends on the changes. The question is, if you can model your
protocol as a set of linear roles and if you can evaluate your security
property over the state our security protocol model provides. If yes, then
our framework might be of quite some help to you. Otherwise, your problem
might be amenable (in the future) to the generalization of the protocol
model that I am working on.

In any case, I would be very interested in seeing the protocol you are
investigating in order to guide me where the put my resources. For example
in the form of your source files. If you'd have an informal description of
the protocol, then this would probably help me understand your sources.

best regards,
Simon




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.