This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Security Modeling and Analysis
May/June 2011 (vol. 9 no. 3)
pp. 18-25
ASCII Text
x 
 
Jason Bau, John C. Mitchell, "Security Modeling and Analysis," IEEE Security & Privacy, vol. 9, no. 3, pp. 18-25, May/June, 2011.
 
 
BibTex
x
 
@article{ 10.1109/MSP.2011.2,
author = {Jason Bau and John C. Mitchell},
title = {Security Modeling and Analysis},
journal ={IEEE Security & Privacy},
volume = {9},
number = {3},
issn = {1540-7993},
year = {2011},
pages = {18-25},
doi = {http://doi.ieeecomputersociety.org/10.1109/MSP.2011.2},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - MGZN
JO - IEEE Security & Privacy
TI - Security Modeling and Analysis
IS - 3
SN - 1540-7993
SP18
EP25
EPD - 18-25
A1 - Jason Bau,
A1 - John C. Mitchell,
PY - 2011
KW - Security modeling
KW - formal methods
KW - model checking
KW - security analysis
VL - 9
JA - IEEE Security & Privacy
ER -
 
Jason Bau, Stanford University
John C. Mitchell, Stanford University
Security modeling centers on identifying system behavior, including any security defenses; the system adversary's power; and the properties that constitute system security. Once a security model is clearly defined, security analysis evaluates whether the adversary, interacting with the system, can defeat the desired security properties. Although the authors illustrate security analysis using model checking, analysts can use various methods and tools to evaluate system security, including manual and automated theorem-proving tools that provide assurance about the absence of attacks in a specified threat model. This article describes a uniform approach for evaluating system security and illustrates the approach by summarizing three case studies. Security modeling and analysis also provides a basis for comparative evaluation and some forms of security metrics.

1. D. Lie et al., "Specifying and Verifying Hardware for Tamper-Resistant Software," Proc. 2003 IEEE Symp. Security and Privacy, IEEE CS Press, 2003, pp. 166–177.
2. G. Klein et al., "seL4: Formal Verification of an OS Kernel," Proc. ACM SIGOPS 22nd Symp. Operating Systems Principles, ACM Press, 2009, pp. 207–220.
3. W. Shin et al., "Towards Formal Analysis of the Permission-Based Security Model for Android," Proc. 5th Int'l Conf. Wireless and Mobile Comm., IEEE CS Press, 2009, pp. 87–92.
4. D. Akhawe et al., "Towards a Formal Foundation of Web Security," Proc. 23rd IEEE Computer Security Foundations Symp., IEEE CS Press, 2010, pp. 290–304.
5. C. Flanagan and S. Qadeer, "Predicate Abstraction for Software Verification," Proc. 29th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL 02), ACM Press, 2002, pp. 191–202.
6. L.C. Paulson, "The Inductive Approach to Verifying Cryptographic Protocols," J. Computer Security, vol. 6, vol. 1–2, 1998, p. 85128.
7. M. Arnaud, V. Cortier, and S. Delaune, "Modeling and Verifying Ad Hoc Routing Protocols," Proc. 23rd IEEE Computer Security Foundations Symp., IEEE CS Press, 2010, pp. 59–74.
8. M. Bruso, K. Chatzikokolakis, and J. den Hartog, "Formal Verification of Privacy for RFID Systems," Proc. 23rd IEEE Computer Security Foundations Symp., IEEE CS Press, 2010, pp. 75–88.
9. R.M. Needham and M.D. Schroeder, "Using Encryption for Authentication in Large Networks of Computers," Comm. ACM, vol. 21, no. 12, 1978, pp. 993–999.
10. G. Lowe, "Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR," Proc. 2nd Int'l Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACA 96), Springer-Verlag, 1996, pp. 147–166.
11. D.L. Dill, "The Murphi Verification System," Proc. 8th Int'l Conf. Computer Aided Verification (CAV 96), Springer-Verlag, 1996, pp. 390–393.
12. J. Mitchell, M. Mitchell, and U. Stern, "Automated Analysis of Cryptographic Protocols Using Murphi," Proc. 1997 IEEE Symp. Security and Privacy, IEEE CS Press, 1997, pp. 141–151.
13. J. Yang et al., "Using Model Checking to Find Serious File System Errors," ACM Trans. Computer Systems, vol. 24, no. 4, 2006, pp. 393–423.
14. A. Barth, C. Jackson, and J.C. Mitchell, "Robust Defenses for Cross-Site Request Forgery," Proc. 15th ACM Conf. Computer and Comm. Security (CCS 08), ACM Press, 2008, pp. 75–88.
15. A. Barth, "The Web Origin Concept,"26 Nov. 2010; http://tools.ietf.org/htmldraft-abarth-origin .

Index Terms:
Security modeling, formal methods, model checking, security analysis
Citation:
Jason Bau, John C. Mitchell, "Security Modeling and Analysis," IEEE Security & Privacy, vol. 9, no. 3, pp. 18-25, May-June 2011, doi:10.1109/MSP.2011.2
Usage of this product signifies your acceptance of the Terms of Use.