งานวิจัยชิ้นนี้มีวัตถุประสงค์ในการพัฒนาวิธีการแบบนัยนิยมที่สามารถนำมาใช้วิเคราะห์ระบบการรักษาความปลอดภัยของข้อมูลสารสนเทศในผลิตภัณฑ์ที่ใช้งานจริง โดยเฉพาะอย่างยิ่งผู้วิจัยได้พัฒนาวิธีการแบบนัยนิยมสำหรับการควบคุมการเข้าถึงข้อมูลสารสนเทศในระบบปฏิบัติการ ระบบไฟร์วอลล์ และโพรโตคอลสำหรับการชำระเงินอีเล็กโทรนิกส์ซึ่งใช้ในระบบพาณิชย์อีเล็กโทรนิกส์ ซึ่งวิธีการแบบนัยนิยมที่พัฒนาขึ้นประกอบด้วย แบบจำลองซึ่งสามารถอธิบายการทำงานของระบบดังกล่าวได้ชัดเจนไม่คลุมเคลือ และการพิสูจน์ตรวจสอบความปลอดภัยในผลิตภัณฑ์ดังกล่าว ซอฟท์แวร์ต้นแบบได้ถูกพัฒนาขึ้นและได้ถูกนำไปใช้งานในกรณีศึกษา ซึ่งจากการทำการทดสอบในกรณีศึกษาพบว่า วิธีการแบบนัยนิยมที่ได้ถูกพัฒนาขึ้นสามารถอธิบายการทำงานของระบบการรักษาความปลอดภัยของข้อมูลได้ชัดเจน ไม่คลุมเครือ ส่งผลให้นำมาสู่ความเข้าใจในการทำงานของระบบและการใช้งานของระบบที่ดีขึ้น นอกจากนี้การที่ได้ถูกพัฒนาขึ้นสามารถนำมาใช้ในการวิเคราะห์การใช้งานของระบบโดยเน้นประโยชน์ใช้สอย โดยเฉพาะอย่างยิ่งการวิเคราะห์ความถูกต้องและความปลอดภัยขั้นพื้นฐานของการใช้งานของระบบได้ดี สำหรับงานวิจัยในอนาคต ผู้วิจัยคาดว่าจะทำการศึกษาวิธีการวิเคราะห์การบุกรุกในระบบอินเตอร์เน็ตและวิธีการในการวิเคราะห์และช่วยสร้างโพรโตคอลที่มีความปลอดภัยสำหรับรัฐบาลอีเล็กโทรนิกส์ This research aims to develop a formal methodology for analyzing the security of information security systems which are currently in use nowadays. In particular, we have developed formal methodology for access control in operating systems, network firewalls and electronic payment protocols. The formal methodology developed consists of formal specification which describes system behavior unambiguously and formal verification that can analyze the security of those systems. A software prototype is developed and is applied to case studies. Experimental results obtained from the case studies show that our methodology can explain system behavior precisely and unambiguously. This provides a better understanding on how the systems work and how to use them correctly. Furthermore, our verification method offers practical analysis on the correctness and the security of the systems. In particular , important properties and attacks can be analyzed . As a future work, we aim to develop further our method for analyzing attacks in internet and crytographic protocols for electronic government systems.