انجمن کامپیوتر ایران

پروتکل‌های رای‌گیری گام‌هایی را مشخص می‌کنند که افراد با پیمودن آن می‌توانند در رای‌گیری شرکت کرده و رای خود را به ثبت برسانند و در عین حال از صحت انتخابات نیز مطمئن باشند. بنابراین این پروتکل‌ها بایستی خواسته‌های امنیتی خاصی را برآورده کنند. در این مقاله سعی داریم با مدلسازی پروتکل F.O.O با ابزارهای صوری، برخی از ویژگی‌های امنیتی آن را تحلیل کنیم. همچنین نشان می‌دهیم که برخلاف ادعای [2] این پروتکل در محیط‌هایی با مقیاس وسیع تنها در شرایط ایده‌آل (و در برخی موارد نزدیک به ایده‌آل) قابل استفاده است، اما در حالت کلی برای محیطی که مقیاس وسیعی را دربرمی‌گیرد، قابل استفاده نخواهد بود.