Irrelevant clauses in resolution problems increase the search space, making proofs hard to find in a reasonable amount of processor time. Simple relevance filtering methods, based on counting symbols...
MetiTarski: An Automatic Prover for the Elementary Functions (2009)
Behzad Akbarpour, Lawrence C. Paulson
Abstract. Many inequalities involving the functions ln, exp, sin, cos, etc., can be proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure...
Applications of MetiTarski in the Verification of Control and Hybrid Systems (2009)
Behzad Akbarpour, Lawrence C. Paulson
Abstract. MetiTarski, an automatic proof procedure for inequalities on elementary functions, can be used to verify control and hybrid systems. We perform a stability analysis of control systems using...
Verifying Electronic Commerce Protocols (2009)
Security protocols prevent network communications from being compromised by adversaries. Those designed for electronic commerce have many differences from traditional security protocols. They must...
Clemens Ballarin, Lawrence C. Paulson
Abstract. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that...
Experiments on supporting interactive proof using resolution (2009)
Abstract. Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for...
Sidi O. Ehmety, Lawrence C. Paulson
Abstract. The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The...
Reasoning about Coding Theory: The Benefits We Get from Computer Algebra (2009)
Clemens Ballarin, Lawrence C. Paulson
Abstract. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that...
Additional Key Words and Phrases: Set theory, specification, types (2009)
Lawrence C. Paulson, Carl A. Gunter
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language...
Mechanizing UNITY in Isabelle (2009)
UNITY is an abstract formalism for proving properties of concurrent systems, which typically are expressed using guarded assignments [Chandy and Misra 1988]. UNITY has been mechanized in higher-order...
Authentication Logics: New Theory and Implementations (2009)
Lawrence C. Paulson, Roger M Needham
was undertaken to provide better tools for verifying security protocols. A new method has been developed in which protocols are modelled inductively [5]. The method has been applied to numerous...
Verifying Electronic Commerce Protocols (2009)
This proposal concerns protocol verification by formal proof. With EPSRC funding, Paulson has developed a new and highly successful approach to verifying security protocols: the inductive method. The...
Automation for Interactive Proof Final Report (2009)
The idea of supporting interactive provers using automatic ones is an old one. An important early effort is the KIV system [1], which has been integrated with 3TAP. Hurd has integrated HOL4 with...
Compositional Proofs of Concurrent Programs (2009)
Council (EPSRC), was undertaken to provide a better understanding of compositional reasoning, that is, how to verify systems built from components. It is a continuation of project GR/K57381,...
Locales: A sectioning concept for Isabelle (2009)
Florian Kammüller, Markus Wenzel, Lawrence C. Paulson
Abstract. Locales are a means to define local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are...
Communication Networks]: Network Protocols—Protocol Verification (2009)
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...
Source-Level Proof Reconstruction for Interactive Theorem Proving (2009)
Lawrence C. Paulson, Kong Woei Susanto
Abstract. Interactive proof assistants should verify the proofs they receive from automatic theorem provers. Normally this proof reconstruction takes place internally, forming part of the integration...
α The Isabelle Reference Manual (2009)
Lawrence C. Paulson, Tobias Nipkow, Markus Wenzel
Note: this document is part of the earlier Isabelle documentation, which is somewhat superseded by the Isabelle/HOL Tutorial [11]. Much of it is concerned with the old-style theory syntax and the...
An overview of the verification of SET (2009)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
Abstract This paper describes the verification of Secure Electronic Transaction (SET), an e-commerce protocol by VISA and MasterCard. The main tasks are to comprehend the written documentation, to...
Verifying the SET protocol: Overview (2009)
Abstract. The project to verify SET, an e-commerce protocol, is described. The main tasks are to comprehend the written documentation, to produce an accurate formal model, to identify specific...
Lightweight relevance filtering for machine-generated resolution problems (2009)
Irrelevant clauses in resolution problems increase the search space, making it hard to find proofs in a reasonable time. Simple relevance filtering methods, based on counting function symbols in...
Exploring properties of normal multimodal logics in simple type theory with LEO-II (2009)
Christoph Benzmüller, Lawrence C. Paulson, To Peter, B. Andrews
There are two well investigated approaches to automate reasoning in modal logics: the direct approach and the translational approach. The direct approach [6, 7, 14, 27] develops specific calculi and...
Translating higher-order problems to first-order clauses (2009)
Proofs involving large specifications are typically carried out through interactive provers that use higher-order logic. A promising approach to improve the automation of interactive provers is by...
Relations between secrets: Two formal analyses of the Yahalom protocol (2009)
The Yahalom protocol is one of those analyzed by Burrows et al. [5]. Based upon their analysis, they have proposed modifications to make the protocol easier to understand and to analyze. Both...
Defining functions on equivalence classes (2009)
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The...
Automation for interactive proof: First prototype (2009)
Jia Meng, Claire Quigley, Lawrence C. Paulson
Interactive theorem provers require too much effort from their users. We have been developing a system in which Isabelle users obtain automatic support from automatic theorem provers (ATPs) such as...
A Termination Checker for Isabelle Hoare Logic (2009)
Jia Meng, Lawrence C. Paulson, Gerwin Klein
Abstract. Hoare logic is widely used for software specification and verification. Frequently we need to prove the total correctness of a program: to prove that the program not only satisfies its pre-...
Mechanising Temporal Reasoning: Summary (2009)
(EPSRC), was undertaken to continue research and development involving the proof tool Isabelle. The emphasis was on temporal logics. Its results include a mechanisation of the UNITY formalism [6] and...
Formal verification of cardholder registration in SET (2009)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
Abstract. The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic...
Mechanizing a theory of program composition for UNITY (2009)
Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which...
Isabelle: The next seven hundred theorem provers (2009)
Isabelle [2] is a theorem prover for a large class of logics. The object-logics are formalized within Isabelle’s meta-logic, which is intuitionistic higher-order logic with implication, universal...
Quantified Multimodal Logics in Simple Type Theory (2009)
Benzmueller, Christoph, Paulson, Lawrence C.
We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of...
Mechanising Temporal Reasoning: Summary (2008)
(EPSRC), was undertaken to continue research and development involving the proof tool Isabelle. The emphasis was on temporal logics. Its results include a mechanisation of the UNITY formalism [6] and...
Verifying Electronic Commerce Protocols (2008)
Security protocols prevent network communications from being compromised by adversaries. Those designed for electronic commerce have many differences from traditional security protocols. They must...
Verifying Electronic Commerce Protocols (2008)
This proposal concerns protocol verification by formal proof. With EPSRC funding, Paulson has developed a new and highly successful approach to verifying security protocols: the inductive method. The...
Defining functions on equivalence classes (2008)
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The...
Authentication Logics: New Theory and Implementations (2008)
Lawrence C. Paulson, Roger M Needham
was undertaken to provide better tools for verifying security protocols. A new method has been developed in which protocols are modelled inductively [5]. The method has been applied to numerous...
Automation for Interactive Proof Final Report 1 Background/Context (2008)
The idea of supporting interactive provers using automatic ones is an old one. An important early effort is the KIV system [1], which has been integrated with 3TAP. Hurd has integrated HOL4 with...
Compositional Proofs of Concurrent Programs (2008)
Council (EPSRC), was undertaken to provide a better understanding of compositional reasoning, that is, how to verify systems built from components. It is a continuation of project GR/K57381,...
Compositional Proofs of Concurrent Programs (2008)
This proposal concerns proving the correctness of programs expressed in the UNITY formalism. Under an existing EPSRC project, Paulson has already developed an environment for verifying UNITY...
Noname manuscript No. (will be inserted by the editor) An Overview of the Verification of SET (2008)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
The date of receipt and acceptance will be inserted by the editor Abstract This paper describes the verification of Secure Electronic Transaction (SET), an e-commerce protocol by VISA and MasterCard....
Exploring Properties of Normal Multimodal Logics in Simple Type Theory with Leo-II 1 (2008)
Christoph E. Benzmüller, Lawrence C. Paulson
There are two well investigated approaches to automate reasoning in modal logics: the direct approach and the translational approach. The direct approach [6, 7, 14, 27] develops specific calculi and...
Translating Higher-Order Clauses to First-Order Clauses (2008)
Abstract. Interactive provers typically use higher-order logic, while automatic provers typically use first-order logic. In order to integrate interactive provers with automatic ones, it is necessary...
A Termination Checker for Isabelle Hoare Logic (2008)
Jia Meng, Lawrence C. Paulson, Gerwin Klein
Abstract. Hoare logic is widely used for software specification and verification. Frequently we need to prove the total correctness of a program: to prove that the program not only satisfies its pre-...
Verifying the SET protocol: Overview (2008)
Abstract. The project to verify SET, an e-commerce protocol, is described. The main tasks are to comprehend the written documentation, to produce an accurate formal model, to identify specific...
Communication Networks]: Network Protocols—Protocol Verification (2008)
Giampaolo Bella, Lawrence C. Paulson
Classical security protocols aim to achieve authentication and confidentiality under the assumption that the peers behave honestly. Some recent protocols are required to achieve their goals even if...
Extending a Resolution Prover for Inequalities on Elementary Functions (2008)
Behzad Akbarpour, Lawrence C. Paulson
Abstract. Experiments show that many inequalities involving exponentials and logarithms can be proved automatically by combining a resolution theorem prover with a decision procedure for the theory...
Source-Level Proof Reconstruction for Interactive Theorem Proving (2008)
Lawrence C. Paulson, Kong Woei Susanto
Abstract. Interactive proof assistants should verify the proofs they receive from automatic theorem provers. Normally this proof reconstruction takes place internally, forming part of the integration...
A Termination Checker for Isabelle Hoare Logic (2008)
Jia Meng, Lawrence C. Paulson, Gerwin Klein
Abstract. Hoare logic is widely used for software specification and verification. Frequently we need to prove the total correctness of a program: to prove that the program not only satisfies its pre-...
Additional Key Words and Phrases: Set theory, specification, types (2008)
Lawrence C. Paulson, Carl A. Gunter
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language...
Communication Networks]: Network Protocols—Protocol Verification (2008)
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...
Abstract Automation for Interactive Proof: First Prototype (2008)
Jia Meng, Claire Quigley, Lawrence C. Paulson
Interactive theorem provers require too much effort from their users. We have been developing a system in which Isabelle users obtain automatic support from automatic theorem provers (ATPs) such as...
Sidi O. Ehmety, Lawrence C. Paulson
Abstract. The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The...
An overview of the verification of SET (2008)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
Abstract This paper describes the verification of Secure Electronic Transaction (SET), an e-commerce protocol by VISA and MasterCard. The main tasks are to comprehend the written documentation, to...
Translating Higher-Order Clauses to First-Order Clauses (2008)
Abstract. Interactive provers typically use higher-order logic, while automatic provers typically use first-order logic. In order to integrate interactive provers with automatic ones, it is necessary...
Defining functions on equivalence classes (2008)
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The...
Abstract Mechanizing Coinduction and Corecursion in Higher-order Logic (2008)
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists;...
Communication Networks]: Network Protocols—Protocol Verification (2008)
Internet browsers use security protocols to protect confidential messages. An inductive analysis of TLS (a descendant of SSL 3.0) has been performed using the theorem prover Isabelle. Proofs are...
Clemens Ballarin, Lawrence C. Paulson
Abstract. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that...
Abstract Automation for Interactive Proof: First Prototype (2008)
Jia Meng, Claire Quigley, Lawrence C. Paulson
Interactive theorem provers require too much effort from their users. We have been developing a system in which Isabelle users obtain automatic support from automatic theorem provers (ATPs) such as...
Reasoning about Coding Theory: The Benefits We Get from Computer Algebra (2008)
Clemens Ballarin, Lawrence C. Paulson
Abstract. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that...
Additional Key Words and Phrases: Set theory, specification, types (2008)
Lawrence C. Paulson, Carl A. Gunter
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language...
Defining Functions on Equivalence Classes (2008)
Lawrence Paulson Computer, Lawrence C. Paulson
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The...
Markus Wenzel, Lawrence C. Paulson
This volume is a self-contained introduction to interactive proof in higherorder logic (HOL), using the proof assistant Isabelle. It is written for potential users rather than for our colleagues in...
LEO-II — A cooperative automatic theorem prover for higher-order logic (2008)
Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss
Abstract. LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present...
α Isabelle’s Logics: HOL 1 (2008)
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
Reasoning About Coding Theory: The Benefits We Get from Computer Algebra (2007)
Clemens Ballarin And, Clemens Ballarin, Lawrence C. Paulson
. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports...
Compositional Proofs of Concurrent Programs (2007)
neric theorem prover. It supports interactive proof in several formal systems, including first-order logic, higher-order logic and Zermelo-Frankel set theory. Derived logics can be supported as well...
Reasoning about Coding Theory: The Benefits We Get from Computer Algebra (2007)
Clemens Ballarin, Lawrence C. Paulson
. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports...
An overview of the verification of SET (2007)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
Abstract This paper describes the verification of Secure Electronic Transaction (SET), an e-commerce protocol by VISA and MasterCard. The main tasks are to comprehend the written documentation, to...
Zermelo-Fraenkel (ZF) set theory is widely regarded as unsuitable for automated reasoning. But a computational logic has been formally derived from the ZF axioms using Isabelle. The library of...
Final Coalgebras as Greatest Fixed Points in ZF Set Theory ∗ (2007)
Lawrence C. Paulson, L. C. Paulson
A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition of function...
1 Folderol: a simple theorem prover 3 1.1 Representation of rules.......................... 4 1.2 Propositional logic............................ 5
Additional Key Words and Phrases: Set theory, specification, types (2007)
Lawrence C. Paulson, Carl A. Gunter
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language...
The theorem prover Isabelle and several of its object-logics are described. Where other papers [15] have been concerned with theory, the emphasis here is completely practical: the operations,...
Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty....
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as “strictly positive, ” the approach lets definitions involve any operators that have...
λ β Isabelle’s Logics: HOL (2007)
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
This manual describes Isabelle’s formalization of Higher-Order Logic, a polymorphic version of Church’s Simple Theory of Types. HOL can be best understood as a simply-typed version of classical...
Should Your Specification Language Be Typed? LESLIE (2007)
Lawrence C. Paulson, Carl A. Gunter
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language...
Applications of Proof Theory to Isabelle (2007)
Isabelle [3, 4] is a generic theorem prover. It suppports interactive proof in several formal systems, including first-order logic (intuitionistic and classical), higher-order logic, Martin-Löf type...
Verifying the SET protocol: Overview (2007)
Abstract. The project to verify SET, an e-commerce protocol, is described. The main tasks are to comprehend the written documentation, to produce an accurate formal model, to identify specific...
Sidi O. Ehmety, Lawrence C. Paulson
Abstract. The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The...
by the Inductive Method (2007)
Mechanising Ban Kerberos, Giampaolo Bella, Lawrence C Paulson
Abstract. The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of...
λ β Isabelle’s Logics: HOL 1 (2007)
Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel
Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm
λ β The Isabelle Reference Manual (2007)
Lawrence C. Paulson, Tobias Nipkow, Markus Wenzel
Note: this document is part of the earlier Isabelle documentation, which is somewhat superseded by the Isabelle/HOL Tutorial [11]. Much of it is concerned with the old-style theory syntax and the...
Extending a Resolution Prover for Inequalities on Elementary Functions (2007)
Behzad Akbarpour, Lawrence C. Paulson
Abstract. Experiments show that many inequalities involving exponentials and logarithms can be proved automatically by combining a resolution theorem prover with a decision procedure for the theory...
Lightweight relevance filtering for machine-generated resolution problems (2006)
Irrelevant clauses in resolution problems increase the search space, making it hard to find proofs in a reasonable time. Simple relevance filtering methods, based on counting function symbols in...
Lightweight relevance filtering for machine-generated resolution problems (2006)
Irrelevant clauses in resolution problems increase the search space, making it hard to find proofs in a reasonable time. Simple relevance filtering methods, based on counting function symbols in...
Towards automatic proofs of inequalities involving elementary functions (2006)
Behzad Akbarpour, Lawrence C. Paulson
Inequalities involving functions such as sines, exponentials and logarithms lie outside the scope of decision procedures, and can only be solved using heuristic methods. Preliminary investigations...
Translating higher-order problems to first-order clauses (2006)
Proofs involving large specifications are typically carried out through interactive provers that use higher-order logic. A promising approach to improve the automation of interactive provers is by...
Translating higher-order problems to first-order clauses (2006)
Proofs involving large specifications are typically carried out through interactive provers that use higher-order logic. A promising approach to improve the automation of interactive provers is by...
Lightweight relevance filtering for machine-generated resolution problems (2006)
Irrelevant clauses in resolution problems increase the search space, making proofs hard to find in a reasonable amount of processor time. Simple relevance filtering methods, based on counting symbols...
Translating higher-order problems to first-order clauses (2006)
Proofs involving large specifications are typically carried out through interactive provers that use higher-order logic. A promising approach to improve the automation of interactive provers is by...
Lightweight relevance filtering for machine-generated resolution problems (2006)
Irrelevant clauses in resolution problems increase the search space, making it hard to find proofs in a reasonable time. Simple relevance filtering methods, based on counting function symbols in...
Translating higher-order problems to first-order clauses (2006)
Proofs involving large specifications are typically carried out through interactive provers that use higher-order logic. A promising approach to improve the automation of interactive provers is by...
Towards Automatic Proofs of Inequalities Involving Elementary Functions (2006)
Behzad Akbarpour, Lawrence C. Paulson
Inequalities involving functions such as sines, exponentials and logarithms lie outside the scope of decision procedures, and can only be solved using heuristic methods. Preliminary investigations...
Proof Pearl: Defining Functions Over Finite Sets. volume 3603 of LNCS (2005)
Tobias Nipkow, Lawrence C. Paulson
Abstract. Structural recursion over sets is meaningful only if the result is independent of the order in which the set’s elements are enumerated. This paper outlines a theory of function definition...
Proof Pearl: Defining Functions Over Finite Sets. volume 3603 of LNCS (2005)
Tobias Nipkow, Lawrence C. Paulson
Abstract. Structural recursion over sets is meaningful only if the result is independent of the order in which the set’s elements are enumerated. This paper outlines a theory of function definition...
Proof Pearl: Defining Functions Over Finite Sets. volume 3603 of LNCS (2005)
Tobias Nipkow, Lawrence C. Paulson
Abstract. Structural recursion over sets is meaningful only if the result is independent of the order in which the set’s elements are enumerated. This paper outlines a theory of function definition...
Accountability Protocols: Formalized and Verified (2004)
Giampaolo Bella, Lawrence C. Paulson
This paper provides a comparative, formal analysis of the two protocols, and confirms that they reach their goals under realistic conditions. The treatment, which is conducted with mechanized support...
Experiments On Supporting Interactive Proof Using Resolution (2004)
Abstract. Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for...
Experiments On Supporting Interactive Proof Using Resolution (2004)
Abstract. Interactive theorem provers can model complex systems, but require much effort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for...
Experiments on Supporting Interactive Proof Using Resolution (2004)
Interactive theorem provers can model complex systems, but require much e#ort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for very...
Organizing numerical theories using axiomatic type classes (2004)
Mathematical reasoning may involve several arithmetic types, including those of the natural, integer, rational, real and complex numbers. These types satisfy many of the same algebraic laws. These...
Organizing numerical theories using axiomatic type classes (2004)
Mathematical reasoning may involve several arithmetic types, including those of the natural, integer, rational, real and complex numbers. These types satisfy many of the same algebraic laws. These...
Verifying the SET registration protocols (2003)
Giampaolo Bella, Lawrence C. Paulson
Abstract—SET (Secure Electronic Transaction) is an immense e-commerce protocol designed to improve the security of credit card purchases. In this paper we focus on the initial bootstrapping phases...
Verifying the SET registration protocols (2003)
Giampaolo Bella, C Giampaolo Bella, Fabio Massacci, Fabio Massacci, Lawrence C. Paulson, Lawrence C. Paulson
SET (Secure Electronic Transaction) is an immense e-commerce protocol designed to improve the security of credit card purchases. In this paper we focus on the initial bootstrapping phases of SET,...
Verifying the SET registration protocols (2003)
Giampaolo Bella, Lawrence C. Paulson
Abstract—SET (Secure Electronic Transaction) is an immense e-commerce protocol designed to improve the security of credit card purchases. In this paper we focus on the initial bootstrapping phases...
Verifying Second-Level Security Protocols (2003)
Giampaolo Bella, Cristiano Longo, Lawrence C Paulson
A second-level security protocol is defined as a security protocol that relies on an underlying security protocol in order to achieve its goals. The verification of classical authentication protocols...
Verifying the SET Registration Protocols (2003)
Giampaolo Bella Jj, Giampaolo Bella, Lawrence C. Paulson
SET (Secure Electronic Transaction) is an immense e-commerce protocol designed to improve the security of credit card purchases.
Mechanizing Compositional Reasoning for Concurrent Systems: Some Lessons (2003)
Lawrence C. Paulson, Lawrence C. Paulson, Lawrence C. Paulson
The paper reports on experiences of mechanizing various proposals for compositional reasoning in concurrent systems. The work uses the UNITY formalism and the Isabelle proof tool. The proposals...
Verifying the SET registration protocols (2003)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
Abstract—Secure electronic transaction (SET) is an immense e-commerce protocol designed to improve the security of credit card purchases. In this paper, we focus on the initial bootstrapping phases...
Isabelle’s isabelle’s logics: FOL and ZF (2003)
Lawrence C. Paulson, Tobias Nipkow, Markus Wenzel
This manual describes Isabelle’s formalizations of many-sorted first-order logic (FOL) and Zermelo-Fraenkel set theory (ZF). See the Reference Manual for general Isabelle commands, and Introduction...
Program composition in Isabelle/UNITY (2002)
Sidi O. Ehmety, Lawrence C. Paulson
We describe the mechanization of recent examples of compositional reasoning, due to Charpentier and Chandy [4]. The examples illustrate a new theory for composition proposed by Chandy and Sanders [2,...
Computer Science Tripos, Lawrence C Paulson
Contents 1 Introduction and Learning Guide 1 2 Propositional Logic 3 3 Proof Systems for Propositional Logic 12 4 Ordered Binary Decision Diagrams 19 5 First-order Logic 22 6 Formal Reasoning in...
Foundations of Computer (2002)
Science Computer Science, Lawrence C Paulson, Copyright Lawrence, C. Paulson
level: names for dates over a certain range Concrete level: typically 6 characters: YYMMDD Date crises caused by INADEQUATE internal formats: .
Tool Support for Logics of Programs (2002)
Machine Several large studies use inductive definitions. Ltzbeyer, Sandner and Nipkow [17, 24] have proved several properties relating the operational and denotational semantics of Winskel's toy...
The reflection theorem: A study in meta-theoretic reasoning (2002)
Abstract. The reflection theorem has been proved using Isabelle/ZF. This theorem cannot be expressed in ZF, and its proof requires reasoning at the meta-level. There is a particularly elegant proof...
The verification of an industrial payment protocol (2002)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. When the customer makes a...
Program composition in Isabelle/UNITY (2002)
Sidi O. Ehmety, Lawrence C. Paulson
We describe the mechanization of recent examples of compositional reasoning, due to Charpentier and Chandy [4]. The examples illustrate a new theory for composition proposed by Chandy and Sanders [2,...
The Verification of an Industrial Payment Protocol (2002)
The Set Purchase, Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. When the customer makes a...
Program Composition in Isabelle/UNITY (2002)
Sidi O. Ehmety, Lawrence C. Paulson
We describe the mechanization of recent examples of compositional reasoning, due to Charpentier and Chandy [4]. The examples illustrate a new theory for composition proposed by Chandy and Sanders [2,...
Program composition in Isabelle/UNITY (2002)
Sidi O. Ehmety, Lawrence C. Paulson
We describe the mechanization of recent examples of compositional reasoning, due to Charpentier and Chandy [4]. The examples illustrate a new theory for composition proposed by Chandy and Sanders [2,...
The reflection theorem: A study in meta-theoretic reasoning (2002)
Abstract. The reflection theorem has been proved using Isabelle/ZF. This theorem cannot be expressed in ZF, and its proof requires reasoning at the meta-level. There is a particularly elegant proof...
Soundness — we can trust the result Transparency — we can follow the reasoning
Representing component states in higher-order logic (2001)
Sidi O. Ehmety, Lawrence C. Paulson
Abstract. Component states can be formalized in higher-order logic as (1) functions from variables to values and (2) records, among other possibilities. Variable-to-value maps are natural, but they...
Mechanical Proofs about a Non-Repudiation Protocol (2001)
Giampaolo Bella, Lawrence C Paulson
Abstract. A non-repudiation protocol of Zhou and Gollmann [18] has been mechanically verified. A non-repudiation protocol gives each party evidence that the other party indeed participated, evidence...
Verifying the SET purchase protocols (2001)
Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci
The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to guarantee the authenticity of e-commerce transactions and the...
SET Cardholder Registration: The Secrecy Proofs (2001)
Security protocols aim to protect the honest users of a network from the dishonest ones. Asymmetric (public key) cryptography is valuable, though it is normally used in conjunction with symmetric...
Representing Component States in Higher-Order Logic (2001)
Sidi O. Ehmety, Lawrence C. Paulson
Component states can be formalized in higher-order logic as (1) functions from variables to values and (2) records, among other possibilities.
Verifying the SET purchase protocols (2001)
Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
Abstract. SET (Secure Electronic Transaction) is a suite of protocols proposed by a consortium of credit card companies and software corporations to secure ecommerce transactions. The Purchase part...
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol (2001)
The Yahalom protocol is one of those analyzed by Burrows et al. [5]. Based upon their analysis, they have proposed modifications to make the protocol easier to understand and to analyze. Both...
Mechanical Proofs about a Non-Repudiation Protocol (2001)
Giampaolo Bella, Lawrence C Paulson
Abstract. A non-repudiation protocol of Zhou and Gollmann [18] has been mechanically verified. A non-repudiation protocol gives each party evidence that the other party indeed participated, evidence...
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol (2001)
The Yahalom protocol is one of those analyzed by Burrows et al. [5]. Based upon their analysis, they have proposed modifications to make the protocol easier to understand and to analyze. Both...
SET Cardholder Registration: The Secrecy Proofs (2001)
Security protocols aim to protect the honest users of a network from the dishonest ones. Asymmetric (public key) cryptography is valuable, though it is normally used in conjunction with symmetric...
Representing component states in higher-order logic (2001)
Sidi O. Ehmety, Lawrence C. Paulson
Abstract. Component states can be formalized in higher-order logic as (1) functions from variables to values and (2) records, among other possibilities. Variable-to-value maps are natural, but they...
Representing component states in higher-order logic (2001)
Sidi O. Ehmety, Lawrence C. Paulson
Abstract. Component states can be formalized in higher-order logic as (1) functions from variables to values and (2) records, among other possibilities. Variable-to-value maps are natural, but they...
Mechanical proofs about a non-repudiation protocol (2001)
Giampaolo Bella, Lawrence C Paulson
Abstract. A non-repudiation protocol of Zhou and Gollmann [18] has been mechanically verified. A non-repudiation protocol gives each party evidence that the other party indeed participated, evidence...
SET Cardholder Registration: The Secrecy Proofs (2001)
Security protocols aim to protect the honest users of a network from the dishonest ones. Asymmetric (public key) cryptography is valuable, though it is normally used in conjunction with symmetric...
Verifying the SET purchase protocols (2001)
Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
Abstract. SET (Secure Electronic Transaction) is a suite of protocols proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. The Purchase part...
Mechanizing a theory of program composition for UNITY (2000)
Lawrence C. Paulson, Lawrence C. Paulson
Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which...
A fixedpoint approach to (co)inductive and (co)datatype definitions (2000)
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as “strictly positive, ” the approach lets definitions involve any operators that have...
Foundations of Functional Programming (2000)
ions are compiled to the closure command, which will push a closure onto the Stack. The closure will include the current Environment and will hold M as a list of commands, from compilation: [[ #x .M...
Formal Verification of Cardholder Registration in SET (2000)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
. The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas...
Formal verification of cardholder registration in SET (2000)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson, Piero Tramontano
Abstract. The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic...
Mechanizing a theory of program composition for UNITY (2000)
Lawrence C. Paulson, Lawrence C. Paulson
Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which...
A fixedpoint approach to (co)inductive and (co)datatype definitions (2000)
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as “strictly positive, ” the approach lets definitions involve any operators that have...
Mechanizing UNITY in Isabelle (2000)
UNITY is an abstract formalism for proving properties of concurrent systems, which typically are expressed using guarded assignments [Chandy and Misra 1988]. UNITY has been mechanized in higher-order...
Making sense of specifications: the formalization of set (extended abstract (2000)
Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson
The last ten years, since the seminal work on the BAN logic [6], have seen the rapid development of formal methods for the analysis of security protocols. But security protocols have also developed...
A fixedpoint approach to (co)inductive and (co)datatype definitions (2000)
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as “strictly positive, ” the approach lets definitions involve any operators that have...
A fixedpoint approach to (co)inductive and (co)datatype definitions (2000)
This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as “strictly positive, ” the approach lets definitions involve any operators that have...
A generic tableau prover and its integration with Isabelle (1999)
Abstract: A generic tableau prover has been implemented and integrated with Isabelle [Paulson, 1994]. Compared with classical rst-order logic provers, it has numerous extensions that allow it to...
A generic tableau prover and its integration with Isabelle (1999)
A generic tableau prover has been implemented and integrated with Isabelle [14]. It is based on leantap [3] but is much more complicated, with numerous modifications to allow it to reason with any...
A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle HOL (1999)
Florian Kammüller, Lawrence C. Paulson
Abstract. The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a non-trivial combinatorial identity. The mathematical proof...
The relative consistency of the axiom of choice -- mechanized using Isabelle/ZF (1999)
The proof of the relative consistency of the axiom of choice has been mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on...
Final Coalgebras as Greatest Fixed Points in ZF Set Theory (1999)
Lawrence C. Paulson, L. C. Paulson
this paper is not to change the axiom system but to adopt new definitions of ordered pairs, functions, and derived concepts such as Cartesian products. Under the new definitions, the stream...
Inductive analysis of the Internet protocol TLS (1999)
Internet browsers use security protocols to protect confidential messages. An inductive analysis of TLS (a descendant of SSL 3.0) has been performed using the theorem prover Isabelle. Proofs are...
Locales: A sectioning concept for Isabelle (1999)
Florian Kammuller, Markus Wenzel, Lawrence C. Paulson
Abstract. Locales are a means to define local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are...
Clemens Ballarin, Fakultat Fur Informatik, Lawrence C. Paulson
. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports...
Clemens Ballarin, Lawrence C. Paulson
. The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports...
Locales: A Sectioning Concept for Isabelle (1999)
Florian Kammüller, Markus Wenzel, Lawrence C. Paulson
. Locales are a means to define local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that...
Mechanizing UNITY in Isabelle (1999)
ing with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works, requires prior specific permission...
Locales: A sectioning concept for Isabelle (1999)
Florian Kammüller, Markus Wenzel, Lawrence C. Paulson
Abstract. Locales are a means to define local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are...
A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle HOL (1999)
Florian Kammüller, Lawrence C. Paulson
Abstract. The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a non-trivial combinatorial identity. The mathematical proof...
A generic tableau prover and its integration with Isabelle (1999)
Abstract: A generic tableau prover has been implemented and integrated with Isabelle (Paulson, 1994). Compared with classical first-order logic provers, it has numerous extensions that allow it to...
Final Coalgebras as Greatest Fixed Points in ZF Set Theory ∗ (1999)
Lawrence C. Paulson, L. C. Paulson
A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition of function...
A Generic Tableau Prover (1999)
And Its Integration, Lawrence C. Paulson
A generic tableau prover has been implemented and integrated with Isabelle (Paulson, 1994). Compared with classical first-order logic provers, it has numerous extensions that allow it to reason with...
A generic tableau prover and its integration with Isabelle (1999)
Abstract: A generic tableau prover has been implemented and integrated with Isabelle (Paulson, 1994). Compared with classical first-order logic provers, it has numerous extensions that allow it to...
Final coalgebras as greatest fixed points (1999)
A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition of function...
A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle HOL (1999)
Florian Kammüller, Lawrence C. Paulson
Abstract. The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a non-trivial combinatorial identity. The mathematical proof...
Proving security protocols correct (1999)
Security protocols use cryptography to set up private communication channels on an insecure network. Many protocols contain flaws, and because security goals are seldom specified in detail, we cannot...
Gödel [3] published a monograph in 1940 proving a highly significant theorem, namely that the axiom of choice (AC) and the generalized continuum hypothesis (GCH) are consistent with respect to the...
Jacques D. Fleuriot, Lawrence C. Paulson
The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia's reasoning is resolutely geometric in nature but...
Jacques D. Fleuriot, Lawrence C. Paulson
Abstract. The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia’s reasoning is resolutely geometric in nature...
Kerberos version IV: Inductive analysis of the secrecy goals (1998)
Giampaolo Bella, Lawrence C Paulson
Abstract. An operational model of crypto-protocols is tailored to the detailed analysis of the secrecy goals accomplished by Kerberos Version IV. The model is faithful to the specication of the...
Jacques D. Fleuriot, Lawrence C. Paulson
Abstract. The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia’s reasoning is resolutely geometric in nature...
A Formal Proof of Sylow's Theorem - An Experiment in Abstract Algebra . . . (1998)
Florian Kammüller, Lawrence C. Paulson
Algebra with Isabelle HOL Florian Kammuller and Lawrence C. Paulson Computer Laboratory, University of Cambridge, UK November 11, Abstract The theorem of Sylow is proved in Isabelle HOL. We follow...
The inductive approach to verifying cryptographic protocols (1998)
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state...
Set Theory for Verification: I. From Foundations to Functions (1998)
A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting...
Should Your Specification Language Be Typed? (1998)
Leslie Lamport, Lawrence C. Paulson
Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language...
Kerberos Version IV: Inductive Analysis of the Secrecy Goals (1998)
Giampaolo Bella, Lawrence C Paulson
An operational model of crypto-protocols is tailored to the detailed analysis of the secrecy goals accomplished by Kerberos Version IV. The model is faithful to the specification of the protocol...
Mechanising BAN Kerberos by the Inductive Method (1998)
Mechanising Ban Kerberos, Giampaolo Bella, Lawrence C Paulson
The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of expired...
Mechanising BAN Kerberos by the Inductive Method (1998)
Mechanising Ban Kerberos, Giampaolo Bella, Lawrence C Paulson
. The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of expired...
Jacques D. Fleuriot, Lawrence C. Paulson
. The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia's reasoning is resolutely geometric in nature but...
Kerberos Version IV: Inductive Analysis of the Secrecy Goals (1998)
Giampaolo Bella, Lawrence C Paulson
. An operational model of crypto-protocols is tailored to the detailed analysis of the secrecy goals accomplished by Kerberos Version IV. The model is faithful to the specification of the protocol...
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol (1998)
The Yahalom protocol is one of those analyzed by Burrows et al. [5]. Based upon their analysis, they have proposed modifications to make the protocol easier to understand and to analyze. Both...
The Inductive Approach to Verifying Cryptographic Protocols (1998)
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state...
A Generic Tableau Prover and its Integration with Isabelle (1998)
A generic tableau prover has been implemented and integrated with Isabelle [14]. It is based on leantap [3] but is much more complicated, with numerous modifications to allow it to reason with any...
Mechanising BAN Kerberos by the Inductive Method (1998)
Giampaolo Bella, Lawrence C Paulson
Abstract. The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of...
The inductive approach to verifying cryptographic protocols (1998)
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state...
Jacques D. Fleuriot, Lawrence C. Paulson
Abstract. The approach previously used to mechanise lemmas and Kepler's Law of Equal Areas from Newton's Principia [13] is here used to mechanically reproduce the famous Propositio...
The inductive approach to verifying cryptographic protocols (1998)
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state...
Jacques D. Fleuriot, Lawrence C. Paulson
Abstract. The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia’s reasoning is resolutely geometric in nature...
Kerberos version IV: Inductive analysis of the secrecy goals (1998)
Giampaolo Bella, Lawrence C Paulson
Abstract. An operational model of crypto-protocols is tailored to the detailed analysis of the secrecy goals accomplished by Kerberos Version IV. The model is faithful to the specification of the...
The inductive approach to verifying cryptographic protocols (1998)
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state...
Jacques D. Fleuriot, Lawrence C. Paulson
Abstract. The approach previously used to mechanise lemmas and Kepler's Law of Equal Areas from Newton's Principia [13] is here used to mechanically reproduce the famous Propositio...
Mechanising BAN Kerberos by the Inductive Method (1998)
Giampaolo Bella, Lawrence C Paulson
Abstract. The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of...
Jacques D. Fleuriot, Lawrence C. Paulson
Abstract. The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia’s reasoning is resolutely geometric in nature...
Kerberos version IV: Inductive analysis of the secrecy goals (1998)
Giampaolo Bella, Lawrence C Paulson
Abstract. An operational model of crypto-protocols is tailored to the detailed analysis of the secrecy goals accomplished by Kerberos Version IV. The model is faithful to the specification of the...
Using Isabelle to Prove Properties of the Kerberos Authentication System (1997)
Giampaolo Bella, Lawrence C Paulson
The Inductive method, previously used to analyse classical, noncebased cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete...
Mechanizing coinduction and corecursion in higher-order logic (1997)
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists;...
Generic Automatic Proof Tools (1997)
This article explores a synthesis between two distinct traditions in automated reasoning: resolution and interaction. In particular it discusses Isabelle, an interactive theorem prover based upon a...
Using Isabelle to Prove Properties of the Kerberos Authentication System (1997)
Giampaolo Bella, Lawrence C Paulson
The Inductive method, previously used to analyse classical, nonce-based cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete...
Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys (1997)
The inductive approach to verifying security protocols, previously applied to shared-key encryption [8], is here applied to the public key version of the Needham-Schroeder protocol. As before,...
Mechanized Proofs for a Recursive Authentication Protocol (1997)
A novel protocol has been formally analyzed using the prover Isabelle/HOL, following the inductive approach described in earlier work [11]. There is no limit on the length of a run, the nesting of...
Computer Science Tripos, Lawrence C Paulson
specification. Describe their functions and constraints ffl Interface design. Precisely define how they fit together ffl Component design. Recursively design each block Source: Sommerville, Software...
specification. Describe their functions and constraints ffl Interface design. Precisely define how they fit together ffl Component design. Recursively design each block Source: Sommerville, Software...
Using Isabelle to Prove Properties of the Kerberos Authentication System (1997)
Giampaolo Bella, Lawrence C. Paulson
The Inductive method, previously used to analyse classical, noncebased cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete...
Relations Between Secrets: Two Formal Analyses of the Yahalom Protocol (1997)
Lawrence Paulson Computer, Lawrence C. Paulson
The Yahalom protocol is one of those analyzed by Burrows et al. [5]. Based upon their analysis, they have proposed modifications to make the protocol easier to understand and to analyze. Both...
Proving Properties of Security Protocols by Induction (1997)
Informal justifications of security protocols involve arguing backwards that various events are impossible. Inductive definitions can make such arguments rigorous. The resulting proofs are...
Isabelle's Object-Logics (1997)
Lawrence C. Paulson, Tobias Nipkow, Markus Wenzel
this document. FOL is many-sorted first-order logic with natural deduction. It comes in both constructive and classical versions.
Using Isabelle to Prove Properties of the Kerberos Authentication System (1997)
Giampaolo Bella, Lawrence C Paulson
The Inductive method, previously used to analyse classical, noncebased cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete...
Proving properties of security protocols by induction (1997)
Informal justifications of security protocols involve arguing backwards that various events are impossible. Inductive definitions can make such arguments rigorous. The resulting proofs are...
Mechanized proofs for a recursive authentication protocol (1997)
A novel protocol has been formally analyzed using the prover Isabelle/HOL, following the inductive approach described in earlier work [10]. There is no limit on the length of a run, the nesting of...
Mechanized proofs of security protocols: Needham-Schroeder with public keys (1997)
The inductive approach to verifying security protocols, previously applied to shared-key encryption [8], is here applied to the public key version of the Needham-Schroeder protocol. As before,...
Mechanizing Coinduction and Corecursion in Higher-order Logic (1997)
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists:...
Using Isabelle to Prove Properties of the Kerberos Authentication System (1997)
Giampaolo Bella, Lawrence C Paulson
The Inductive method, previously used to analyse classical, noncebased cryptographic protocols, is here tailored to formalise Kerberos, a real-world, timestamp-based protocol. A complete...
Applications of Proof Theory to Isabelle (1996)
Isabelle [3, 4] is a generic theorem prover. It suppports interactive proof in several formal systems, including first-order logic (intuitionistic and classical), higher-order logic, Martin-Löf type...
A Simple Formalization and Proof for the Mutilated Chess Board (1996)
Lawrence C. Paulson, Computer Laboratory
The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are...
A Simple Formalization and Proof for the Mutilated Chess Board (1996)
The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are...
A Simple Formalization and Proof for the Mutilated Chess Board (1996)
The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are...
Mechanizing set theory: cardinal arithmetic and the axiom of choice (1996)
Lawrence C. Paulson, Krzysztof Grabczewski
Abstract. Fairly deep results of Zermelo-Frænkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key...
Mechanizing Set Theory - Cardinal Arithmetic and the Axiom of Choice (1996)
Lawrence C. Paulson, Krzysztof Grabczewski
. Fairly deep results of Zermelo-Fraenkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result...
Tool Support for Logics of Programs (1996)
Proof tools must be well designed if they...
Foundations of Functional Programming (1996)
ions are compiled to the closure command, which will push a closure onto the Stack. The closure will include the current Environment and will hold M as a list of commands, from compilation: [[x:M ]]...
Tool Support for Logics of Programs (1996)
International Summer, School Marktoberdorf, Lawrence C. Paulson
Machine Several large studies use inductive deønitions. L#tzbeyer, Sandner and Nipkow [17, 25] have proved several properties relating the operational and denotational semantics of Winskel's...
A Simple Formalization and Proof for the (1996)
Mutilated Chess Board, Lawrence C. Paulson, Computer Laboratory
The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are...
1. What Should Proof Tools Do For Us?................................ 1 (1996)
cryptographic protocols Summary. Proof tools must be well designed if they are to be more effective than pen and paper. Isabelle supports a range of formalisms, two of which are described...
A Simple Formalization and Proof for the Mutilated Chess Board (1996)
Lawrence C. Paulson, Computer Laboratory
The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are...
Mechanizing set theory: cardinal arithmetic and the axiom of choice (1996)
Lawrence C. Paulson, Krzysztof Grabczewski
(Received.....; Accepted in final form.....) Abstract. Fairly deep results of Zermelo-Fraenkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal...
Mechanizing set theory: cardinal arithmetic and the axiom of choice (1996)
Lawrence C. Paulson, Krzysztof Grabczewski
Abstract. Fairly deep results of Zermelo-Frænkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key...
Mechanizing set theory: Cardinal arithmetic and the axiom of choice (1996)
Lawrence C. Paulson, Krzysztof Grabczewski
Abstract. Fairly deep results of Zermelo-Frænkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key...
Applications of Proof Theory to Isabelle (1996)
Isabelle [3, 4] is a generic theorem prover. It suppports interactive proof in several formal systems, including first-order logic (intuitionistic and classical), higher-order logic, Martin-Löf type...
Set theory for verification: II. induction and recursion (1995)
Abstract. A theory of recursive definitions has been mechanized in Isabelle’s Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for...
Set theory for verification: II. induction and recursion (1995)
Abstract. A theory of recursive definitions has been mechanized in Isabelle’s Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for...
Set Theory for Verification: II - Induction and Recursion (1995)
. A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use...
Set Theory for Verification: II - Induction and Recursion (1995)
. A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use...
Foundations of Functional Programming (1995)
ions are compiled to the closure command, which will push a closure onto the Stack. The closure will include the current Environment and will hold M as a list of commands, from compilation: [[x:M ]]...
A concrete final coalgebra theorem for ZF set theory (1995)
Abstract. A special final coalgebra theorem, in the style of Aczel’s [2], is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition...
Set theory for verification: II. induction and recursion (1995)
Abstract. A theory of recursive definitions has been mechanized in Isabelle’s Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for...
Set theory for verification: II. Induction and recursion (1995)
Abstract. A theory of recursive definitions has been mechanized in Isabelle’s Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for...
Isabelle: A generic theorem prover (1994)
Isabelle [28, 30] is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations...
A Concrete Final Coalgebra Theorem for ZF Set Theory (1994)
. A special final coalgebra theorem, in the style of Aczel's [2], is proved within standard Zermelo-Fraenkel set theory. Aczel's AntiFoundation Axiom is replaced by a variant definition of...
Set theory for verification: I. From foundations to functions (1993)
A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting...
Set theory for verification: I. From foundations to functions (1993)
A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting...
Tobias Nipkow And, Tobias Nipkow, Lawrence C. Paulson
ormula P is true"; we usually distinguish object-level formulae (form) from meta-level formulae (prop). In practice the brackets can be dropped; parser and pretty-printer take care of such...
Tobias Nipkow, Lawrence C. Paulson
Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle’s meta-logic. Proofs are performed by a generalization of resolution, using...
Tobias Nipkow, Lawrence C. Paulson
Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle’s meta-logic. Proofs are performed by a generalization of resolution, using...
Logic programming, functional programming, and inductive definitions (1991)
Lawrence C. Paulson, Lawrence C. Paulson, Andrew W. Smith, Andrew W. Smith
Isabelle tutorial and user's manual (1990)
Lawrence C. Paulson, Copyright Lawrence, C. Paulson, Tobias Nipkow, Tobias Nipkow
This manual describes how to use the theorem prover Isabelle. For beginners, it explains how to perform simple single-step proofs in the built-in logics. These include first-order logic, a classical...
Isabelle: The next seven hundred theorem provers (1988)
Isabelle [2] is a theorem prover for a large class of logics. The object-logics are formalized within Isabelle’s meta-logic, which is intuitionistic higher-order logic with implication, universal...
Isabelle: The next seven hundred theorem provers (1988)
Isabelle [2] is a theorem prover for a large class of logics. The object-logics are formalized within Isabelle’s meta-logic, which is intuitionistic higher-order logic with implication, universal...
Natural deduction as higher-order resolution (1986)
An interactive theorem prover, Isabelle, is under development. In LCF, each inference rule is represented by one function for forwards proof and another (a tactic) for backwards proof. In Isabelle,...
Proving termination of normalization functions for conditional expressions (1986)
Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form [1]. It is difficult to prove that this function terminates on all inputs. Three termination...
Constructing recursion operators in intuitionistic type theory (1986)
Martin-Löf’s Intuitionistic Theory of Types is becoming popular for formal reasoning about computer programs. To handle recursion schemes other than primitive recursion, a theory of well-founded...
Verifying the unification algorithm in lcf (1985)
Abstract. Manna and Waldinger’s theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented in detail,...
The Reflection Theorem: A Study in Meta-Theoretic Reasoning
The reflection theorem has been proved using Isabelle/ZF.