@inproceedings{edelkamp02symbolic,
author = {Stefan Edelkamp},
booktitle = {International Conference on AI Planning and Scheduling International Conference on AI Planning and Scheduling (AIPS'02) Workshop on Model Checking},
title = {Symbolic exploration in two-player games: Preliminary results},
url = {http://citeseer.ist.psu.edu/edelkamp02symbolic.html},
year = {2002}
}
@inproceedings{narciso-playing04,
author = {Miguel Palomino and Narciso Mart{\'i}-Oliet and Alberto Verdejo},
booktitle = {5th International Workshop on Rule-Based Programming (RULE)},
title = {Playing with {Maude}},
url = {http://citeseer.ist.psu.edu/712738.html},
year = {2004}
}
@inproceedings{1016531,
author = {Ratul Mahajan and Maya Rodrig and David Wetherall and John Zahorjan},
booktitle = {PINS '04: Proceedings of the ACM SIGCOMM workshop on Practice and theory of incentives in networked systems},
doi = {http://doi.acm.org/10.1145/1016527.1016531},
isbn = {1-58113-942-9},
location = {Portland, Oregon, USA},
pages = {183--190},
publisher = {ACM Press},
title = {Experiences applying game theory to system design},
year = {2004}
}
@inproceedings{SheynerWing2004,
author = {Oleg Sheyner and Jeannette Wing},
title = {Tools for Generating and Analyzing Attack Graphs},
booktitle = {Proceedings of Formal Methods for Components and Objects},
pages = {344--371},
year = {2004},
optvolume = {},
optnumber = {},
pdf = {http://www.cs.cmu.edu/~wing/publications/SheynerWing04.pdf},
series = {Lecture Notes in Computer Science}
}
@article{LyeWing2005,
author = {Kong-wei Lye and Jeannette Wing},
title = {Game Strategies in Network Security},
journal = {International Journal of Information Security},
year = {2005},
volume = {4},
number = {1--2},
pages = {71--86},
month = {February},
issn = {1615-5262 (Paper), 1615-5270 (Online)},
doi = {http://dx.doi.org/10.1007/s10207-004-0060-x},
pdf = {http://www.cs.cmu.edu/~wing/publications/LyeWing05.pdf},
abstract = {This paper presents a game-theoretic method for analyzing the security of computer networks. We view the interactions between an attacker and the administrator as a two-player stochastic game and construct a model for the game. Using a nonlinear program, we compute Nash equilibria or best-response strategies for the players (attacker and administrator). We then explain why the strategies are realistic and how administrators can use these results to enhance the security of their network.}
}
@phdthesis{SheynerPhD2004,
author = {Oleg Sheyner},
title = {Scenario Graphs and Attack Graphs},
school = {Carnegie Mellon University},
year = {2004},
month = {April},
pdf = {http://www.milena.org/thesis/sg-ag.pdf},
abstract = {We develop formal techniques that give users flexibility in examining design errors discovered by automated analysis. We build our results using the model checking approach to verification. The two inputs to a model checker are a finite system model and a formal correctness property specifying acceptable behaviors. The correctness property induces a bipartition on the set of behaviors of the model: correct behaviors, which satisfy the property, and faulty behaviors, which violate the property. Traditional model checkers give users a single counterexample, chosen from the set of faulty behaviors. Giving the user access to the entire set, however, lets him have more control over the design refinement process. The focus of our work is on ways of generating, presenting, and analyzing faulty behavior sets. \par We present our results in two parts. In Part I we introduce concepts that let us define faulty behavior sets as ``failure scenario graphs.'' We then describe algorithms for generating scenario graphs. The algorithms use model checking techniques to produce sound and complete faulty behavior sets. \par In Part II we apply our formal concepts to the security domain. Building on the foundation established in Part I, we define and attack graphs, an application of scenario graphs to represent ways in which intruders attack computer networks. Attack graphs depict ways in which an adversary exploits system vulnerabilities to achieve a desired state. System administrators use attack graphs to determine how vulnerable their systems are and to determine what security measures to deploy to defend their systems. This application of formal analysis contributes to techniques and tools for strengthening network security. }
}
@inproceedings{Wing2005,
author = {Jeannette M.~Wing},
title = {Scenario Graphs Applied to Security},
booktitle = {Proceedings of Verification of Infinite State Systems with Applications to Security (VISSAS)},
optpages = {},
year = {2005},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
address = {Timisoara, Romania},
month = {March},
note = {Summary paper},
pdf = {http://www.cs.cmu.edu/~wing/publications/Wing05.pdf}
}
@inproceedings{380883,
author = {Christos Papadimitriou},
title = {Algorithms, games, and the internet},
booktitle = {Proceedings of the thirty-third annual ACM symposium on Theory of computing (STOC)},
year = {2001},
isbn = {1-58113-349-9},
pages = {749--753},
location = {Hersonissos, Greece},
doi = {http://doi.acm.org/10.1145/380752.380883},
publisher = {ACM Press},
address = {New York, NY, USA}
}
@article{nisan01a,
author = {Noam Nisan and Amir Ronen},
title = {Algorithmic Mechanism Design},
journal = {Games and Economic Behavior},
year = {2001},
volume = {35},
pages = {166--196},
abstract = {We consider algorithmic problems in a distributed setting where the participants cannot be assumed to follow the algorithm but rather their own self-interest. As such participants, termed agents, are capable of manipulating the algorithm, the algorithm designer should ensure in advance that the agents' interests are best served by behaving correctly. Following notions from the field of mechanism design, we suggest a framework for studying such algorithms. Our main technical contribution concerns the study of a representative task scheduling problem for which the standard mechanism design tools do not suffice.},
doi = {http://dx.doi.org/10.1006/game.1999.0790}
}
@article{feigenbaum01a,
author = {Joan Feigenbaum and Christos H. Papadimitriou and Scott Shenker},
title = {Sharing the Cost of Multicast Transmissions},
journal = {Journal of Computer and System Sciences},
year = {2001},
volume = {63},
number = {1},
pages = {21--41},
month = {August},
abstract = {We investigate cost-sharing algorithms for multicast transmission. Economic considerations point to two distinct mechanisms, marginal cost and Shapley value, as the two solutions most appropriate in this context. We prove that the former has a natural algorithm that uses only two messages per link of the multicast tree, while we give evidence that the latter requires a quadratic total number of messages. We also show that the welfare value achieved by an optimal multicast tree is NP-hard to approximate within any constant factor, even for bounded-degree networks. The lower-bound proof for the Shapley value uses a novel algebraic technique for bounding from below the number of messages exchanged in a distributed computation; this technique may prove useful in other contexts as well.},
doi = {http://dx.doi.org/10.1006/jcss.2001.1754}
}
This file was generated by bibtex2html 1.96.