[moca] Ambient logics and theorem proving

[devrimu@xxxxxxxxxxxxxxxxxxxx]

 Hello to all,

   I would like to use logics to reason about security properties of
models specified in ambient calculus.

   My intent is to analyse properties ambient-calculus based
specifications with respect to a security policy specified as a formal
language and its related theorems.

   For this purpose, I would like to utilise theorem proving and model
checking. If possible I would like to use Isabelle theorem prover for
this purpose. It supports the High Order Logic and the likes.

   I am aware of the modal ambient logics for ambient calculus. Can I use
this logics somehow in any automated theorem prover? If so, how?
Alternatively, can I map the High Order Logic to be used as a logic in
ambient calculus? Can I use another tool for model checking and theorem
proving for logical specifications in ambient calculus? Can I use
another logic that I can use for automated model checking/theorem
proving in ambient calculus?

   Any comments / information is deeply appreciated,

   Thank you in advance
   Devrim Ünal
   Researcher



  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html