Entry Paulson:1999:IAI from tissec.bib
Last update: Sun Oct 15 02:58:48 MDT 2017
Top |
Symbols |
Numbers |
Math |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z
BibTeX entry
@Article{Paulson:1999:IAI,
author = "Lawrence C. Paulson",
title = "Inductive analysis of the {Internet} protocol {TLS}",
journal = j-TISSEC,
volume = "2",
number = "3",
pages = "332--351",
month = aug,
year = "1999",
CODEN = "ATISBQ",
ISSN = "1094-9224 (print), 1557-7406 (electronic)",
ISSN-L = "1094-9224",
bibdate = "Thu Oct 26 11:39:38 MDT 2000",
bibsource = "http://www.acm.org/tissec/contents/v2no3.html;
http://www.math.utah.edu/pub/tex/bib/tissec.bib",
URL = "http://www.acm.org/pubs/citations/journals/tissec/1999-2-3/p332-paulson/",
abstract = "Internet browsers use security protocols to protect
sensitive messages. An inductive analysis of TLS (a
descendant of SSL 3.0) has been performed using the
theorem prover Isabelle. Proofs are based on
higher-order logic and make no assumptions concerning
beliefs of finiteness. All the obvious security goals
can be proved; session resumption appears to be secure
even if old session keys are compromised. The proofs
suggest minor changes to simplify the analysis.
\par
TLS, even at an abstract level, is much more
complicated than most protocols verified by
researchers. Session keys are negotiated rather than
distributed, and the protocol has many optional parts.
Netherless, the resources needed to verify TLS are
modest: six man-weeks of effort and three minutes of
processor time.",
acknowledgement = ack-nhfb,
fjournal = "ACM Transactions on Information and System Security",
generalterms = "Security; Verification",
journal-URL = "http://portal.acm.org/browse_dl.cfm?idx=J789",
keywords = "authentication; inductive method; Isabelle; proof
tools; TLS",
subject = "Theory of Computation --- Logics and Meanings of
Programs --- Specifying and Verifying and Reasoning
about Programs (F.3.1): {\bf Mechanical verification};
Computer Systems Organization ---
Computer-Communication Networks --- Network Protocols
(C.2.2): {\bf Protocol verification}",
}
Related entries
- abstract,
10(1)4,
15(3)13,
15(3)14,
17(1)3,
18(2)8
- all,
1(1)93,
2(2)159,
2(4)416,
10(1)4,
10(2)5,
10(4)2,
10(4)4,
11(2)1,
11(2)3,
11(2)4,
11(2)5,
11(2)6,
11(3)13,
11(4)18,
11(4)20,
11(4)22,
12(2)10,
12(3)18,
13(1)10,
13(3)25,
13(3)28,
13(4)38,
13(4)41,
14(1)6,
14(1)14,
14(3)27,
15(1)4,
15(2)9,
15(3)14,
15(4)16,
15(4)17,
16(1)4,
17(1)2,
17(3)9,
17(3)11,
18(1)2,
18(2)5
- analysis,
1(1)66,
2(1)34,
2(2)138,
2(3)230,
4(1)1,
6(4)443,
7(2)175,
7(4)489,
8(3)312,
9(3)292,
9(4)391,
10(1)2,
10(3)9,
10(3)10,
10(3)11,
10(4)2,
10(4)6,
11(2)3,
11(3)13,
11(3)15,
11(4)17,
11(4)18,
11(4)23,
12(1)4,
12(2)10,
12(3)16,
13(1)10,
13(3)25,
13(3)26,
13(3)27,
13(4)41,
14(1)6,
14(1)8,
14(1)13,
14(2)15,
14(4)28,
15(3)14,
15(4)17,
15(4)18,
16(1)2,
16(1)4,
16(2)8,
16(3)10,
16(3)11,
16(4)14,
16(4)17,
17(1)1,
17(1)4,
17(2)7,
17(3)9,
17(4)14,
18(1)1,
18(1)4,
18(2)6
- appear,
2(2)138,
18(1)1
- assumption,
2(3)230,
3(3)161,
9(2)181,
11(2)3,
11(2)6,
11(4)20,
12(1)1,
12(1)3,
12(2)9,
12(4)21,
13(4)38,
15(1)4,
15(3)12,
16(1)4,
16(2)5,
16(4)13,
18(3)10
- authentication,
1(1)3,
2(2)138,
2(2)159,
2(2)177,
2(3)230,
2(4)354,
2(4)390,
5(4)367,
5(4)458,
6(2)258,
10(3)10,
10(3)11,
11(2)5,
11(3)14,
11(4)22,
11(4)23,
12(4)21,
13(2)17,
13(4)32,
14(1)5,
14(1)11,
14(4)29,
16(2)6,
16(2)8,
16(4)15,
17(2)6,
17(4)14,
18(1)1,
18(3)11,
18(4)14
- based,
1(1)3,
2(1)34,
2(2)177,
2(3)230,
2(3)295,
3(3)161,
7(2)319,
9(2)162,
9(2)181,
9(4)421,
10(1)2,
10(1)4,
10(2)6,
11(1)3,
11(2)1,
11(2)4,
11(3)12,
11(3)15,
11(4)17,
11(4)18,
12(1)1,
12(1)4,
12(2)13,
12(3)16,
12(3)17,
12(3)18,
13(3)24,
13(3)27,
13(3)28,
13(4)29,
13(4)30,
13(4)31,
13(4)41,
14(1)3,
14(1)4,
14(1)8,
14(1)9,
14(1)10,
14(4)30,
15(2)6,
15(2)7,
15(3)13,
16(2)8,
16(4)16,
17(1)3,
17(2)7,
17(3)12,
17(4)13,
17(4)14,
17(4)15,
17(4)16,
18(1)1,
18(1)4,
18(3)10,
18(3)11,
18(4)14
- been,
1(1)93,
2(3)269,
10(1)2,
10(3)12,
10(4)4,
11(1)2,
11(4)17,
11(4)22,
11(4)23,
12(1)1,
12(1)2,
12(3)17,
13(3)20,
13(3)27,
13(4)36,
13(4)39,
14(1)3,
14(1)13,
14(1)14,
14(3)27,
14(4)28,
15(2)10,
16(3)10,
16(4)14,
17(1)3,
17(3)12,
17(4)14,
17(4)15,
17(4)16,
18(2)7,
18(4)14
- browser,
8(2)153,
12(2)12,
16(4)13
- C.2.2,
1(1)66,
2(2)159
- change,
12(3)14,
13(4)30,
13(4)34,
14(1)2,
15(3)13,
15(4)16,
15(4)17,
16(4)17,
17(4)15,
18(3)9
- Communication, Computer-,
2(2)159,
2(3)230,
2(3)269
- complicated,
12(2)8,
16(4)17
- compromised,
10(4)6,
11(3)12,
11(3)15,
11(4)18,
12(2)13,
13(4)30,
13(4)38,
15(1)5
- computation,
1(1)26,
9(4)461,
11(2)6,
12(1)6,
13(3)22,
13(4)29,
14(1)5,
14(4)29,
14(4)31,
15(1)2,
15(2)9,
16(3)11,
17(3)11
- computer,
1(1)66,
2(1)34,
2(1)105,
2(2)159,
2(3)230,
2(3)269,
2(4)354,
2(4)416,
10(2)5,
11(4)20,
12(2)7,
13(2)11,
15(1)1,
15(2)9,
16(2)5,
17(2)6
- Computer-Communication,
2(2)159,
2(3)230,
2(3)269
- concerning,
10(1)2,
14(1)4
- descendant,
12(3)18
- distributed,
2(1)34,
2(1)105,
2(2)159,
4(2)103,
4(4)407,
6(1)128,
8(1)41,
9(1)1,
9(4)421,
10(2)7,
11(1)3,
11(1)4,
11(2)1,
11(3)14,
12(1)1,
12(1)2,
12(2)8,
12(2)12,
13(2)16,
13(3)25,
14(1)3,
14(1)12,
14(3)27,
14(4)31,
15(2)6,
15(3)13,
16(4)14,
16(4)15,
17(4)13,
18(1)2,
18(2)6
- effort,
2(2)138,
10(4)6,
15(3)13,
16(3)10
- even,
1(1)66,
2(4)416,
10(1)2,
11(1)4,
11(2)6,
11(4)22,
12(2)11,
12(4)20,
13(1)10,
13(4)30,
13(4)35,
13(4)41,
14(3)25,
14(3)27,
15(1)5,
16(3)12,
17(3)11,
17(3)12,
18(1)1
- goal,
12(2)13,
17(4)13
- has,
1(1)93,
2(1)105,
2(2)138,
2(3)230,
2(3)269,
9(4)391,
10(1)3,
10(1)4,
10(3)10,
11(1)2,
11(2)2,
11(3)14,
11(4)17,
11(4)19,
11(4)22,
11(4)23,
12(1)2,
12(2)9,
12(2)10,
12(3)15,
12(4)22,
13(3)20,
13(3)25,
13(3)26,
13(3)27,
13(3)28,
13(4)36,
14(1)3,
14(1)12,
14(1)14,
14(3)26,
14(4)28,
15(1)2,
15(2)6,
15(2)10,
15(3)12,
16(2)8,
16(4)14,
17(1)2,
17(1)3,
17(3)9,
17(3)11,
17(4)14,
17(4)15,
17(4)16,
18(2)7,
18(3)11,
18(4)14
- Internet,
2(4)390,
7(2)242,
11(2)5,
12(2)13,
12(3)17,
13(4)38,
15(3)11,
17(1)4,
17(3)12,
17(4)16
- level,
2(1)34,
2(3)269,
10(1)2,
10(1)4,
11(4)18,
12(1)4,
12(2)8,
12(4)22,
15(2)7,
15(3)12
- logic,
2(1)3,
2(1)65,
6(1)128,
6(4)501,
11(4)21,
12(1)1,
13(3)20,
14(1)8,
14(1)9,
16(4)17,
17(1)2,
17(2)5,
18(2)7
- make,
9(1)31,
10(1)2,
10(3)11,
10(4)6,
11(1)4,
11(3)13,
11(3)14,
11(4)22,
11(4)23,
12(1)1,
12(3)15,
13(3)22,
13(3)26,
13(3)28,
13(4)35,
14(4)29,
15(1)3,
15(1)4,
15(4)17,
16(3)10,
17(3)10,
18(1)1,
18(2)7,
18(4)13
- many,
1(1)93,
2(1)65,
2(2)159,
10(1)4,
10(4)1,
11(3)13,
11(4)22,
11(4)23,
12(1)2,
12(3)17,
12(3)18,
13(3)20,
13(3)22,
13(4)38,
13(4)39,
15(1)4,
15(2)6,
15(2)7,
16(2)5,
16(3)9,
16(4)17,
17(1)4,
17(3)12,
18(1)1,
18(4)13
- message,
2(2)177,
9(4)461,
10(2)8,
11(2)4,
11(2)6,
11(3)15,
11(4)23,
12(1)3,
13(4)31,
13(4)37,
14(4)32,
17(3)9,
17(4)13
- method,
1(1)3,
1(1)26,
2(2)159,
2(3)295,
2(4)416,
9(3)259,
10(1)3,
10(3)10,
10(4)4,
10(4)5,
11(2)2,
11(3)16,
11(4)19,
11(4)22,
12(1)2,
12(1)6,
12(2)13,
12(3)16,
13(2)15,
13(4)35,
15(1)4,
15(2)10,
15(3)12,
15(4)15,
15(4)17,
17(3)12,
18(3)9
- minor,
10(3)9,
18(3)11
- minutes,
17(4)13,
18(1)2
- modest,
13(3)25,
13(4)34,
15(2)6,
16(3)9,
16(3)11
- more,
2(1)3,
2(1)65,
9(2)181,
9(4)391,
9(4)421,
9(4)461,
10(1)4,
10(3)9,
10(4)1,
10(4)4,
10(4)6,
11(2)3,
11(2)4,
11(2)6,
11(3)14,
11(4)21,
12(1)1,
12(2)8,
12(2)10,
12(2)12,
12(2)13,
12(3)18,
13(1)10,
13(3)20,
13(3)21,
13(3)22,
13(3)28,
13(4)32,
13(4)34,
13(4)39,
14(3)27,
14(4)31,
15(1)2,
15(1)5,
15(2)8,
15(2)9,
15(3)11,
15(3)12,
15(4)16,
16(1)2,
16(2)8,
16(3)10,
16(3)11,
16(4)17,
17(1)2,
17(1)3,
17(3)9,
17(4)14,
17(4)16,
18(1)1,
18(3)11,
18(4)13
- most,
9(4)391,
11(2)2,
11(3)12,
11(4)22,
12(2)8,
12(2)12,
12(3)14,
12(4)21,
13(1)10,
13(3)27,
13(4)30,
14(3)27,
15(1)5,
15(2)6,
15(4)15,
15(4)18,
16(1)4,
16(2)6,
16(4)13,
16(4)14,
17(3)11,
17(3)12,
17(4)16,
18(1)1
- much,
12(2)10,
13(2)13,
13(3)28,
15(1)5,
15(3)14,
15(4)16,
18(3)11
- needed,
10(4)3,
14(1)5,
15(2)10,
15(4)15,
17(4)13,
18(2)6
- old,
18(2)5
- organization,
1(1)66,
2(1)34,
2(1)65,
2(1)105,
2(2)159,
2(3)230,
2(3)269,
2(4)416,
9(2)113,
9(4)391,
10(4)2,
11(1)3,
12(3)15,
14(3)23,
14(3)25
- part,
10(3)9,
10(4)4,
11(2)2,
11(4)20,
12(1)1,
13(1)10,
15(2)8,
15(2)9,
16(4)15,
17(2)6,
17(4)16
- Paulson, Lawrence C.,
9(2)138
- performed,
3(4)262,
9(4)421,
10(4)6,
11(4)18,
13(4)40
- processor,
16(1)1
- program,
2(1)65,
11(3)14,
12(1)1,
12(2)10,
12(2)11,
12(3)16,
12(3)19,
13(3)21,
14(3)24,
15(1)2,
15(2)10,
16(2)7,
17(1)2,
17(3)11,
18(1)4
- proof,
1(1)93,
2(3)230,
2(4)354,
9(2)181,
10(2)6,
11(3)13,
12(1)3,
12(2)8,
13(3)20,
13(3)25,
14(1)12,
15(1)4,
17(1)4,
17(4)15,
18(1)4,
18(2)8
- protect,
11(1)3,
12(3)15,
13(3)22,
13(3)28,
13(4)32,
15(4)18,
16(1)1,
16(2)6,
17(1)4,
17(3)10,
18(1)1
- proved,
15(3)11,
18(2)8
- rather,
2(1)65,
9(4)461,
10(2)8,
12(3)16,
13(1)10,
13(4)31,
15(4)15,
18(4)13
- reasoning,
6(1)71,
7(4)591,
11(3)12,
12(1)4,
12(1)5,
13(3)20,
14(1)8,
14(2)16
- researcher,
11(1)2,
12(1)2,
12(3)17,
13(4)36,
16(3)10,
16(4)16,
17(1)1
- resource,
9(4)391,
10(4)4,
11(1)2,
11(1)3,
11(1)4,
11(2)2,
11(3)14,
11(4)19,
11(4)20,
12(1)1,
12(1)6,
12(4)22,
13(3)20,
14(1)7,
14(1)10,
15(4)18,
17(1)2,
17(3)9,
18(2)6
- secure,
1(1)93,
2(2)159,
2(2)177,
2(4)390,
4(1)72,
4(2)103,
4(2)134,
4(4)321,
5(3)290,
6(4)472,
7(4)523,
9(1)1,
9(1)31,
9(1)94,
9(2)162,
9(4)461,
10(2)8,
10(3)10,
10(3)11,
10(4)3,
10(4)6,
11(2)4,
11(2)5,
11(3)13,
11(3)14,
11(4)18,
11(4)22,
11(4)23,
12(1)2,
12(1)3,
12(1)6,
12(3)16,
12(3)18,
12(4)21,
12(4)22,
13(1)9,
13(3)21,
13(3)28,
13(4)29,
14(3)23,
14(3)27,
14(4)31,
15(2)6,
15(2)9,
16(3)11,
16(4)15,
17(2)5,
17(2)6,
17(4)13,
18(2)5,
18(4)13
- sensitive,
1(1)26,
2(2)159,
6(1)1,
10(2)5,
10(2)7,
10(3)12,
12(2)9,
12(3)15,
13(3)21,
13(3)22,
13(3)24
- session,
7(3)333,
10(2)8,
10(4)2,
16(3)10,
16(4)15
- simplify,
2(1)65,
2(1)105,
13(4)37
- specifying,
9(4)421,
10(1)2,
10(1)3,
13(3)20,
14(1)8,
15(3)13,
16(2)5
- SSL,
12(3)17,
13(1)10
- suggest,
10(4)5,
12(1)5,
16(1)4,
17(1)1
- than,
2(1)3,
2(1)65,
9(4)391,
9(4)461,
10(1)4,
11(2)3,
11(2)6,
11(3)14,
12(1)1,
12(2)10,
12(3)16,
12(4)22,
13(1)10,
13(3)21,
13(4)29,
13(4)31,
13(4)35,
14(3)27,
14(4)31,
15(1)5,
15(2)9,
15(2)10,
15(4)15,
15(4)16,
16(2)8,
16(4)17,
17(1)2,
17(3)9,
17(3)10,
17(3)12,
17(4)14,
17(4)16,
18(4)13
- theorem,
18(2)6
- theory,
2(1)3,
2(1)105,
13(4)40,
14(4)31,
16(1)4,
16(4)16,
16(4)17,
17(3)10
- three,
2(1)105,
9(2)181,
12(2)10,
13(3)25,
13(4)31,
16(2)6,
16(2)8,
16(4)16,
17(2)8,
17(4)13,
18(3)11,
18(4)12
- time,
2(1)105,
2(4)390,
2(4)416,
9(4)461,
10(1)3,
10(2)8,
11(2)3,
11(2)4,
11(2)5,
11(3)13,
11(4)17,
11(4)20,
11(4)21,
11(4)23,
12(2)8,
12(3)17,
12(3)18,
12(3)19,
12(4)20,
12(4)21,
12(4)22,
13(4)37,
13(4)39,
14(1)2,
14(1)11,
14(1)14,
14(3)26,
14(4)31,
15(2)7,
15(3)12,
15(4)17,
16(1)4,
16(4)13,
16(4)14,
16(4)17,
17(3)9,
17(3)10,
17(3)11,
17(4)13,
18(1)2,
18(1)4,
18(3)10
- TLS,
4(2)134,
7(4)553,
11(1)2,
15(1)3
- tool,
1(1)66,
2(4)390,
7(2)274,
9(2)181,
10(4)2,
12(2)10,
13(3)24,
13(3)26,
13(4)30,
13(4)40,
14(1)6,
15(1)3,
15(4)18,
16(1)4,
16(2)7,
17(2)7,
18(1)1,
18(1)4
- use,
2(1)3,
2(1)105,
2(2)138,
2(2)177,
2(3)230,
2(3)269,
2(4)354,
2(4)390,
4(2)103,
7(1)21,
9(4)391,
9(4)421,
9(4)461,
10(1)4,
10(2)5,
10(3)11,
10(4)1,
10(4)3,
10(4)5,
10(4)6,
11(1)2,
11(1)3,
11(1)4,
11(2)1,
11(2)4,
11(3)13,
11(3)14,
11(4)18,
11(4)19,
11(4)21,
11(4)22,
12(2)10,
12(3)16,
12(3)18,
13(3)22,
13(3)24,
13(3)25,
13(4)29,
13(4)31,
13(4)36,
14(1)6,
14(1)8,
14(1)10,
14(1)11,
14(4)31,
14(4)32,
15(1)3,
15(1)4,
15(1)5,
15(2)7,
15(3)12,
15(4)15,
15(4)16,
15(4)17,
16(2)8,
16(4)15,
16(4)17,
17(2)5,
17(2)6,
17(2)7,
17(2)8,
17(4)15,
17(4)16,
18(1)1,
18(2)6,
18(3)9,
18(4)14
- using,
2(2)138,
2(2)177,
4(3)289,
6(2)258,
6(3)327,
9(2)113,
9(2)162,
9(2)181,
9(3)292,
9(3)325,
9(4)461,
10(1)4,
10(2)8,
10(3)11,
10(4)3,
10(4)6,
11(1)2,
11(2)1,
11(2)2,
11(2)3,
11(3)14,
11(4)19,
11(4)21,
12(2)10,
12(2)11,
13(1)2,
13(1)8,
13(3)20,
13(3)26,
13(4)31,
13(4)35,
13(4)39,
14(1)3,
14(1)12,
14(1)14,
14(3)27,
15(1)2,
15(3)11,
15(3)12,
15(4)15,
15(4)17,
16(1)1,
16(1)2,
16(1)4,
16(2)5,
16(2)6,
16(3)10,
16(4)17,
17(1)1,
17(2)5,
17(3)10,
17(3)11,
17(4)13,
17(4)14,
17(4)16,
18(2)7,
18(2)8,
18(3)10,
18(3)11,
18(4)14
- verification,
3(1)51,
8(3)287,
10(2)5,
10(2)6,
10(2)7,
10(3)9,
10(3)11,
11(2)5,
11(3)14,
12(1)3,
12(1)6,
14(1)5,
14(3)25,
14(4)32,
15(1)3,
15(2)9,
15(4)18,
16(2)8,
17(2)6,
18(2)6,
18(2)8,
18(3)11,
18(4)14
- verified,
9(2)138,
13(3)26,
15(1)3,
15(3)11,
16(4)17,
18(2)7
- verify,
9(4)421,
11(2)5,
11(3)14,
14(1)12,
15(1)3,
16(3)11,
17(2)6,
18(2)6,
18(3)11
- verifying,
10(2)5,
10(2)7,
10(3)11,
11(2)5,
14(3)25,
15(4)18