1	Proof Planning in Logical Frameworks Carsten Schürmann Yale University September 2002
2	Motivating questions Is the number of CERT advisories increasing or decreasing? Who can vouch for the correctness of the BLUETOOTH protocol? Will we ever vote electronically? Is the complexity of network protocols increasing or decreasing?
3	Safety Architectures Examples Authentication Network routing E-voting Mobile Code Requirements Flexible design Extensibility Trust
4	Type System (toy)
5	Type System (real)
6	Programming Languages
7	Complexity Safety proof languages PCC : 129 rules [Necula, Lee 97] FPCC : several 100 rules [Appel, Felty 01] FLINT : ?? rules [Zhao, et al 02] Typed Assembly Language Type theory: 31 rules [Morrisett, Crary … 98] Proof Checker: approx 4000 lines Blue Tooth Protocol Type system: 1000 pages prose
8	We need tools to … … control the inherent complexity design safety architectures reason about our designs automate reasoning processes involved program with our designs
9	Dimension 1: Design Logical Frameworks encode Safety Proof Languages Type Systems Security Protocols Benefit: Storing Shipping Checking
10	Dimension 1: Design Safety Proof Languages Higher-order logic Temporal Logic Modal Logic Linear Logic Coq Logic Type Systems
11	Dimension 2: Reasoning Meta logical framework Consistency Completeness Type Safety Freeness of attacks Benefit: Trusting Verifying
12	Dimension 2: Reasoning
13	Dimension 3: Automation Proof planning [CS, Autexier] Push buttom technology Ease of use Failure interpretation Benefit: Level of abstraction Interactive design cycle Quick response
14	Dimension 3: Automation
15	Dimension 4: Programming Delphin [CS, Yu, Poswolsky] Compilers [CS, Xi] Client-server Architecture Theorem Provers for Proof Carrying Authentication Benefit: Direct manipulation of derivations Automatic code generation
16	Dimension 4: Programming
17	Rest of this Talk Proof Planning in Twelf Used at Yale, CMU, Princeton, Stanford, Harvard (?)…
18	Overview
19	Let’s get started
20	Safety Proof Language Intuitionistic logic: Sequent calculus: [Gentzen 35] Judgment: Rules:
21	Representation Logical framework LF [Honsell, Harper, Plotkin 93] Simply typed λ-calculus Dependent types Paradigm Judgments as types (assumptions as contexts) Derivations as objects
22	Representation (cont’d) Inference rules as constants
23	Representation (cont’d) Reasoning about the real world is as good as the encoding is
24	Logical Frameworks Research Focuses on common concepts Hypotheses State Enriches logical framework Substitution (beta reduction) Update (resource oriented logics)
25	Logical Frameworks Research Emphasis 1: Representation Extend frameworks conservatively Terms are not dead, they live! Example: Twelf Emphasis 2: Reasoning Examples: Coq, Isabelle, Lego
26	Remarks Elegance Higher-order representation techniques Dependent types Benefit for this work: Variables and substitutions come for free!
27	Overview
28	Is the Logic Consistent? Theorem [Admissibility]: [Gentzen 35] If and then
29	Meta Logic M_w First-order logic Induction principles for arbitrary higher-order encodings [CS 00,01]
30	Proof Planning
31	The Situation What we have: Logical Framework LF Proofs by induction How can we find proofs automatically and quickly?
32	Pruning the Search Space
33	Common Operations Splitting (Case analysis) Recursion (Induction hypothesis) Filling Constructing safety proofs Resolution based techniques
34	Profiling reveals With naïve Prototype implementation:
35	Explanation Reason 1: Search spaces enormous Reason 2: Side effect of failure
36	Possible Tackles Reason 1: Search spaces enormous Tabled proof search [Pientka ‘02] Outsourcing [Vampire?] Reason 2: Side effect of failure Pruning through proof plans Decidable criterion
37	Approximations Meta Logic
38	Proof Planning Calculus P_w First order logic [CS, Autexier 02] Propositions approximate type families Natural deduction Decidable (because of M2L)
39	Central Insight Exploit information contained in types indices. Example: “We have an object of type family conc containing information on A” “We have another object of type family conc containing information on B once we know …”
40	Observation There is no proof of But Splitting on (D, E) Proof plans exist for each case. Let’s try to prove. SUCCESS!
41	A Few Details Abstraction is defined as follows
42	Soundness Theorem If without case rules And Then . Proof: by induction on . Benefit: Read it backwards!
43	Summary Proof planning calculus P_w Recognizes unpromising states Provides proof search guidance Gives a logical explanation to proof plans Failure criterion Inspects a proof state Recognizes unpromising ones quickly Decidable
44	Summary Importance Push button technology Network/authentication/e-voting protocols Proof planning system P_w Works for encodings in LF TI-abstraction [Giungilia, Walsh 91] Implementation is underway
45	Our Goal: Tools to … design safety architectures reason about our designs automate reasoning processes involved program with our designs We are on the way!
46	Future Work Alternative proof techniques Logical relations [CS, Sarnat] Coinduction [CS, Momigliano] Application domain Network protocols E-Voting Infinite structures Choice sequences vs. Co-induction Adequate representation of infinite traces
47	Conclusion For more information about Twelf and Delphin check
48	Authentication Protocols