کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951423 | 1441450 | 2017 | 90 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Stateful applied pi calculus: Observational equivalence and labelled bisimilarity
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
We extend Abadi-Fournet's applied pi calculus with state cells, which are used to reason about protocols that store persistent information. Examples are protocols involving databases or hardware modules with internal state. We distinguish between private state cells, which are not available to the attacker, and public state cells, which arise when a private state cell is compromised by the attacker. For processes involving only private state cells we define observational equivalence and labelled bisimilarity in the same way as in the original applied pi calculus, and show that they coincide. Our result implies Abadi-Fournet's theorem - the coincidence of observational equivalence and labelled bisimilarity - in a revised version of the applied pi calculus. For processes involving public state cells, we can essentially keep the definition of observational equivalence, but need to strengthen the definition of labelled bisimulation in order to show that observational equivalence and labelled bisimilarity coincide in this case as well.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 89, June 2017, Pages 95-149
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 89, June 2017, Pages 95-149
نویسندگان
Myrto Arapinis, Jia Liu, Eike Ritter, Mark Ryan,