tag:blogger.com,1999:blog-27705661.post1434812140551459434..comments2023-10-28T10:58:57.140+00:00Comments on Process Algebra Diary: Vardi on Process EquivalencesLuca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.comBlogger1125tag:blogger.com,1999:blog-27705661.post-22171349006184470892007-08-07T03:26:00.000+00:002007-08-07T03:26:00.000+00:00The principle of contextual equivalence makes a lo...The principle of contextual equivalence makes a lot of sense for security. (Security can often be defined as indistinguishability between instantiations of a parameterized process.) Bisimulation is indeed too fine an equivalence for security; often weaker notions of observational congruence are defined, such as for the applied pi calculus. <BR/><BR/>However deriving (denotational) semantics from equivalences seldom helps proofs. I find proofs easier in a setting that starts off with an operational semantics and then defines congruences. <BR/><BR/>I don't think bisimulation is a good technique for proving implementations correct (given a specification) in any case; a much better approach is proving full abstraction, i.e., preservation of observational congruence. However without bisimulation, proving full abstraction can be tedious. I usually show simulations both ways modulo "wrappers", and then show that the wrappers in the two directions "cancel out", thus doing 3 proofs for one. Is there a better technique for this setting?<BR/><BR/>The principle of observable I/O is also obvious. However I don't quite understand the principle of comprehensive modeling. To me it seems to push under the rug the very reasons for having so many equivalences.Anonymousnoreply@blogger.com