<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
        {font-family:Cambria;
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
h1
        {mso-style-priority:9;
        mso-style-link:"Heading 1 Char";
        margin-top:24.0pt;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
h1.CxSpFirst
        {mso-style-priority:9;
        mso-style-link:"Heading 1 Char";
        mso-style-type:export-only;
        margin-top:24.0pt;
        margin-right:0in;
        margin-bottom:0in;
        margin-left:0in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
h1.CxSpMiddle
        {mso-style-priority:9;
        mso-style-link:"Heading 1 Char";
        mso-style-type:export-only;
        margin:0in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
h1.CxSpLast
        {mso-style-priority:9;
        mso-style-link:"Heading 1 Char";
        mso-style-type:export-only;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
h2
        {mso-style-priority:9;
        mso-style-link:"Heading 2 Char";
        margin-top:10.0pt;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:13.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
h3
        {mso-style-priority:9;
        mso-style-link:"Heading 3 Char";
        margin-top:10.0pt;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        line-height:110%;
        font-size:12.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
h4
        {mso-style-priority:9;
        mso-style-link:"Heading 4 Char";
        margin-top:10.0pt;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;
        font-style:italic;}
h5
        {mso-style-priority:9;
        mso-style-link:"Heading 5 Char";
        margin-top:10.0pt;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Cambria","serif";
        color:#7F7F7F;
        font-weight:bold;}
h6
        {mso-style-priority:9;
        mso-style-link:"Heading 6 Char";
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        line-height:110%;
        font-size:12.0pt;
        font-family:"Cambria","serif";
        color:#7F7F7F;
        font-weight:bold;
        font-style:italic;}
p.MsoHeading7, li.MsoHeading7, div.MsoHeading7
        {mso-style-priority:9;
        mso-style-link:"Heading 7 Char";
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Cambria","serif";
        font-style:italic;}
p.MsoHeading8, li.MsoHeading8, div.MsoHeading8
        {mso-style-priority:9;
        mso-style-link:"Heading 8 Char";
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:10.0pt;
        font-family:"Cambria","serif";}
p.MsoHeading9, li.MsoHeading9, div.MsoHeading9
        {mso-style-priority:9;
        mso-style-link:"Heading 9 Char";
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:10.0pt;
        font-family:"Cambria","serif";
        letter-spacing:.25pt;
        font-style:italic;}
p.MsoTitle, li.MsoTitle, div.MsoTitle
        {mso-style-priority:10;
        mso-style-link:"Title Char";
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        mso-add-space:auto;
        font-size:26.0pt;
        font-family:"Cambria","serif";
        letter-spacing:.25pt;}
p.MsoTitleCxSpFirst, li.MsoTitleCxSpFirst, div.MsoTitleCxSpFirst
        {mso-style-priority:10;
        mso-style-link:"Title Char";
        mso-style-type:export-only;
        margin:0in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:26.0pt;
        font-family:"Cambria","serif";
        letter-spacing:.25pt;}
p.MsoTitleCxSpMiddle, li.MsoTitleCxSpMiddle, div.MsoTitleCxSpMiddle
        {mso-style-priority:10;
        mso-style-link:"Title Char";
        mso-style-type:export-only;
        margin:0in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:26.0pt;
        font-family:"Cambria","serif";
        letter-spacing:.25pt;}
p.MsoTitleCxSpLast, li.MsoTitleCxSpLast, div.MsoTitleCxSpLast
        {mso-style-priority:10;
        mso-style-link:"Title Char";
        mso-style-type:export-only;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        mso-add-space:auto;
        font-size:26.0pt;
        font-family:"Cambria","serif";
        letter-spacing:.25pt;}
p.MsoSubtitle, li.MsoSubtitle, div.MsoSubtitle
        {mso-style-priority:11;
        mso-style-link:"Subtitle Char";
        margin-top:0in;
        margin-right:0in;
        margin-bottom:30.0pt;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Cambria","serif";
        letter-spacing:.65pt;
        font-style:italic;}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
em
        {mso-style-priority:20;
        letter-spacing:.5pt;
        border:none windowtext 1.0pt;
        padding:0in;
        font-weight:bold;}
p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
        {mso-style-priority:99;
        mso-style-link:"Plain Text Char";
        margin:0in;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Courier New";}
p
        {mso-style-priority:99;
        mso-margin-top-alt:auto;
        margin-right:0in;
        mso-margin-bottom-alt:auto;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
p.MsoNoSpacing, li.MsoNoSpacing, div.MsoNoSpacing
        {mso-style-priority:1;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
        {mso-style-priority:34;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:.5in;
        mso-add-space:auto;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
p.MsoListParagraphCxSpFirst, li.MsoListParagraphCxSpFirst, div.MsoListParagraphCxSpFirst
        {mso-style-priority:34;
        mso-style-type:export-only;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:0in;
        margin-left:.5in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
p.MsoListParagraphCxSpMiddle, li.MsoListParagraphCxSpMiddle, div.MsoListParagraphCxSpMiddle
        {mso-style-priority:34;
        mso-style-type:export-only;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:0in;
        margin-left:.5in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
p.MsoListParagraphCxSpLast, li.MsoListParagraphCxSpLast, div.MsoListParagraphCxSpLast
        {mso-style-priority:34;
        mso-style-type:export-only;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:.5in;
        mso-add-space:auto;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
p.MsoQuote, li.MsoQuote, div.MsoQuote
        {mso-style-priority:29;
        mso-style-link:"Quote Char";
        margin-top:10.0pt;
        margin-right:.25in;
        margin-bottom:4.0pt;
        margin-left:.25in;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";
        font-style:italic;}
p.MsoIntenseQuote, li.MsoIntenseQuote, div.MsoIntenseQuote
        {mso-style-priority:30;
        mso-style-link:"Intense Quote Char";
        margin-top:10.0pt;
        margin-right:.8in;
        margin-bottom:14.0pt;
        margin-left:.7in;
        text-align:justify;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";
        font-weight:bold;
        font-style:italic;}
span.MsoSubtleEmphasis
        {mso-style-priority:19;
        font-style:italic;}
span.MsoIntenseEmphasis
        {mso-style-priority:21;
        font-weight:bold;}
span.MsoSubtleReference
        {mso-style-priority:31;
        font-variant:small-caps;}
span.MsoIntenseReference
        {mso-style-priority:32;
        font-variant:small-caps;
        letter-spacing:.25pt;
        text-decoration:underline;}
span.MsoBookTitle
        {mso-style-priority:33;
        font-variant:small-caps;
        letter-spacing:.25pt;
        font-style:italic;}
p.MsoTocHeading, li.MsoTocHeading, div.MsoTocHeading
        {mso-style-priority:39;
        margin-top:24.0pt;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
p.MsoTocHeadingCxSpFirst, li.MsoTocHeadingCxSpFirst, div.MsoTocHeadingCxSpFirst
        {mso-style-priority:39;
        mso-style-type:export-only;
        margin-top:24.0pt;
        margin-right:0in;
        margin-bottom:0in;
        margin-left:0in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
p.MsoTocHeadingCxSpMiddle, li.MsoTocHeadingCxSpMiddle, div.MsoTocHeadingCxSpMiddle
        {mso-style-priority:39;
        mso-style-type:export-only;
        margin:0in;
        margin-bottom:.0001pt;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
p.MsoTocHeadingCxSpLast, li.MsoTocHeadingCxSpLast, div.MsoTocHeadingCxSpLast
        {mso-style-priority:39;
        mso-style-type:export-only;
        margin-top:0in;
        margin-right:0in;
        margin-bottom:4.0pt;
        margin-left:0in;
        mso-add-space:auto;
        font-size:14.0pt;
        font-family:"Cambria","serif";
        font-weight:bold;}
span.Heading1Char
        {mso-style-name:"Heading 1 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 1";
        font-family:"Cambria","serif";
        font-weight:bold;}
span.Heading2Char
        {mso-style-name:"Heading 2 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 2";
        font-family:"Cambria","serif";
        font-weight:bold;}
span.Heading3Char
        {mso-style-name:"Heading 3 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 3";
        font-family:"Cambria","serif";
        font-weight:bold;}
span.Heading4Char
        {mso-style-name:"Heading 4 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 4";
        font-family:"Cambria","serif";
        font-weight:bold;
        font-style:italic;}
span.Heading5Char
        {mso-style-name:"Heading 5 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 5";
        font-family:"Cambria","serif";
        color:#7F7F7F;
        font-weight:bold;}
span.Heading6Char
        {mso-style-name:"Heading 6 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 6";
        font-family:"Cambria","serif";
        color:#7F7F7F;
        font-weight:bold;
        font-style:italic;}
span.Heading7Char
        {mso-style-name:"Heading 7 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 7";
        font-family:"Cambria","serif";
        font-style:italic;}
span.Heading8Char
        {mso-style-name:"Heading 8 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 8";
        font-family:"Cambria","serif";}
span.Heading9Char
        {mso-style-name:"Heading 9 Char";
        mso-style-priority:9;
        mso-style-link:"Heading 9";
        font-family:"Cambria","serif";
        letter-spacing:.25pt;
        font-style:italic;}
span.TitleChar
        {mso-style-name:"Title Char";
        mso-style-priority:10;
        mso-style-link:Title;
        font-family:"Cambria","serif";
        letter-spacing:.25pt;}
span.SubtitleChar
        {mso-style-name:"Subtitle Char";
        mso-style-priority:11;
        mso-style-link:Subtitle;
        font-family:"Cambria","serif";
        letter-spacing:.65pt;
        font-style:italic;}
span.QuoteChar
        {mso-style-name:"Quote Char";
        mso-style-priority:29;
        mso-style-link:Quote;
        font-style:italic;}
span.IntenseQuoteChar
        {mso-style-name:"Intense Quote Char";
        mso-style-priority:30;
        mso-style-link:"Intense Quote";
        font-weight:bold;
        font-style:italic;}
span.PlainTextChar
        {mso-style-name:"Plain Text Char";
        mso-style-priority:99;
        mso-style-link:"Plain Text";
        font-family:"Courier New";}
span.EmailStyle47
        {mso-style-type:personal-compose;
        font-family:"Times New Roman","serif";}
.MsoChpDefault
        {mso-style-type:export-only;
        font-size:10.0pt;}
@page WordSection1
        {size:8.5in 11.0in;
        margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
        {page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="blue" vlink="purple">
<div class="WordSection1">
<table class="MsoNormalTable" border="0" cellpadding="0" width="600" style="width:6.25in">
<tbody>
<tr>
<td style="padding:.75pt .75pt .75pt .75pt">
<div style="margin-bottom:4.0pt">
<table class="MsoNormalTable" border="0" cellpadding="0" width="600" style="width:6.25in">
<tbody>
<tr>
<td style="padding:.75pt .75pt .75pt .75pt">
<div style="margin-bottom:4.0pt">
<div class="MsoNormal" align="center" style="margin-bottom:0in;margin-bottom:.0001pt;text-align:center">
<hr size="2" width="100%" align="center">
</div>
</div>
<p align="center" style="margin-bottom:12.0pt;text-align:center"><b><span style="font-size:10.0pt;font-variant:small-caps">Computer Science Department / College of Arts and Sciences<o:p></o:p></span></b></p>
<p align="center" style="margin-bottom:12.0pt;text-align:center"><b><span style="font-size:10.0pt;font-variant:small-caps">PhD Oral Area Exam of Rick Skowyra</span></b><span style="font-size:11.0pt"><br>
<br>
Monday April 23, 2:00pm &#8211; 3:30pm<br>
Location: MCS-148<o:p></o:p></span></p>
<div style="margin-bottom:4.0pt">
<div class="MsoNormal" align="center" style="margin-bottom:0in;margin-bottom:.0001pt;text-align:center">
<span style="color:blue">
<hr size="2" width="100%" align="center">
</span></div>
</div>
</td>
</tr>
<tr>
<td style="padding:.75pt .75pt .75pt .75pt">
<p align="center" style="margin-right:11.25pt;text-align:center"><strong><span style="font-size:11.0pt">Model Checking Techniques for Protocol Design and Analysis</span></strong><b><span style="font-size:11.0pt"><o:p></o:p></span></b></p>
<p align="center" style="mso-margin-top-alt:5.0pt;margin-right:11.25pt;margin-bottom:12.0pt;margin-left:0in;text-align:center">
<strong><span style="font-size:11.0pt">Rick Skowyra</span></strong><b><span style="font-size:11.0pt"><o:p></o:p></span></b></p>
<p class="MsoNormal" style="mso-margin-top-alt:5.0pt;margin-right:11.25pt;margin-bottom:4.0pt;margin-left:0in;text-align:justify">
<strong>Abstract:</strong> <o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:5.0pt;margin-right:11.25pt;margin-bottom:4.0pt;margin-left:0in;text-align:justify">
In recent years, outsourcing of data and computation to cloud environments has prompted the development of many new networking, data management, and distributed systems protocols. Due to the potentially high financial value of information in the cloud, as well
 as legal and regulatory implications for its leakage or loss, these protocols must often guarantee enforcement of strong availability, integrity, confidentiality, and privacy properties. To this end, verification techniques for checking system implementations
 against their specifications are increasingly used to catch violations of such properties before a protocol is deployed.
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:5.0pt;margin-right:11.25pt;margin-bottom:4.0pt;margin-left:0in;text-align:justify">
While theorem provers like Coq and Isabelle have been used in the past to perform this verification, the substantial amount of time and effort required to employ these tools has limited their adoption. Instead, model checking has often been used to expose protocol
 flaws. A model checker compares an incomplete model of the system under evaluation against a set of properties inherited from its specification. Counter-examples to these properties (bugs) are then searched for by exploring the state-space of all possible
 execution paths defined by the model. This approach is sound, but not complete: a counter-example found by model checking is guaranteed to be a real bug, but the lack of any counter-examples in the checked model does not prove the implementation is bug-free.
 Model checking has been used to find bugs in a large number of deployed protocols, ranging from cryptographic authentication schemes to transport and application layer protocols.<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:5.0pt;margin-right:11.25pt;margin-bottom:4.0pt;margin-left:0in;text-align:justify">
In this talk, I will discuss three model checkers that collectively span the design space. I will focus on the formal logics they support, the kind of problems which are most amenable to being modeled in their syntax, and the mechanisms by which the model checker
 formalizes a model and searches for counter examples. I will also present a survey of protocols in which model checkers have found severe flaws, attacks, or unexpected behavior.<span style="font-size:11.0pt"><o:p></o:p></span></p>
<p class="MsoNormal" style="mso-margin-top-alt:5.0pt;margin-right:11.25pt;margin-bottom:4.0pt;margin-left:0in;text-align:justify">
<o:p>&nbsp;</o:p></p>
<p class="MsoNormal" style="margin-right:11.25pt;text-align:justify"><b>Examination Committee:
<o:p></o:p></b></p>
<p class="MsoNormal" style="margin-right:11.25pt;text-align:justify">Azer Bestavros, Ran Canetti, and Assaf Kfoury.<span style="font-size:11.0pt;font-family:&quot;Calibri&quot;,&quot;sans-serif&quot;"><o:p></o:p></span></p>
</td>
</tr>
<tr>
<td style="padding:.75pt .75pt .75pt .75pt">
<div style="margin-bottom:4.0pt">
<div class="MsoNormal" align="center" style="margin-bottom:0in;margin-bottom:.0001pt;text-align:center">
<span style="color:blue">
<hr size="2" width="100%" align="center">
</span></div>
</div>
</td>
</tr>
</tbody>
</table>
</div>
</td>
</tr>
<tr>
<td style="padding:.75pt .75pt .75pt .75pt">
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="text-align:justify"><span style="font-size:11.0pt"><o:p>&nbsp;</o:p></span></p>
</blockquote>
</td>
</tr>
<tr>
<td style="padding:.75pt .75pt .75pt .75pt">
<div style="margin-bottom:4.0pt">
<p class="MsoNormal" align="center" style="margin-bottom:0in;margin-bottom:.0001pt;text-align:center">
<span style="font-size:11.0pt;color:blue"><o:p>&nbsp;</o:p></span></p>
</div>
</td>
</tr>
</tbody>
</table>
<p><span style="font-size:11.0pt">&nbsp;<o:p></o:p></span></p>
</div>
</body>
</html>