diff --git a/CHANGES b/CHANGES --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,7 @@ +* 0.5.0.0 + - implemented proof generation for injective agreement + - fixed bug in unification of inverse-key constructors + * 0.4.1.0 Bugfixes and dropped export of library - widen 'pretty' dependency - update package description @@ -35,6 +39,6 @@ - Changed lexer to also recognize `!' * 0.3.0 First public version - + Aligned with paper submission for CCS'11: Provably repairing the ISO-9798 authentication protocols. diff --git a/README b/README deleted file mode 100644 --- a/README +++ /dev/null @@ -1,167 +0,0 @@ -====================================================================== -README for the scyther-proof security protocol verification tool -====================================================================== - -Author: Simon Meier - -Creation Date: 13/05/2011 -Updated: 02/04/2012 - - -1. Introduction -=============== - - Every distribution of the scyther-proof tool contains a copy of the - Isabelle/HOL theories formalizing its verification theory and a copy of the - protocol models that were verified using scyther-proof. In particular, these - examples include models for all of our repaired versions of the protocols - from the ISO/IEC-9798 authentication standard. (In the source distribution - of scyther-proof they can be found at 'data/examples/iso9798'.) - - In the following sections, we give step by step instructions to get the - whole system working and we explain the usage of our tools and provide - further information (e.g., building documentation). - - -2. Installation instructions -============================ - -2.1 Installing scyther-proof ----------------------------- - - You need a working Haskell environment that provides a version of GHC from - 7.0.x to 7.4.x and the 'cabal install' tool. The simplest way to get such an - environment is to download and install the Haskell Platform package for your - OS. - - http://hackage.haskell.org/platform/ - - Then call - - cabal install - - in the root directory of this source code package. This will use the - Haskell's deployment tool 'cabal-install' to download all missing libraries - from Hackage, the central Haskell library repository and install the - 'scyther-proof' executable in the default installation location of - cabal-install. The installation location is printed at the end of the build - process. - - Call - - scyther-proof - - without any arguments to get an overview of the arguments supported and the - paths to the examples and the Isabelle/HOL theories. - - -3.2 Installing the Isabelle/HOL theories ----------------------------------------- - - Download and install full Isabelle2009-1 according to the installation - instructions at - - http://isabelle.in.tum.de/website-Isabelle2009-1/download_x86-linux.html - - The first time you call 'scyther-proof' with the '--isabelle' flag it will - build the logic image of the Isabelle/HOL theories formalizing the security - protocol verification theory underlying scyther-proof. - - For enabling interactive processing of theory files based using our - extensions to Isabelle's ISAR proof language use one of the following two - variants. - - Variant a: Brute Force - ---------------------- - - Overwrite the standard Emacs keywords file - - $ISABELLE_HOME/etc/isar-keywords.el - - with the Emacs keywords file provided with the ESPL distribution. - - $SCYTHER_PROOF_HOME/isabelle/src/isar-keywords.el - - This is needed in order to make the new ISAR keywords "role", - "protocol", "sources", and "prefix_close" available in the Emacs - frontend. - - - Variant b: Elegance - ------------------- - - A more elegant way is to copy the keywords file provided with our - distribution to - - $ISABELLE_HOME/etc/isar-keywords-ESPL.el - - and start Isabelle using the -k switch as follows. - - isabelle emacs -k ESPL - - - -3. Usage -======== - - -3.1 scyther-proof ------------- - - - Usage Example - ------------- - - You can now execute the 'scyther-proof' binary without any arguments to get a - list of the available flags. A simple example usage is (assuming - 'scyther-proof' is in the PATH). - - scyther-proof $EXAMPLE_DIR/classic/NS_Public.spthy --shortest - - This will parse the NSL protocol modeled in the 'nsl.spthy' file and output - all specified security properties together with the proof with the fewest - number of chain rule applications to stdout. - - In order to generate an Isabelle proof script two additional options need to - be added - - scyther-proof $EXAMPLE_DIR/classic/NS_Public.spthy --shortest --output=nsl_cert.thy --ASCII - - The first one specifies the output file and the second one instructs - scyther-proof to use Isabelle's ASCII notation as the output format. - - - To build the source code documentation you can use the call - - cabal configure; cabal haddock - - which will use cabal-install and Haskell's source code documentation tool - 'haddock' to build the source code documentation. The location of this - documentation is again output on the command line. - - -3.2 The Isabelle/HOL theories ------------------------------ - - In the directory output by scyther-proof, load the Tutorial on interactive - proof construction using the following commands - - cd /src - isabelle emacs Tutorial.thy - - or if you've chosen the elegant variant - - isabelle emacs -k ESPL Tutorial.thy - - Note that in many case the easiest way to start with constructing - machine-checked proofs interactively is to use a proof script generated by - scyther-proof. - - -*** -* Happy Proving :-) -* -* In case of questions do not hesistate to contact me at -* simon.meier@inf.ethz.ch -*** - diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,165 @@ +README: The scyther-proof security protocol verification tool +============================================================= + +Author: Simon Meier + +Creation Date: 13/05/2011 -- Last Updated: 28/06/2012 + + +1. Introduction +=============== + + Every distribution of the scyther-proof tool contains a copy of the + Isabelle/HOL theories formalizing its verification theory and a copy of the + protocol models that were verified using scyther-proof. In particular, these + examples include models for all of our repaired versions of the protocols + from the ISO/IEC-9798 authentication standard. (In the source distribution + of scyther-proof they can be found at `data/examples/iso9798`.) + + In the following sections, we give step by step instructions to get the + whole system working and we explain the usage of our tools and provide + further information (e.g., building documentation). + + +2. Installation instructions +============================ + +2.1 Installing scyther-proof +---------------------------- + + You need a working Haskell environment that provides a version of GHC from + 7.0.x to 7.4.x and the 'cabal install' tool. The simplest way to get such an + environment is to download and install the Haskell Platform package for your + OS. + + http://hackage.haskell.org/platform/ + + Then call + + cabal install + + in the root directory of this source code package. This will use the + Haskell's deployment tool `cabal-install` to download all missing libraries + from Hackage, the central Haskell library repository and install the + `scyther-proof` executable in the default installation location of + cabal-install. The installation location is printed at the end of the build + process. + + Call + + scyther-proof + + without any arguments to get an overview of the arguments supported and the + paths to the examples and the Isabelle/HOL theories. + + +2.2 Installing the Isabelle/HOL theories +---------------------------------------- + +Download and install full Isabelle2009-1 according to the installation +instructions at + + http://isabelle.in.tum.de/website-Isabelle2009-1/download_x86-linux.html + +The first time you call `scyther-proof` with the `--isabelle` flag it will +build the logic image of the Isabelle/HOL theories formalizing the security +protocol verification theory underlying `scyther-proof`. + +For enabling interactive processing of theory files based using our +extensions to Isabelle's ISAR proof language use one of the following two +variants. + +Variant a: Brute Force +---------------------- + +Overwrite the standard Emacs keywords file + + $ISABELLE_HOME/etc/isar-keywords.el + +with the Emacs keywords file provided with the ESPL distribution. + + $SCYTHER_PROOF_HOME/isabelle/src/isar-keywords.el + +This is needed in order to make the new ISAR keywords `role`, +`protocol`, `sources`, and `prefix_close` available in the Emacs +frontend. + + +Variant b: Elegance +------------------- + +A more elegant way is to copy the keywords file provided with our +distribution to + + $ISABELLE_HOME/etc/isar-keywords-ESPL.el + +and start Isabelle using the -k switch as follows. + + isabelle emacs -k ESPL + + + +3. Usage +======== + + +3.1 scyther-proof +------------ + + + Usage Example + ------------- + + You can now execute the 'scyther-proof' binary without any arguments to get a + list of the available flags. A simple example usage is (assuming + 'scyther-proof' is in the PATH). + + scyther-proof $EXAMPLE_DIR/classic/NS_Public.spthy --shortest + + This will parse the NSL protocol modeled in the 'nsl.spthy' file and output + all specified security properties together with the proof with the fewest + number of chain rule applications to stdout. + + In order to generate an Isabelle proof script two additional options need to + be added + + scyther-proof $EXAMPLE_DIR/classic/NS_Public.spthy --shortest --output=nsl_cert.thy --ASCII + + The first one specifies the output file and the second one instructs + scyther-proof to use Isabelle's ASCII notation as the output format. + + + To build the source code documentation you can use the call + + cabal configure; cabal haddock + + which will use cabal-install and Haskell's source code documentation tool + 'haddock' to build the source code documentation. The location of this + documentation is again output on the command line. + + +3.2 The Isabelle/HOL theories +----------------------------- + + In the directory output by scyther-proof, load the Tutorial on interactive + proof construction using the following commands + + cd /src + isabelle emacs Tutorial.thy + + or if you've chosen the elegant variant + + isabelle emacs -k ESPL Tutorial.thy + + Note that in many case the easiest way to start with constructing + machine-checked proofs interactively is to use a proof script generated by + scyther-proof. + + +*** + +`Happy Proving :)` + +In case of questions do not hesistate to contact me at +iridcode@gmail.com. + diff --git a/data/examples/iso9798/isoiec-9798-2-bdkey.spthy b/data/examples/iso9798/isoiec-9798-2-bdkey.spthy --- a/data/examples/iso9798/isoiec-9798-2-bdkey.spthy +++ b/data/examples/iso9798/isoiec-9798-2-bdkey.spthy @@ -1,4 +1,4 @@ -/* +/* * Modeled from ISO/IEC 9798-2 * Modeler: Cas Cremers, Dec. 2010 * Ported to scyther-proof: Simon Meier, Feb. 2011 @@ -33,8 +33,10 @@ 1. A -> B: A, B, Text2, {'isoiec_9798_2_1_enc_1', TNA, B, Text1 }k[A,B] } +// Here we dont get any injective agreement, as there could be two B thread +// receiving the same message from one A. property (of isoiec_9798_2_1_bdkey) - B_non_injective_agreement: + B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) @@ -60,8 +62,8 @@ } property (of isoiec_9798_2_2_bdkey) - B_non_injective_agreement: - niagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B}) @@ -89,11 +91,15 @@ 2. B -> A: B, A, Text4, {'isoiec_9798_2_3_enc_2', TNB, A, Text3 }k[B,A] } +// NOTE: We do not get injective agreement here, in neither direction. The +// problem is the same as in isoiec_9798_2_1_bdkey. However, we are missing +// the opportunity to strengthen the property for A, as we could just embed +// TNA in the message sent from B. properties (of isoiec_9798_2_3_bdkey) - A_non_injective_agreement: + A_non_injective_agreement: niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {A, B}) - B_non_injective_agreement: + B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) @@ -123,11 +129,11 @@ } properties (of isoiec_9798_2_4_bdkey) - A_non_injective_agreement: - niagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B}) + A_injective_agreement: + iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B}) - B_non_injective_agreement: - niagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B}) /****************************************************************************** @@ -179,15 +185,20 @@ // (a) we also verify agreement on the freshness data TNa, TNb // (b) we also verify agreement with the trusted third party // - A_non_injective_agreement_B: - niagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) + A_injective_agreement_B: + iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) - B_non_injective_agreement_A: + // Injective agreement does not hold. See + // isoiec_9798_2_5_special_TTP_bdkey for more information. + B_non_injective_agreement_A: niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P}) - A_non_injective_agreement_P: - niagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) - B_non_injective_agreement_P: + A_injective_agreement_P: + iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) + + // Injective agreement does not hold. See + // isoiec_9798_2_5_special_TTP_bdkey for more information. + B_non_injective_agreement_P: niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P}) @@ -221,12 +232,12 @@ -> A: P, A, Text5, {'isoiec_9798_2_6_enc_3_1', Ra, Kab, A, B, Text4}k[A,P] , TokenPA_for_B - text_4. -> A: Text6, Text7 + text_4. -> A: Text6, Text7 4. A -> : A, B, Text7, P, TokenPA_for_B , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab -> B: A, B, Text7, P, {'isoiec_9798_2_6_enc_3_2', Rb, Kab, A, B, Text3}k[B,P] , {'isoiec_9798_2_6_enc_4', Rpa, Rb, Text6}Kab - + text_5. -> B: Text8, Text9 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_enc_5', Rb, Rpa, Text8}Kab } @@ -237,20 +248,20 @@ B_secret_Kab: secret(B, 4, Kab, {A, B, P}) // Agreement properties strengthened with respect to Cas Cremers' models: - // (a) we also verify agreement on the freshness data + // (a) we also verify agreement on the freshness data // (b) we also verify agreement with the trusted third party // - A_non_injective_agreement_B: - niagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) + A_injective_agreement_B: + iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) - B_non_injective_agreement_A: - niagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) + B_injective_agreement_A: + iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) - A_non_injective_agreement_P: - niagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) + A_injective_agreement_P: + iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) - B_non_injective_agreement_P: - niagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) + B_injective_agreement_P: + iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) /****************************************************************************** @@ -310,22 +321,28 @@ // Agreement properties strengthened with respect to Cas Cremers' models: // (a) we also verify agreement on the freshness data TNa, TNb // (b) we also verify agreement with the trusted third party - // - // Note: If no axiom dependency for a property below, then it can be proven - // without the axiom. - - A_non_injective_agreement_B: - niagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) + // + // Note: If no axiom dependency is noted for a property below, then it can + // be proven without the axiom. - // depends on 'different_actors_A_P' - B_non_injective_agreement_A: + A_injective_agreement_B: + iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) + + // Depends on 'different_actors_A_P' + // + // NO injective agreement can be proven. There may be several B-threads + // communicating with the same A-thread! Checking the 'TNb' timestamp in + // later steps could be used to remove this problem, up to the clock + // resolution. + B_non_injective_agreement_A: niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P}) // depends on 'different_actors_A_P' - A_non_injective_agreement_P: - niagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) + A_injective_agreement_P: + iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) - B_non_injective_agreement_P: + // No injective agreement, as the TTP does not receive any message from 'B'. + B_non_injective_agreement_P: niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P}) @@ -360,12 +377,12 @@ -> A: P, A, Text5, {'isoiec_9798_2_6_special_TTP_enc_3_1', Ra, Kab, B, Text4}k[A,P] , TokenPA_for_B - text_4. -> A: Text6, Text7 + text_4. -> A: Text6, Text7 4. A -> : A, B, Text7, P, TokenPA_for_B , {'isoiec_9798_2_6_special_TTP_enc_4', Rpa, Rb, Text6}Kab -> B: A, B, Text7, P, {'isoiec_9798_2_6_special_TTP_enc_3_2', Rb, Kab, A, Text3}k[B,P] , {'isoiec_9798_2_6_special_TTP_enc_4', Rpa, Rb, Text6}Kab - + text_5. -> B: Text8, Text9 5. B -> A: B, A, Text9, {'isoiec_9798_2_6_special_TTP_enc_5', Rb, Rpa, Text8}Kab } @@ -392,26 +409,26 @@ B_secret_Kab: secret(B, 4, Kab, {A, B, P}) // Agreement properties strengthened with respect to Cas Cremers' models: - // (a) we also verify agreement on the freshness data + // (a) we also verify agreement on the freshness data // (b) we also verify agreement with the trusted third party - // - // Note: If no axiom dependency for a property below, then it can be proven - // without the axiom. + // + // Note: If no axiom dependency is noted for a property below, then it can + // be proven without the axiom. // depends on 'different_actors_B_P' and 'different_actors_A_P' - A_non_injective_agreement_B: - niagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) + A_injective_agreement_B: + iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) // depends on 'different_actors_B_P' and 'different_actors_A_P' - B_non_injective_agreement_A: - niagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) + B_injective_agreement_A: + iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) // depends on 'different_actors_A_P - A_non_injective_agreement_P: - niagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) + A_injective_agreement_P: + iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) // depends on 'different_actors_B_P - B_non_injective_agreement_P: - niagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) + B_injective_agreement_P: + iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) end diff --git a/data/examples/iso9798/isoiec-9798-2-udkey.spthy b/data/examples/iso9798/isoiec-9798-2-udkey.spthy --- a/data/examples/iso9798/isoiec-9798-2-udkey.spthy +++ b/data/examples/iso9798/isoiec-9798-2-udkey.spthy @@ -31,6 +31,8 @@ 1. A -> B: A, B, Text2, {'isoiec_9798_2_1_enc_1', TNA, Text1 }k(A,B) } +// Here we dont get any injective agreement, as there could be two B thread +// receiving the same message from one A. property (of isoiec_9798_2_1_udkey) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) @@ -56,8 +58,8 @@ } property (of isoiec_9798_2_2_udkey) - B_non_injective_agreement: - niagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,RB,Text2] -> A_2[A,B,RB,Text2], {A, B}) @@ -83,6 +85,10 @@ 2. B -> A: B, A, Text4, {'isoiec_9798_2_3_enc_2', TNB, Text3 }k(B,A) } +// NOTE: We do not get injective agreement here, in neither direction. The +// problem is the same as in isoiec_9798_2_1_bdkey. However, we are missing +// the opportunity to strengthen the property for A, as we could just embed +// TNA in the message sent from B. properties (of isoiec_9798_2_3_udkey) A_non_injective_agreement: niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {A, B}) @@ -118,11 +124,11 @@ } properties (of isoiec_9798_2_4_udkey) - A_non_injective_agreement: - niagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B}) + A_injective_agreement: + iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A, B}) - B_non_injective_agreement: - niagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A, B}) /****************************************************************************** @@ -173,14 +179,22 @@ // (a) we also verify agreement on the freshness data TNa, TNb // (b) we also verify agreement with the trusted third party // - A_non_injective_agreement_B: - niagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) + A_injective_agreement_B: + iagree(A_4[A,B,P,Kab,TNa,Text5,TNb,Text7] -> B_4[A,B,P,Kab,TNa,Text5,TNb,Text7], {A, B, P}) + // Injectivity agreement does not hold. See + // + // NO injective agreement can be proven. There may be several B-threads + // communicating with the same A-thread! Checking the 'TNb' timestamp in + // later steps could be used to remove this problem, up to the clock + // resolution. B_non_injective_agreement_A: niagree(B_3[A,B,P,Kab,TNa,Text5] -> A_3[A,B,P,Kab,TNa,Text5], {A, B, P}) - A_non_injective_agreement_P: - niagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) + A_injective_agreement_P: + iagree(A_2[A,B,P,Kab,TVPa,Text3] -> P_2[A,B,P,Kab,TVPa,Text3], {A, B, P}) + + // No injective agreement, as the TTP does not receive any message from 'B'. B_non_injective_agreement_P: niagree(B_3[A,B,P,Kab,TNp,Text2] -> P_2[A,B,P,Kab,TNp,Text2], {A, B, P}) @@ -233,16 +247,16 @@ // (a) we also verify agreement on the freshness data // (b) we also verify agreement with the trusted third party // - A_non_injective_agreement_B: - niagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) + A_injective_agreement_B: + iagree(A_5[A,B,P,Kab,Rpa,Rb,Text6,Text8] -> B_5[A,B,P,Kab,Rpa,Rb,Text6,Text8], {A, B, P}) - B_non_injective_agreement_A: - niagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) + B_injective_agreement_A: + iagree(B_4[A,B,P,Kab,Rpa,Rb,Text6] -> A_4[A,B,P,Kab,Rpa,Rb,Text6], {A, B, P}) - A_non_injective_agreement_P: - niagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) + A_injective_agreement_P: + iagree(A_3[A,B,P,Ra,Kab,Text4] -> P_3[A,B,P,Ra,Kab,Text4], {A, B, P}) - B_non_injective_agreement_P: - niagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) + B_injective_agreement_P: + iagree(B_4[A,B,P,Rb,Kab,Text3] -> P_3[A,B,P,Rb,Kab,Text3], {A, B, P}) end diff --git a/data/examples/iso9798/isoiec-9798-3.spthy b/data/examples/iso9798/isoiec-9798-3.spthy --- a/data/examples/iso9798/isoiec-9798-3.spthy +++ b/data/examples/iso9798/isoiec-9798-3.spthy @@ -8,7 +8,7 @@ * - time-variant-parameters, time-stamps, and sequence numbers are * modeled by nonces leaked to the adversary at the start of a role. * - Given some pattern 'pkA', then the signature pattern 'sign{m}pkA' is - * translated to the message '(m, {m}inv(pkA))' upon execution. + * translated to the message '(m, {m}inv(pkA))' upon execution. */ theory isoiec_9798_3 begin @@ -30,12 +30,13 @@ leak_A. A -> : TNA text_1. -> A: Text1, Text2 - 1. A -> B: A, B, Text2, + 1. A -> B: A, B, Text2, sign{'isoiec_9798_3_1_sig_1', TNA, B, Text1 }pk(A) } +// No injective agreement here. properties (of isoiec_9798_3_1) - B_non_injective_agreement: + B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A}) @@ -56,14 +57,13 @@ 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 - 2. A -> B: A, B, Text3, + 2. A -> B: A, B, Text3, sign{'isoiec_9798_3_2_sig_2', Ra, Rb, B, Text2 }pk(A) } properties (of isoiec_9798_3_2) - // Note: for this agreement property the identity B must not be dropped - B_non_injective_agreement: - niagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A}) + B_injective_agreement: + iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A}) /**************************************************************************** @@ -83,21 +83,24 @@ { leak_A. A -> : TNA leak_B. B -> : TNB - + text_1. -> A: Text1, Text2 - 1. A -> B: A, B, Text2, + 1. A -> B: A, B, Text2, sign{'isoiec_9798_3_3_sig_1', TNA, B, Text1 }pk(A) text_2. -> B: Text3, Text4 - 2. B -> A: A, B, Text4, + 2. B -> A: A, B, Text4, sign{'isoiec_9798_3_3_sig_2', TNB, A, Text3 }pk(B) } +// No injective agreement. It requires a forth and back message, which does +// not exist for role B. For role 'A', we miss an opportunity for injective +// authentication, as we could include 'TNA' in the second message exchange. properties (of isoiec_9798_3_3) - A_non_injective_agreement: + A_non_injective_agreement: niagree(A_2[A,B,TNB,Text3] -> B_2[A,B,TNB,Text3], {B}) - B_non_injective_agreement: + B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A}) @@ -118,22 +121,22 @@ 1. B -> A: B, A, RB, Text1 text_2. -> A: Text2, Text3 - 2. A -> B: A, B, Text3, + 2. A -> B: A, B, Text3, sign{'isoiec_9798_3_4_sig_1', RA, RB, B, Text2 }pk(A) text_3. -> B: Text4, Text5 - 3. B -> A: B, A, Text5, + 3. B -> A: B, A, Text5, sign{'isoiec_9798_3_4_sig_2', RB, RA, A, Text4 }pk(B) } properties (of isoiec_9798_3_4) // The identity A in Step 3 is required for this property to hold. - A_non_injective_agreement: - niagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A,B}) + A_injective_agreement: + iagree(A_3[A,B,RA,RB,Text2,Text4] -> B_3[A,B,RA,RB,Text2,Text4], {A,B}) // The identity B in Step 2 is required for this property to hold. - B_non_injective_agreement: - niagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A}) + B_injective_agreement: + iagree(B_2[A,B,RA,RB,Text2] -> A_2[A,B,RA,RB,Text2], {A}) /**************************************************************************** @@ -158,22 +161,22 @@ 2. B -> A: B, A, RB, Text2 text_3. -> B: Text5, Text6 - 3. B -> A: B, A, Text6, + 3. B -> A: B, A, Text6, sign{'isoiec_9798_3_5_sig_1', RB, RA, A, Text5 }pk(B) text_4. -> A: Text3, Text4 - 4. A -> B: A, B, Text4, + 4. A -> B: A, B, Text4, sign{'isoiec_9798_3_5_sig_2', RA, RB, B, Text3 }pk(A) } properties (of isoiec_9798_3_5) // The identity A in Step 3 is required for this property to hold. - A_non_injective_agreement: - niagree(A_3[A,B,RA,RB,Text5] -> B_3[A,B,RA,RB,Text5], {B}) + A_injective_agreement: + iagree(A_3[A,B,RA,RB,Text5] -> B_3[A,B,RA,RB,Text5], {B}) // The identity B in Step 4 is required for this property to hold. - B_non_injective_agreement: - niagree(B_4[A,B,RA,RB,Text3,Text5] -> A_4[A,B,RA,RB,Text3,Text5], {A,B}) + B_injective_agreement: + iagree(B_4[A,B,RA,RB,Text3,Text5] -> A_4[A,B,RA,RB,Text3,Text5], {A,B}) /**************************************************************************** @@ -195,13 +198,13 @@ protocol isoiec_9798_3_6_1 { text_1. -> A: Text1 - 1. A -> B: A, B, Ra, Text1 - + 1. A -> B: A, B, Ra, Text1 + text_2. -> B: Text2, Text3 2. B -> : A, B, Ra, Rb, Text3, sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pk(B) - -> A: A, B, Ra, Rb, Text3, + -> A: A, B, Ra, Rb, Text3, TokenBA text_3. -> A: Text4 @@ -209,57 +212,52 @@ text_4. -> T: Text5, Text6, Text7 4. T -> : T, A, Text7, A, pk(A), B, pk(B), - sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pk(B), Text6}pk(T), + sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pk(B), Text6}pk(T), sign{'isoiec_9798_3_6_opt_1_sig_4_2', Rb, A, pk(A), Text5}pk(T) -> A: T, A, Text7, A, pk(A), B, pkB, - sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pkB, Text6}pk(T), + sign{'isoiec_9798_3_6_opt_1_sig_4_1', Rpa, B, pkB, Text6}pk(T), TokenTA_for_B // Here, A checks TokenBA against the public key pkB received from T. // As we lack support for additionally checked equalities, A sends a message // to itself encrypted with a fresh nonce to emulate the equality check. - check_4_out. A -> : {'check_4', + check_4_out. A -> : {'check_4', TokenBA }check_nonce_4 - check_4_in. -> A: {'check_4', - sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pkB + check_4_in. -> A: {'check_4', + sign{'isoiec_9798_3_6_opt_1_sig_2', B, Ra, Rb, A, Text2}pkB }check_nonce_4 // Note: we additionally send T such that B knows which key to use for // checking TokenTA_for_B text_5. -> A: Text8, Text9 5. A -> : A, B, Text9, T, - TokenTA_for_B, + TokenTA_for_B, sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra, B, A, Text8}pk(A) -> B: A, B, Text9, T, sign{'isoiec_9798_3_6_opt_1_sig_4_2', Rb, A, pkA, Text5}pk(T), - // Note: the standard does not require to check that 'Ra5 = Ra'! - sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra5, B, A, Text8}pkA + sign{'isoiec_9798_3_6_opt_1_sig_5', Rb, Ra, B, A, Text8}pkA } +// All properties except hold injectively. NOTE: Investigate this +// authentication "flaw" between Ra5 and Ra in role 'B'. properties (of isoiec_9798_3_6_1) - A_non_injective_agreement: - niagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) + A_injective_agreement: + iagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) - // Possible authentication FLAW: - // We do NOT get agreement on Ra because the standard does not require B to - // check its occurence in the signature from Step 5 to be equal with the - // one in Step 2. - // - // FIXME: What are the consequences? - B_non_injective_agreement: - niagree(B_5[A,B,Ra5,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) + B_injective_agreement: + iagree(B_5[A,B,Ra,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) // We additionally verify agreement of A and B with the TTP T. - A_non_injective_agreement_T: - niagree(A_5[B,T,Rpa,pkB ,Text6] -> - T_4[B,T,Rpa,pk(B),Text6], {T}) + A_injective_agreement_T: + iagree(A_5[B,T,Rpa,pkB ,Text6] -> + T_4[B,T,Rpa,pk(B),Text6], {T}) - B_non_injective_agreement_T: - niagree(B_5[A,T,Rb,pkA ,Text5] -> - T_4[A,T,Rb,pk(A),Text5], {T}) + B_injective_agreement_T: + iagree(B_5[A,T,Rb,pkA ,Text5] -> + T_4[A,T,Rb,pk(A),Text5], {T}) @@ -278,33 +276,30 @@ * - Option 1 and Option 2 must not share tags! * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. - - FIXME: Compare equality checks done here to what is prescribed in the - standard. We probably do a few more => there may be attacks on the - standard. - - We probably also shouldn't check the public keys delivered by T. - + * - Our model might perform a few equality checks more than what is strictly + * required by the standard. All of them are practically feasible and we + * advise to implement them. We do not verify whether we the security + * properties also hold with fewer equality checks. */ protocol isoiec_9798_3_6_2 { text_1. -> A: Text1 - 1. A -> B: A, B, Ra, Text1 - + 1. A -> B: A, B, Ra, Text1 + text_2. -> B: Text2, Text3 2. B -> : A, B, Ra, Rb, Text3, sign{'isoiec_9798_3_6_opt_2_sig_2', B, Ra, Rb, A, Text2}pk(B) - -> A: A, B, Ra, Rb, Text3, + -> A: A, B, Ra, Rb, Text3, TokenBA text_3. -> A: Text4 3. A -> T: A, T, Rpa, Rb, B, Text4 // Note: Text6 is not used in Option 2 - text_4. -> T: Text5, Text7 + text_4. -> T: Text5, Text7 4. T -> : T, A, Text7, A, pk(A), B, pk(B), - sign{ 'isoiec_9798_3_6_opt_2_sig_4', + sign{ 'isoiec_9798_3_6_opt_2_sig_4', Rpa, Rb, A, pk(A), B, pk(B), Text5 }pk(T) -> A: T, A, Text7, A, pk(A), B, pkB, TokenTA @@ -313,12 +308,12 @@ // key received from T. As we lack support for additionally checked // equalities, A sends a message to itself encrypted with a fresh nonce to // emulate the equality check. - check_4_out. A -> : {'check_4', + check_4_out. A -> : {'check_4', TokenTA, TokenBA }check_nonce_4 - check_4_in. -> A: {'check_4', - sign{'isoiec_9798_3_6_opt_2_sig_4', + check_4_in. -> A: {'check_4', + sign{'isoiec_9798_3_6_opt_2_sig_4', Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T), sign{'isoiec_9798_3_6_opt_2_sig_2', B, Ra, Rb, A, Text2}pkB }check_nonce_4 @@ -326,39 +321,32 @@ // Note: we additionally send T such that B knows which key to use for // checking TokenTA text_5. -> A: Text8, Text9 - 5. A -> : A, B, Rpa, Text9, T, + 5. A -> : A, B, Rpa, Text9, T, TokenTA, sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra, B, A, Text8}pk(A) -> B: A, B, Rpa, Text9, T, - sign{'isoiec_9798_3_6_opt_2_sig_4', - Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T), - // Note: the standard does not require to check that 'Ra5 = Ra'! - sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra5, B, A, Text8}pkA + sign{'isoiec_9798_3_6_opt_2_sig_4', + Rpa, Rb, A, pkA, B, pkB, Text5 }pk(T), + sign{'isoiec_9798_3_6_opt_2_sig_5', Rb, Ra, B, A, Text8}pkA } properties (of isoiec_9798_3_6_2) // Note that we do not get agreement on T! - A_non_injective_agreement: - niagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) + A_injective_agreement: + iagree(A_5[A,B,Ra,Rb,Text2] -> B_2[A,B,Ra,Rb,Text2], {B, T}) - // Possible authentication FLAW: - // We do NOT get agreement on Ra because the standard does not require B to - // check its occurence in the signature from Step 5 to be equal with the - // one in Step 2. - // - // FIXME: What are the consequences? - B_non_injective_agreement: - niagree(B_5[A,B,Ra5,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) + B_injective_agreement: + iagree(B_5[A,B,Ra,Rb,Text8] -> A_5[A,B,Ra,Rb,Text8], {A, T}) // We additionally verify agreement of A and B with the TTP T - A_non_injective_agreement_T: - niagree(A_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> - T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) + A_injective_agreement_T: + iagree(A_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> + T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) - B_non_injective_agreement_T: - niagree(B_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> - T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) + B_injective_agreement_T: + iagree(B_5[A,B,T,Rpa,Rb,pkA ,pkB ,Text5] -> + T_4[A,B,T,Rpa,Rb,pk(A),pk(B),Text5], {T}) @@ -377,21 +365,20 @@ * - Option 1 and Option 2 must not share tags! * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. - - FIXME: Compare equality checks done here to what is prescribed in the - standard. We probably do a few more => there may be attacks on the - standard. - + * - Our model might perform a few equality checks more than what is strictly + * required by the standard. All of them are practically feasible and we + * advise to implement them. We do not verify whether we the security + * properties also hold with fewer equality checks. */ protocol isoiec_9798_3_7_1 { text_1. -> B: Text1 - 1. B -> A: B, A, Rb, Text1 - + 1. B -> A: B, A, Rb, Text1 + text_2. -> A: Text2 - 2. A -> T: A, T, Rpa, Rb, A, B, Text2 + 2. A -> T: A, T, Rpa, Rb, A, B, Text2 - text_3. -> T: Text3, Text4, Text5 + text_3. -> T: Text3, Text4, Text5 3. T -> : T, A, Text5, A, pk(A), B, pk(B), sign{ 'isoiec_9798_3_7_opt_1_sig_3_1', Rpa, B, pk(B), Text4 }pk(T), sign{ 'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pk(A), Text3 }pk(T) @@ -402,36 +389,36 @@ // Note: we additionally send T such that B knows which key to use for // checking TokenTA text_4. -> A: Text6, Text7 - 4. A -> : A, B, Rpa, Text7, T, + 4. A -> : A, B, Rpa, Text7, T, TokenTA_for_B, sign{'isoiec_9798_3_7_opt_1_sig_4', Rb, Ra, B, A, Text6}pk(A) -> B: A, B, Rpa, Text9, T, - sign{'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pkA, Text3}pk(T), + sign{'isoiec_9798_3_7_opt_1_sig_3_2', Rb, A, pkA, Text3}pk(T), sign{'isoiec_9798_3_7_opt_1_sig_4', Rb, Ra, B, A, Text6}pkA text_5. -> B: Text8, Text9 5. B -> : A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_1_sig_5', Ra, Rb, A, B, Text8}pk(B) - -> A: A, B, Ra, Rb, Text9, + -> A: A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_1_sig_5', Ra, Rb, A, B, Text8}pkB } properties (of isoiec_9798_3_7_1) // Note that we do not get agreement on T! - A_non_injective_agreement: - niagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) + A_injective_agreement: + iagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) - B_non_injective_agreement: - niagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T}) + B_injective_agreement: + iagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T}) // We additionally verify agreement of A and B with the TTP T - A_non_injective_agreement_T: - niagree(A_3[B,T,Rpa,pkB,Text4] -> T_3[B,T,Rpa,pk(B),Text4], {T}) - B_non_injective_agreement_T: - niagree(B_4[A,T,Rb,pkA,Text3] -> T_3[A,T,Rb,pk(A),Text3], {T}) + A_injective_agreement_T: + iagree(A_3[B,T,Rpa,pkB,Text4] -> T_3[B,T,Rpa,pk(B),Text4], {T}) + B_injective_agreement_T: + iagree(B_4[A,T,Rb,pkA,Text3] -> T_3[A,T,Rb,pk(A),Text3], {T}) @@ -450,24 +437,23 @@ * - Option 1 and Option 2 must not share tags! * - We model the case where T sends the public keys instead of just verifying * the certificates; i.e., 'ResA = (A, pk(A))' and 'ResB = (B, pk(B))'. - - FIXME: Compare equality checks done here to what is prescribed in the - standard. We probably do a few more => there may be attacks on the - standard. - + * - Our model might perform a few equality checks more than what is strictly + * required by the standard. All of them are practically feasible and we + * advise to implement them. We do not verify whether we the security + * properties also hold with fewer equality checks. */ protocol isoiec_9798_3_7_2 { text_1. -> B: Text1 - 1. B -> A: B, A, Rb, Text1 - + 1. B -> A: B, A, Rb, Text1 + text_2. -> A: Text2 - 2. A -> T: A, T, Rpa, Rb, A, B, Text2 + 2. A -> T: A, T, Rpa, Rb, A, B, Text2 // Note: Text4 is not used in Option 2 - text_3. -> T: Text3, Text5 + text_3. -> T: Text3, Text5 3. T -> : T, A, Text5, A, pk(A), B, pk(B), - sign{ 'isoiec_9798_3_7_opt_2_sig_3', + sign{ 'isoiec_9798_3_7_opt_2_sig_3', Rpa, Rb, A, pk(A), B, pk(B), Text3 }pk(T) -> A: T, A, Text5, A, pk(A), B, pkB, TokenTA @@ -475,50 +461,50 @@ // Here, A checks TokenTA. As we lack support for additionally checked // equalities, A sends a message to itself encrypted with a fresh nonce to // emulate the equality check. - check_3_out. A -> : {'check_4', + check_3_out. A -> : {'check_4', TokenTA }check_nonce_4 - check_3_in. -> A: {'check_4', - sign{'isoiec_9798_3_7_opt_2_sig_3', + check_3_in. -> A: {'check_4', + sign{'isoiec_9798_3_7_opt_2_sig_3', Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T) }check_nonce_4 // Note: we additionally send T such that B knows which key to use for // checking TokenTA text_4. -> A: Text6, Text7 - 4. A -> : A, B, Rpa, Text7, T, + 4. A -> : A, B, Rpa, Text7, T, TokenTA, sign{'isoiec_9798_3_7_opt_2_sig_4', Rb, Ra, B, A, Text6}pk(A) -> B: A, B, Rpa, Text9, T, - sign{'isoiec_9798_3_7_opt_2_sig_3', - Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T), + sign{'isoiec_9798_3_7_opt_2_sig_3', + Rpa, Rb, A, pkA, B, pkB, Text3 }pk(T), sign{'isoiec_9798_3_7_opt_2_sig_4', Rb, Ra, B, A, Text6}pkA text_5. -> B: Text8, Text9 5. B -> : A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_2_sig_5', Ra, Rb, A, B, Text8}pk(B) - -> A: A, B, Ra, Rb, Text9, + -> A: A, B, Ra, Rb, Text9, sign{'isoiec_9798_3_7_opt_2_sig_5', Ra, Rb, A, B, Text8}pkB } properties (of isoiec_9798_3_7_2) - A_non_injective_agreement: - niagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) + A_injective_agreement: + iagree(A_5[A,B,Ra,Rb,Text8] -> B_5[A,B,Ra,Rb,Text8], {B, T}) - B_non_injective_agreement: - niagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T}) + B_injective_agreement: + iagree(B_4[A,B,Ra,Rb,Text6] -> A_4[A,B,Ra,Rb,Text6], {A, T}) // We additionally verify agreement of A and B with the TTP T - A_non_injective_agreement_T: - niagree(A_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> - T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) + A_injective_agreement_T: + iagree(A_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> + T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) - B_non_injective_agreement_T: - niagree(B_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> - T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) + B_injective_agreement_T: + iagree(B_4[A,B,T,Rpa,Rb,pkA ,pkB ,Text3] -> + T_3[A,B,T,Rpa,Rb,pk(A),pk(B),Text3], {T}) diff --git a/data/examples/iso9798/isoiec-9798-4-bdkey.spthy b/data/examples/iso9798/isoiec-9798-4-bdkey.spthy --- a/data/examples/iso9798/isoiec-9798-4-bdkey.spthy +++ b/data/examples/iso9798/isoiec-9798-4-bdkey.spthy @@ -31,6 +31,7 @@ h(('CCF', k[A,B]), ('isoiec_9798_4_1_ccf_1', TNA, B, Text1)) } +// Does not hold injectively. properties (of isoiec_9798_4_1_bdkey) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) @@ -55,8 +56,8 @@ } properties (of isoiec_9798_4_2_bdkey) - B_non_injective_agreement: - niagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B}) /****************************************************************************** @@ -81,6 +82,8 @@ h(('CCF', k[A,B]), ('isoiec_9798_4_3_ccf_2', TNb, A, Text3)) } +// Does not hold injectively. Missing an opportunity to get injective +// agreement for role A by adding TNa in the second message. properties (of isoiec_9798_4_3_bdkey) A_non_injective_agreement: niagree(A_2[A,B,TNb,Text3] -> B_2[A,B,TNb,Text3], {A, B}) @@ -112,11 +115,11 @@ } properties (of isoiec_9798_4_4_bdkey) - A_non_injective_agreement: - niagree(A_3[A,B,Ra,Rb,Text2,Text4] -> B_3[A,B,Ra,Rb,Text2,Text4], {A, B}) + A_injective_agreement: + iagree(A_3[A,B,Ra,Rb,Text2,Text4] -> B_3[A,B,Ra,Rb,Text2,Text4], {A, B}) - B_non_injective_agreement: - niagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A, B}) end diff --git a/data/examples/iso9798/isoiec-9798-4-udkey.spthy b/data/examples/iso9798/isoiec-9798-4-udkey.spthy --- a/data/examples/iso9798/isoiec-9798-4-udkey.spthy +++ b/data/examples/iso9798/isoiec-9798-4-udkey.spthy @@ -4,7 +4,7 @@ * Ported to scyther-proof: Simon Meier, Feb. 2011. * * Modeling notes: - * - Variant of ISO/IEC 9798-4 with unidirectional keys k(A,B) and + * - Variant of ISO/IEC 9798-4 with unidirectional keys k(A,B) and * identities dropped if possible. * - time-variant-parameters, time-stamps, and sequence numbers are * modeled by nonces leaked to the adversary at the start of a role. @@ -27,15 +27,18 @@ leak_A. A -> : TNA text_1. -> A: Text1, Text2 - 1. A -> B: A, B, TNA, Text2, Text1, + 1. A -> B: A, B, TNA, Text2, Text1, h(('CCF', k(A,B)), ('isoiec_9798_4_1_ccf_1', TNA, Text1)) } +// No injective agreement here, as the message from A can be received by +// multiple 'B's. properties (of isoiec_9798_4_1_udkey) B_non_injective_agreement: niagree(B_1[A,B,TNA,Text1] -> A_1[A,B,TNA,Text1], {A, B}) + /****************************************************************************** * Protocol 2 ****************************************************************************** @@ -50,13 +53,13 @@ 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 - 2. A -> B: A, B, Text3, Rb, Text2, + 2. A -> B: A, B, Text3, Rb, Text2, h(('CCF', k(A,B)), ('isoiec_9798_4_2_ccf_2', Rb, Text2)) } properties (of isoiec_9798_4_2_udkey) - B_non_injective_agreement: - niagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,Rb,Text2] -> A_2[A,B,Rb,Text2], {A, B}) /****************************************************************************** @@ -73,14 +76,17 @@ leak_B. B -> : TNb text_1. -> A: Text1, Text2 - 1. A -> B: A, B, TNa, Text2, Text1, + 1. A -> B: A, B, TNa, Text2, Text1, h(('CCF', k(A,B)), ('isoiec_9798_4_3_ccf_1', TNa, Text1)) text_2. -> B: Text3, Text4 - 2. B -> A: B, A, TNb, Text4, Text3, + 2. B -> A: B, A, TNb, Text4, Text3, h(('CCF', k(A,B)), ('isoiec_9798_4_3_ccf_2', TNb, Text3)) } +// The following properties do not hold injectively. This protocols misses a +// simple opportunity to get injective agreement for role A by adding TNa in +// the second message. properties (of isoiec_9798_4_3_udkey) A_non_injective_agreement: niagree(A_2[A,B,TNb,Text3] -> B_2[A,B,TNb,Text3], {A, B}) @@ -103,7 +109,7 @@ 1. B -> A: B, A, Rb, Text1 text_2. -> A: Text2, Text3 - 2. A -> B: A, B, Ra, Text3, Text2, + 2. A -> B: A, B, Ra, Text3, Text2, h(('CCF', k(A,B)), ('isoiec_9798_4_4_ccf_2', Ra, Rb, Text2)) text_3. -> B: Text4, Text5 @@ -112,10 +118,10 @@ } properties (of isoiec_9798_4_4_udkey) - A_non_injective_agreement: - niagree(A_3[A,B,Ra,Rb,Text2,Text4] -> B_3[A,B,Ra,Rb,Text2,Text4], {A, B}) + A_injective_agreement: + iagree(A_3[A,B,Ra,Rb,Text2,Text4] -> B_3[A,B,Ra,Rb,Text2,Text4], {A, B}) - B_non_injective_agreement: - niagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A, B}) + B_injective_agreement: + iagree(B_2[A,B,Ra,Rb,Text2] -> A_2[A,B,Ra,Rb,Text2], {A, B}) end diff --git a/data/isabelle/README b/data/isabelle/README --- a/data/isabelle/README +++ b/data/isabelle/README @@ -1,11 +1,9 @@ -====================================================================== -README for the scyther-proof security protocol verification tool -====================================================================== +README: The scyther-proof security protocol verification tool +============================================================= Author: Simon Meier -Creation Date: 13/05/2011 -Updated: 02/04/2012 +Creation Date: 13/05/2011 -- Last Updated: 28/06/2012 1. Introduction @@ -16,7 +14,7 @@ protocol models that were verified using scyther-proof. In particular, these examples include models for all of our repaired versions of the protocols from the ISO/IEC-9798 authentication standard. (In the source distribution - of scyther-proof they can be found at 'data/examples/iso9798'.) + of scyther-proof they can be found at `data/examples/iso9798`.) In the following sections, we give step by step instructions to get the whole system working and we explain the usage of our tools and provide @@ -32,75 +30,75 @@ You need a working Haskell environment that provides a version of GHC from 7.0.x to 7.4.x and the 'cabal install' tool. The simplest way to get such an environment is to download and install the Haskell Platform package for your - OS. - + OS. + http://hackage.haskell.org/platform/ - + Then call cabal install in the root directory of this source code package. This will use the - Haskell's deployment tool 'cabal-install' to download all missing libraries + Haskell's deployment tool `cabal-install` to download all missing libraries from Hackage, the central Haskell library repository and install the - 'scyther-proof' executable in the default installation location of + `scyther-proof` executable in the default installation location of cabal-install. The installation location is printed at the end of the build process. - Call - + Call + scyther-proof without any arguments to get an overview of the arguments supported and the paths to the examples and the Isabelle/HOL theories. -3.2 Installing the Isabelle/HOL theories +2.2 Installing the Isabelle/HOL theories ---------------------------------------- - Download and install full Isabelle2009-1 according to the installation - instructions at +Download and install full Isabelle2009-1 according to the installation +instructions at - http://isabelle.in.tum.de/website-Isabelle2009-1/download_x86-linux.html + http://isabelle.in.tum.de/website-Isabelle2009-1/download_x86-linux.html - The first time you call 'scyther-proof' with the '--isabelle' flag it will - build the logic image of the Isabelle/HOL theories formalizing the security - protocol verification theory underlying scyther-proof. +The first time you call `scyther-proof` with the `--isabelle` flag it will +build the logic image of the Isabelle/HOL theories formalizing the security +protocol verification theory underlying `scyther-proof`. - For enabling interactive processing of theory files based using our - extensions to Isabelle's ISAR proof language use one of the following two - variants. +For enabling interactive processing of theory files based using our +extensions to Isabelle's ISAR proof language use one of the following two +variants. - Variant a: Brute Force - ---------------------- +Variant a: Brute Force +---------------------- - Overwrite the standard Emacs keywords file - - $ISABELLE_HOME/etc/isar-keywords.el - - with the Emacs keywords file provided with the ESPL distribution. - - $SCYTHER_PROOF_HOME/isabelle/src/isar-keywords.el +Overwrite the standard Emacs keywords file - This is needed in order to make the new ISAR keywords "role", - "protocol", "sources", and "prefix_close" available in the Emacs - frontend. + $ISABELLE_HOME/etc/isar-keywords.el +with the Emacs keywords file provided with the ESPL distribution. - Variant b: Elegance - ------------------- + $SCYTHER_PROOF_HOME/isabelle/src/isar-keywords.el - A more elegant way is to copy the keywords file provided with our - distribution to +This is needed in order to make the new ISAR keywords `role`, +`protocol`, `sources`, and `prefix_close` available in the Emacs +frontend. - $ISABELLE_HOME/etc/isar-keywords-ESPL.el - and start Isabelle using the -k switch as follows. +Variant b: Elegance +------------------- - isabelle emacs -k ESPL +A more elegant way is to copy the keywords file provided with our +distribution to - + $ISABELLE_HOME/etc/isar-keywords-ESPL.el +and start Isabelle using the -k switch as follows. + + isabelle emacs -k ESPL + + + 3. Usage ======== @@ -147,11 +145,11 @@ proof construction using the following commands cd /src - isabelle emacs Tutorial.thy + isabelle emacs Tutorial.thy or if you've chosen the elegant variant - isabelle emacs -k ESPL Tutorial.thy + isabelle emacs -k ESPL Tutorial.thy Note that in many case the easiest way to start with constructing machine-checked proofs interactively is to use a proof script generated by @@ -159,9 +157,9 @@ *** -* Happy Proving :-) -* -* In case of questions do not hesistate to contact me at -* simon.meier@inf.ethz.ch -*** + +`Happy Proving :)` + +In case of questions do not hesistate to contact me at +iridcode@gmail.com. diff --git a/data/isabelle/src/ESPLogic/InferenceRules.thy b/data/isabelle/src/ESPLogic/InferenceRules.thy --- a/data/isabelle/src/ESPLogic/InferenceRules.thy +++ b/data/isabelle/src/ESPLogic/InferenceRules.thy @@ -478,4 +478,25 @@ end +subsubsection{* Reducing injective to non-injective agreement proofs *} + +lemma iagree_to_niagree: + assumes niagree: "\ i. prem i \ (\ j. conc i j)" + and conc_inj: "\ i1 i2 j. \ conc i1 j \ conc i2 j \ \ i1 = i2" + shows "let prems = prem; + concs = conc + in \f. inj_on f prems \ (\i. prems i \ concs i (f i))" +proof - + let ?f = "\ i. SOME j. conc i j" + have "inj_on ?f prem" + apply(auto simp: inj_on_def mem_def dest!: niagree) + apply(rule_tac j="(SOME j. conc x j)" in conc_inj[OF conjI]) + apply(rule someI, simp+)+ + done + moreover have "\ i. prem i \ conc i (?f i)" + by(auto simp: inj_on_def dest!: niagree intro: someI) + ultimately show ?thesis + by auto +qed + end diff --git a/interactive-only-src/Paths_scyther_proof.hs b/interactive-only-src/Paths_scyther_proof.hs --- a/interactive-only-src/Paths_scyther_proof.hs +++ b/interactive-only-src/Paths_scyther_proof.hs @@ -12,7 +12,7 @@ version :: Version -version = Version {versionBranch = [0,4,1,0], versionTags = []} +version = Version {versionBranch = [0,5,0,0], versionTags = []} bindir, libdir, datadir, libexecdir :: FilePath bindir = "." diff --git a/scyther-proof.cabal b/scyther-proof.cabal --- a/scyther-proof.cabal +++ b/scyther-proof.cabal @@ -1,6 +1,6 @@ build-type: Simple name: scyther-proof -version: 0.4.1.0 +version: 0.5.0.0 license: GPL license-file: LICENSE category: Security, Theorem Provers @@ -79,12 +79,12 @@ examples/iso9798/isabelle-parallel-proofs/*.thy examples/experimental/ExponentialBlowup.spthy - isabelle/AUTHORS - isabelle/document/root.tex - isabelle/IsaMakefile - isabelle/Makefile - isabelle/README - isabelle/ROOT.ML + isabelle/AUTHORS + isabelle/document/root.tex + isabelle/IsaMakefile + isabelle/Makefile + isabelle/README + isabelle/ROOT.ML isabelle/src/isar-keywords.el isabelle/src/*.thy isabelle/src/ESPLogic/*.thy @@ -96,7 +96,7 @@ .ghci interactive-only-src/Paths_scyther_proof.hs src/Scyther/Theory/Lexer.x_src_only - README + README.md CHANGES @@ -106,19 +106,19 @@ executable scyther-proof build-depends: - base == 4.* , - array >= 0.3 && < 0.5 , + base == 4.* , + array >= 0.3 && < 0.5 , containers >= 0.4.2 && < 0.5 , safe >= 0.2 && < 0.4 , - + mtl == 2.0.* , - + cmdargs >= 0.6.8 && < 0.7 , filepath >= 1.2 && < 1.4 , directory >= 1.0 && < 1.3 , - process == 1.1.* , + process == 1.1.* , time >= 1.1 && < 1.3 , - + parsec == 3.1.* , pretty >= 1.0 && < 1.2 , tagsoup == 0.12.* , @@ -134,7 +134,7 @@ other-modules: Extension.Prelude - Data.Color + Data.Color Data.Table Data.DAG.Simple Data.UnionFind @@ -166,4 +166,7 @@ Scyther.GoalFlow +source-repository head + type: git + location: https://github.com/meiersi/scyther-proof.git diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -30,7 +30,7 @@ import System.Process import System.Console.CmdArgs.Text -import System.Console.CmdArgs.Explicit +import System.Console.CmdArgs.Explicit import Extension.Prelude @@ -77,7 +77,7 @@ , ", ETH Zurich, 2009-2012" ] where - link href name = + link href name = "" ++ name ++ "" -- | Line width to use. @@ -122,11 +122,11 @@ | argExists "version" as = putStrLn versionStr | otherwise = io as - + ------------------------------------------------------------------------------ -- Argument Parsing ------------------------------------------------------------------------------ - + data PrintMode = SPTheory -- ^ Output as a security protocol theory. | IsarXSymbol -- ^ Output as an Isabelle theory using XSymbol symbols. @@ -139,7 +139,7 @@ examplePath <- getDataFileName "examples" readmePath <- getDataFileName "isabelle/README" isabellePath <- esplTheoryDir - return $ + return $ ( defaultMode programName "Automatic generation of machine-checked proofs for security protocols." [ "Additional information:" @@ -157,7 +157,7 @@ ) { modeCheck = upd "mode" "translate" , modeArgs = Just $ flagArg (upd "inFile") "FILES" - , modeGroupFlags = Group + , modeGroupFlags = Group { groupUnnamed = [ flagNone ["first", "f"] (addArg "strategy" "first") "Return the first found proof." @@ -234,14 +234,14 @@ ] } } - where + where upd a v = Right . addArg a v addEmpty a = addArg a "" defaultMode name help helpSuffix = Mode { modeGroupModes = toGroup [] - , modeNames = [name] - , modeValue = [] + , modeNames = [name] + , modeValue = [] , modeCheck = upd "mode" name , modeReform = const Nothing-- no reform possibility , modeHelp = help @@ -250,7 +250,7 @@ , modeGroupFlags = toGroup [] -- no flags } - outputFlags = + outputFlags = [ flagOpt "" ["output","o"] (upd "outFile") "FILE" "Output file" , flagOpt "" ["Output","O"] (upd "outDir") "DIR" "Output directory" ] @@ -262,7 +262,7 @@ mainMode <- setupMainMode putStrLn $ "error: " ++ msg putStrLn $ "" - putStrLn $ showText (Wrap 100) + putStrLn $ showText (Wrap 100) $ helpText HelpFormatDefault mainMode exitFailure @@ -292,7 +292,7 @@ -- | Execute a translation. -translateWorker :: Arguments +translateWorker :: Arguments -> FilePath -- ^ Path to HTML template file. -> MVar (T.Table String) -- ^ Empty MVar for building the report. -> IO () @@ -301,9 +301,9 @@ | otherwise = do -- check required tools when (not dryRun && html) (ensureGraphVizDot dotTool) - when (rebuildLogic || (not dryRun && isabelle)) + when (rebuildLogic || (not dryRun && isabelle)) (ensureIsabelleESPL rebuildLogic isabelleTool) - + -- translate all input files and ensure report is written with a special -- interrupted marker when an exception like Ctrl-C happened unless (n <= 1) (putInfoLn $ "processing "++show n++" files:") @@ -331,10 +331,10 @@ --------------- dryRun = outFile == "" && outDir == "" reportFile = fromMaybe "" $ findArg "report" as - outFile = fromMaybe "" $ findArg "outFile" as - outDir = fromMaybe "" $ findArg "outDir" as - + outFile = fromMaybe "" $ findArg "outFile" as + outDir = fromMaybe "" $ findArg "outDir" as + -- automatically generate the filename for output mkAutoPath :: FilePath -> String -> FilePath mkAutoPath dir name @@ -343,7 +343,7 @@ mkOutPath :: FilePath -- ^ Input file name. -> FilePath -- ^ Output file name. - mkOutPath inFile = + mkOutPath inFile = case outFile of "" -> case outDir of "" -> error "outPath: undefined in dry-run mode" @@ -366,7 +366,7 @@ -- protocol composition ----------------------- composeProtos :: Theory -> Theory - composeProtos + composeProtos | argExists "composeParallel" as = composeParallel | otherwise = id @@ -380,7 +380,7 @@ Nothing -> io Just t -> do res <- timeout (t * 1000000) io - case res of + case res of Nothing -> do updateReport (T.appendCell $ "timeout: "++show maxTime++"s") throw CustomTimeout @@ -403,15 +403,15 @@ reportNewRow = updateReport T.newRow >> putInfoLn "" reportNumber :: Show a => String -> a -> IO () - reportNumber header x = + reportNumber header x = updateReport (T.headerLastCell header . T.alignLastCell T.AlignRight. T.appendCell (show x)) reportString :: String -> String -> IO () - reportString header msg = + reportString header msg = updateReport (T.headerLastCell header . T.appendCell msg) - + updateReport :: (T.Table String -> T.Table String) -> IO () - updateReport + updateReport | null reportFile = const $ return () -- no report will be produced => don't update it | otherwise = modifyMVar_ reportVar . (return .) @@ -420,7 +420,7 @@ reportNumber "#chain rules" nChains reportNumber "#forward resolutions" nForward reportNumber "#missing proofs" nMissing - where + where (nChains, nForward, nMissing) = getProofSize s reportProperties :: Theory -> IO () @@ -447,7 +447,7 @@ ] return . concat $ [ "\n\n" - , header + , header , "\n" , T.toLaTeX (filter (/='\t')) table ] @@ -457,7 +457,7 @@ "" -> return () "-" -> mkReport >>= putStrLn _ -> mkReport >>= appendFile reportFile - + -- HTML generation ------------------ generateHtml :: FilePath -- ^ Input file @@ -475,14 +475,14 @@ , giTemplate = templateFile , giOutDir = mkOutPath inFile , giMarkup = thyToDoc printMode thy - , giProofScript = - \outPath -> renderDoc . runIdentity . + , giProofScript = + \outPath -> renderDoc . runIdentity . thyToDoc (ensureIsabellePrintMode printMode) $ adaptTheoryName outPath thy , giCmdLine = cmdLine , giDotTool = dotTool - , giIsabelle = - if isabelle + , giIsabelle = + if isabelle then Just $ checkTheoryFile isabelleTool isabelleThreads 0 "ESPL" else Nothing } @@ -495,7 +495,7 @@ makeOverview | overview = protocolsOnly -- theoryOverview | otherwise = id where - protocolsOnly (Theory name items) = + protocolsOnly (Theory name items) = Theory name [x | x@(ThyProtocol _) <- items ] thyToOverviewDoc :: Theory -> Isar.Doc @@ -508,9 +508,9 @@ reportString "Revision" =<< getSvnRevision inFile thy <- (makeOverview . ensureUniqueRoleNames) `liftM` parseTheory inFile reportProperties thy - return . + return . removeHiddenItems . - proveThy . + proveThy . composeProtos . addMissingTypingInvariants . -- if no reuse is done, then remove the hidden items before proving @@ -532,18 +532,19 @@ reuseSelector = case findArg "reuse" as of Just "none" -> mkReuse $ const False Just "secrecy" -> mkReuse $ \th -> - (complete $ thmProof th) && (FAtom AFalse == seConcl (thmSequent th)) + (complete $ thmProof th) && + (FAtom (ABool False) == seConcl (thmSequent th)) _ -> mkReuse $ (complete . thmProof) where mkReuse thmSel se th - | isTypingFormula $ seConcl se = + | isTypingFormula $ seConcl se = -- we do not support reusing in typing proofs -- because the ISAR pretty printer cannot handle it yet correctly. False - | otherwise = + | otherwise = -- type invariants and axioms are always reused isAxiom th || (isTypingFormula . seConcl $ thmSequent th) || thmSel th - + minimizer :: Proof -> Proof minimizer | noMinimize = id | otherwise = minimizeProof @@ -554,22 +555,22 @@ Just "shortest" -> allClaims $ shortestProof bound oldestOpenMessages _ -> id where - allClaims prover0 = + allClaims prover0 = proveSequents reuseSelector prover where prover toReuse se = fmap minimizer $ - (do guard (not noAttackSearch && bound == Nothing) + (do guard (not noAttackSearch && bound == Nothing) -- TODO: Make attack search respect bound. existsPossibleAttack oldestOpenMessages toReuse se - `mplus` + `mplus` prover0 toReuse se) - + -- Theory output ---------------- noGeneration = argExists "noGeneration" as html = argExists "html" as - isabelle = argExists "isabelle" as + isabelle = argExists "isabelle" as width = maybe lineWidth read $ findArg "charsPerLine" as isabelleThreads :: Maybe Int @@ -587,7 +588,7 @@ thyToDoc :: MarkupMonad m => PrintMode -> Theory -> m Isar.Doc thyToDoc pmode thy0 = case pmode of - SPTheory -> runTaggedIdentityT SlimOutput thyDoc + SPTheory -> runTaggedIdentityT SlimOutput thyDoc IsarXSymbol -> runReaderT thyDoc (Isar.defaultIsarConf { Isar.isarStyle = Isar.XSymbol }) IsarASCII -> runReaderT thyDoc Isar.defaultIsarConf where @@ -603,7 +604,7 @@ renderDoc = Isar.renderStyle (Isar.style { Isar.lineLength = width }) thyToString :: Theory -> String - thyToString + thyToString | html = renderDoc . evalHtmlMarkup . thyToDoc printMode -- | fol = render . tptpProblem . toTPTP | overview = renderDoc . thyToOverviewDoc @@ -612,7 +613,7 @@ writeThyFile :: FilePath -> Theory -> IO () writeThyFile outPath thy = do - if not noGeneration + if not noGeneration then do tGen <- execWithTimeout . timed_ . writeFile outPath . thyToString $ adaptTheoryName outPath thy @@ -640,7 +641,7 @@ mapM_ (putInfo . ('\t':)) ["CHECK FAILED", show tCheck, show msg] reportString "Isabelle Status" "check failed" reportString "Isabelle Message" (show msg) - else + else return () -- Translate one theory file @@ -650,7 +651,7 @@ -- writeThyFile. I didn't do this once, which cost me quite some -- debugging time. processThy :: FilePath -> Theory -> IO () - processThy inFile thy + processThy inFile thy | dryRun = putStrLn (thyToString thy) | html = do generateHtml inFile thy @@ -691,7 +692,7 @@ -- | Read the SVN revision of the given file using the SVN command. getSvnRevision :: FilePath -> IO String -getSvnRevision file = +getSvnRevision file = handle handler $ do (_, info, _) <- readProcessWithExitCode "svn" ["info",file] [] return $ maybe "unversioned" @@ -703,7 +704,7 @@ -- | Read the cpu info using a call to cat /proc/cpuinfo getCpuModel :: IO String -getCpuModel = +getCpuModel = handle handler $ do (_, info, _) <- readProcessWithExitCode "cat" ["/proc/cpuinfo"] [] return $ maybe errMsg @@ -717,7 +718,7 @@ -- | Test if a process is executable and check its response. This is used to -- determine the versions and capabilities of tools that we depend on. -testProcess :: (String -> String -> Either String String) +testProcess :: (String -> String -> Either String String) -- ^ Analysis of stdout, stderr. Use 'Left' to report error. -> String -- ^ Test description to display. -> FilePath -- ^ Process to start @@ -739,7 +740,7 @@ case exitCode of ExitFailure code -> errMsg $ "failed with exit code " ++ show code - ExitSuccess -> + ExitSuccess -> case check out err of Left msg -> errMsg msg Right msg -> do putStrLn msg @@ -805,16 +806,16 @@ putStrLn "---" putStrLn "Attempting to build ESPL logic (this may take several minutes):" theoryDir <- esplTheoryDir - let isamake args = + let isamake args = runProcess isabelle ("make" :args) (Just theoryDir) Nothing Nothing Nothing Nothing >>= waitForProcess exitCode <- isamake ["clean"] >> isamake [] case exitCode of ExitSuccess -> putStrLn "Sucess! :-)\n---" - ExitFailure code -> putStrLn $ unlines + ExitFailure code -> putStrLn $ unlines [ " Logic building failed with code: " ++ show code , " Proof checking is likely not to work." , " To investigate the problem try manually loading/building the theories in" , " '" ++ theoryDir ++ "'" ] - + diff --git a/src/Scyther/Facts.hs b/src/Scyther/Facts.hs --- a/src/Scyther/Facts.hs +++ b/src/Scyther/Facts.hs @@ -11,7 +11,7 @@ -- * Facts , Facts , protocol - + -- ** Construction , empty , freshTID @@ -29,6 +29,7 @@ , proveAtom , proveFormula , toAtoms + , toFormula , nextTID , nextArbMsgId , quantifiedTIDs @@ -45,7 +46,7 @@ , saturateFacts , exploitTypingFacts , exploitLongTermKeySecrecy - + , splittableEqs , splitEqFacts @@ -103,7 +104,7 @@ ------------------------------------------------------------------------------ -- | A conjunction of logical facts. --- +-- -- Invariants that hold for a value @facts = Facts _ evs evord co uc eqs@: -- -- 1. All facts are invariant under their corresponding substitution. This @@ -132,7 +133,7 @@ -- NOTE: The Maybe is used for facts that don't have a typing. , typeAnns :: S.Set TypeAnn -- ^ Type annotations on messages. - , covered :: S.Set Message -- ^ The messages that have already been used in a + , covered :: S.Set Message -- ^ The messages that have already been used in a -- case distinction. , protocol :: Protocol -- ^ The protocol that the current state -- is a reachable state of. @@ -147,7 +148,7 @@ -- well-typedness claim are present. Note that there may be quantifiers and -- covered goals. nullFacts :: Facts -> Bool -nullFacts facts = +nullFacts facts = S.null (events facts) && S.null (eventOrd facts) && S.null (compromised facts) && @@ -170,19 +171,19 @@ -- -- Uses 'fail' for error reporting. setProtocol :: Monad m => Protocol -> Facts -> m Facts -setProtocol proto facts +setProtocol proto facts | proto == protocol facts = return facts - | otherwise = fail $ "setProtocol: '" ++ show proto ++ "' /= '" - ++ show (protocol facts) ++ "'" + | otherwise = fail $ "setProtocol: '" ++ show proto ++ "' /= '" + ++ show (protocol facts) ++ "'" --- | Set the typing. +-- | Set the typing. -- -- PRE: There mustn't be a different existing typing. -- -- Uses 'fail' for error reporting. setTyping :: Monad m => Typing -> Facts -> m Facts setTyping typ facts = case optTyping facts of - Just typ' | typ /= typ' -> fail $ "setTyping: '" ++ show typ ++ "' /= '" + Just typ' | typ /= typ' -> fail $ "setTyping: '" ++ show typ ++ "' /= '" ++ show typ' ++ "'" _ -> return $ facts { optTyping = Just typ } @@ -198,23 +199,23 @@ -- `fail` is called in the given monad. quantifyTID :: Monad m => TID -> Facts -> m Facts quantifyTID tid facts - | null (tidQuantified facts tid) = + | null (tidQuantified facts tid) = fail $ "quantifyTID: " ++ show tid ++ " already quantified." - | otherwise = + | otherwise = return $ facts { tidQuantifiers = S.insert tid $ tidQuantifiers facts } -- | Tries to quantify the given agent identifier. If it is already quantified -- `fail` is called in the given monad. quantifyArbMsgId :: Monad m => ArbMsgId -> Facts -> m Facts quantifyArbMsgId aid facts - | null (arbMsgIdQuantified facts aid) = + | null (arbMsgIdQuantified facts aid) = fail $ "quantifyArbMsgId: " ++ show aid ++ " already quantified." - | otherwise = + | otherwise = return $ facts { amQuantifiers = S.insert aid $ amQuantifiers facts } -- | Get a fresh TID and the updated set of facts. freshTID :: Facts -> (TID, Facts) -freshTID facts = +freshTID facts = (tid, facts { tidQuantifiers = S.insert tid $ tidQuantifiers facts }) where tid = nextTID facts @@ -260,7 +261,7 @@ -- | Check if a TID is quantified in these facts tidQuantified :: Facts -> TID -> CertResult -tidQuantified facts tid = +tidQuantified facts tid = certErrorIf (tid `S.notMember` tidQuantifiers facts) $ "unquantified tid: " ++ show tid @@ -299,7 +300,7 @@ -- | Check if all logical variables in a type annotation are quantified. typeAnnQuantified :: Facts -> TypeAnn -> CertResult -typeAnnQuantified facts (m, _, tid) = +typeAnnQuantified facts (m, _, tid) = msgQuantified facts m >< tidQuantified facts tid -- | Check if an equality contains only quantified logical variables. @@ -312,11 +313,11 @@ E.AVarEq (av1, av2) -> avarQuantified facts av1 >< avarQuantified facts av2 E.MVarEq (mv, m) -> mvarQuantified facts mv >< msgQuantified facts m E.MsgEq (m1, m2) -> msgQuantified facts m1 >< msgQuantified facts m2 - + -- | Check if an atom contains only quantified logical variables. atomQuantified :: Facts -> Atom -> CertResult atomQuantified facts atom = case atom of - AFalse -> certSuccess + ABool _ -> certSuccess AEq eq -> anyEqQuantified facts eq AEv ev -> evQuantified facts ev AEvOrd ord -> evOrdQuantified facts ord @@ -329,9 +330,9 @@ -- | Certification of a value with respect to a check and a morphism required -- to establish the required invariants in the context of a set of facts. -certify :: Show a => (Facts -> a -> CertResult) -> (Facts -> a -> b) +certify :: Show a => (Facts -> a -> CertResult) -> (Facts -> a -> b) -> Facts -> a -> Cert b -certify check conv facts x = +certify check conv facts x = case check facts x of [] -> x' -- FIXME: Somehow bidirectional shared keys lead in some cases to an @@ -339,8 +340,8 @@ -- dealt with proofs that failed (i.e., attackable security -- properties). Therfore, we have not yet debugged this to its full -- extent. - errs -> trace - (unlines $ + errs -> trace + (unlines $ ("warning: internal check failed for '" ++ show x ++ "' because of") : (map (" "++) $ errs) ) @@ -438,8 +439,8 @@ -- This operation is logically safe iff there are no references to the mapped -- logical variables outside the facts. trimQuantifiers :: Facts -> Facts -trimQuantifiers facts = facts { - equalities = eqs' +trimQuantifiers facts = facts { + equalities = eqs' , tidQuantifiers = S.filter (`notElem` tids) $ tidQuantifiers facts , amQuantifiers = S.filter (`notElem` aids) $ amQuantifiers facts } @@ -463,7 +464,7 @@ , covered = S.map (E.substMsg eqs) (covered facts) } - + -- Compromised agents --------------------- @@ -497,7 +498,7 @@ -- | Inserts an event order fact. insertEvOrd :: Cert (Event, Event) -> Facts -> Facts -insertEvOrd ord prems = +insertEvOrd ord prems = prems { eventOrd = S.insert (certified ord) (eventOrd prems) } -- | Delete an event order fact. @@ -526,24 +527,24 @@ -- -- PRE: The atom must pass certification under the given facts. -- --- PRE: The atom must not be a 'AHasTyp' or a 'ATyping' atom, as they are not --- representable by 'Facts' conjoinAtoms :: Monad m => [Atom] -> Facts -> m (Maybe Facts) -conjoinAtoms atoms facts0 = foldM conjoinAtom (Just facts0) atoms +conjoinAtoms atoms facts0 = + foldM conjoinAtom (Just facts0) atoms where - conjoinAtom Nothing _ = return Nothing - conjoinAtom (Just facts) atom = case certified $ certAtom facts atom of - AFalse -> return Nothing - -- FIXME: repeated calls to solve may be a bit expensive due to duplicated - -- work of 'removeTrivialFacts'. - AEq eq -> return $ solve [Cert eq] facts - AEv ev -> return . Just $ insertEvNonTrivial (Cert ev) facts - AEvOrd ord -> return . Just $ insertEvOrdNonTrivial (Cert ord) facts - ACompr m -> return . Just $ compromise m facts - AUncompr m -> return . Just $ uncompromise m facts - AReachable p -> Just `liftM` setProtocol p facts - ATyping typ -> Just `liftM` setTyping typ facts - AHasType tya -> return . Just $ insertTypeAnn (Cert tya) facts + conjoinAtom Nothing _ = return Nothing + conjoinAtom (Just facts) atom = case certified $ certAtom facts atom of + ABool False -> return Nothing + ABool True -> return (Just facts) + -- FIXME: repeated calls to solve may be a bit expensive due to duplicated + -- work of 'removeTrivialFacts'. + AEq eq -> return $ solve [Cert eq] facts + AEv ev -> return . Just $ insertEvNonTrivial (Cert ev) facts + AEvOrd ord -> return . Just $ insertEvOrdNonTrivial (Cert ord) facts + ACompr m -> return . Just $ compromise m facts + AUncompr m -> return . Just $ uncompromise m facts + AReachable p -> Just `liftM` setProtocol p facts + ATyping typ -> Just `liftM` setTyping typ facts + AHasType tya -> return . Just $ insertTypeAnn (Cert tya) facts -- Combined construction and application of inference rules @@ -552,8 +553,8 @@ -- | Inserts an event order fact and both event facts implied by the presence -- of this event oder fact. insertEvOrdAndEvs :: Cert (Event, Event) -> Facts -> Facts -insertEvOrdAndEvs ord = - insertEv (mapCertified fst ord) . +insertEvOrdAndEvs ord = + insertEv (mapCertified fst ord) . insertEv (mapCertified snd ord) . insertEvOrd ord -- | Insert all non-trivial events implied by the given event. @@ -570,7 +571,7 @@ _ -> insertEvOrdAndEvs ord prems where insertLearnBefore to p m = insertEvOrdAndEvs (Cert (Learn m, to)) p - + -- | Insert an executed role step and all non-trivial facts implied by the -- Input rule. insertStepInputClosed :: Cert (TID, RoleStep) -> Facts -> Facts @@ -600,7 +601,7 @@ (Step tid step) -> insertStepPrefixClosed (Cert (tid, step)) -- | Derive all non-trivial facts implied by the splitting rules and remove --- remove trivial facts. +-- trivial facts. removeTrivialFacts :: Facts -> Facts removeTrivialFacts = execState $ do evs <- S.toList <$> gets events @@ -633,8 +634,8 @@ -- -- Is equal to 'mzero' in case the facts don't contain a typing. exploitTypingFacts :: MonadPlus m => Facts -> m Facts -exploitTypingFacts facts0 = return facts0 -- TODO: implement this check. - {- cf. the one for weak atomicity below: +exploitTypingFacts facts0 = return facts0 -- TODO: implement this check. + {- cf. the one for weak atomicity below: do -- WeaklyAtomic -> foldl' weaklyAtomic facts0 . E.getMVarEqs . equalities $ facts0 where @@ -644,11 +645,11 @@ weaklyAtomic facts (MVar (LocalId (i, tid)), m ) = case threadRole tid facts of Nothing -> error $ "exploitTypingFacts: no role assigned to '"++show tid++"'" - Just role -> + Just role -> case find (S.member i . stepFMV) (roleSteps role) of - Nothing -> + Nothing -> error $ "exploitTypingFacts: variable '"++show i++"' does not occur in role." - Just step -> + Just step -> insertEvOrdNonTrivial (Cert (Learn m, Step tid step)) facts -} @@ -673,7 +674,7 @@ -- NOTE: This is not the same as trying to prove the atom AFalse under these -- premises. The checks are separated due to efficiency reasons. proveFalse :: Facts -> Bool -proveFalse prems = +proveFalse prems = not (S.null (compromised prems `S.intersection` uncompromised prems)) || any noAgent (S.toList (compromised prems)) || cyclic (eventOrd prems) @@ -694,7 +695,7 @@ where -- PRE: atom is fully substituted checkAtom atom = case atom of - AFalse -> False + ABool b -> b AEq eq -> E.reflexive eq AEv (Learn m) -> all checkLearn (splitNonTrivial m) AEv ev -> ev `S.member` events facts @@ -709,12 +710,12 @@ checkLearn m = Learn m `S.member` events facts checkLearnBefore to m = before (eventOrd facts) (Learn m) to - hasType (m0, ty0, tid0) = + hasType (m0, ty0, tid0) = go m0 ty0 where go (MAVar _) (AgentT) = True go (MConst i) (ConstT i') = i == i' - go (MFresh (Fresh (LocalId (i, tid)))) (NonceT role i') = + go (MFresh (Fresh (LocalId (i, tid)))) (NonceT role i') = i == i' && threadRole tid facts == Just role go (MHash m) (HashT ty) = go m ty go (MEnc m1 m2) (EncT ty1 ty2) = go m1 ty1 && go m2 ty2 @@ -728,7 +729,7 @@ (m', ty', tid') <- S.toList $ typeAnns facts guard (m == m') return $ (ty', tid') `subType` (ty, tid0) - + -- ty `subType` ty' holds iff every instance of ty is also an instance of ty'. subType (ty0, tid) (ty'0, tid') = go ty0 ty'0 @@ -792,6 +793,13 @@ , AHasType <$> S.toList (typeAnns facts) ] +-- | Represent the facts as a formula. +toFormula :: Facts -> Formula +toFormula facts = case toAtoms facts of + [] -> FAtom (ABool True) + atoms -> foldr1 FConj (map FAtom atoms) + + ------------------------------------------------------------------------------ -- Chain Rule Application ------------------------------------------------------------------------------ @@ -802,9 +810,9 @@ -- set of events. openMessages :: Facts -> [Message] openMessages prems = nub $ filter okGoal $ catMaybes - [ case e of Learn m -> Just m; _ -> Nothing + [ case e of Learn m -> Just m; _ -> Nothing | e <- S.toList $ events prems `S.difference` S.map snd (eventOrd prems) ] - where + where okGoal (MMVar _) = False okGoal (MArbMsg _) = False okGoal (MAsymPK _) = False @@ -813,12 +821,12 @@ -- | Sort open messages ascending with respect to the maximal thread id. oldestOpenMessages :: Facts -> [Message] -oldestOpenMessages prems = +oldestOpenMessages prems = map fst . sortOn snd . mapMaybe score $ ms where ms = openMessages prems co = compromised prems - ltkLocalIds (MAsymSK m@(MAVar a)) + ltkLocalIds (MAsymSK m@(MAVar a)) | m `S.member` co = [] | otherwise = [getAVar a] ltkLocalIds (MSymK ma@(MAVar a) mb@(MAVar b)) @@ -843,7 +851,7 @@ type ChainRuleM = StateT ChainRuleState [] --- | Add a fragment of the case name. +-- | Add a fragment of the case name. addCaseFragment :: String -> ChainRuleM () addCaseFragment name = modify $ \crs -> crs { crsCaseName = crsCaseName crs ++ [name] } @@ -866,13 +874,13 @@ -- try to unify the two messages in the context of the current facts; -- this function will always succeed, but the facts may be Nothing unify :: Message -> Message -> ChainRuleM () -unify m m' +unify m m' | m == m' = return () -- performance optimization | otherwise = do crs <- get - maybe mzero (modifyFacts . const) $ + maybe mzero (modifyFacts . const) $ solve [certAnyEq (crsFacts crs) $ E.MsgEq (m', m)] (crsFacts crs) - + -- | Get a fresh thread identifier and update the facts accordingly getFreshTID :: ChainRuleM TID getFreshTID = do @@ -880,7 +888,7 @@ modifyFacts (const facts) addNewVar (Left tid) return tid - + -- | Get a fresh thread arbitrary-message id and update the facts accordingly getFreshAMID :: ChainRuleM ArbMsgId getFreshAMID = do @@ -891,13 +899,13 @@ -- | Add a type annotation. addTypeAnn :: TypeAnn -> ChainRuleM () -addTypeAnn tya = modifyFacts $ +addTypeAnn tya = modifyFacts $ \facts -> insertTypeAnn (certTypeAnn facts tya) facts -- | Delete the given type annotation. Logically, this means forgetting -- the corresponding assumption. deleteTypeAnn :: TypeAnn -> ChainRuleM () -deleteTypeAnn tya = modifyFacts $ +deleteTypeAnn tya = modifyFacts $ \facts -> facts { typeAnns = S.delete tya (typeAnns facts) } -- | Add a type annotation in expanded form. Expansion stops at SumT types @@ -912,13 +920,13 @@ expand :: ChainRuleM Message -> Type -> ChainRuleM Message expand mkV AgentT = do v <- mkV - addTypeAnn (v, AgentT, tid) + addTypeAnn (v, AgentT, tid) return v expand _ (NonceT role n) = do nTid <- getFreshTID modifyFacts $ insertRole nTid role return $ MFresh (Fresh (LocalId (n, nTid))) - + expand mkV ty@(SumT _ _) = do v <- mkV addTypeAnn (v, ty, tid) @@ -939,7 +947,7 @@ arb :: ChainRuleM Message arb = MArbMsg <$> getFreshAMID - + -- | Get the type annotation of a message. -- -- PRE: The message must be normalized with respect to the current facts. @@ -965,10 +973,10 @@ extractCase :: [E.AnyEq] -> ChainRuleState -> Maybe ((String, [Either TID ArbMsgId]), Facts) extractCase delayedEqs0 crs = do let facts0 = crsFacts crs - unmappedTID tid + unmappedTID tid | substTID facts0 tid == tid = return (Left tid) | otherwise = mzero - unmappedAMID aid + unmappedAMID aid | substAMID facts0 aid == MArbMsg aid = return (Right aid) | otherwise = mzero @@ -1025,12 +1033,12 @@ chainRuleFacts (MInvKey _) _ = error $ "chainRuleFacts: application to symbolically inverted keys not supported." chainRuleFacts (MAsymPK _) _ = error $ "chainRuleFacts: no support for public keys." chainRuleFacts (MTup _ _) _ = error $ "chainRuleFacts: no support for tuples." -chainRuleFacts m facts0 +chainRuleFacts m facts0 | proveAtom facts0 (F.AEv (Learn m)) = assembleCases `liftM` getTyping facts0 | otherwise = error $ "chainRuleFacts: could not prove that '" ++ show m ++ "' is known to the intruder." where - assembleCases typ = - mapMaybe (extractCase delayedEqs) . numberCases . + assembleCases typ = + mapMaybe (extractCase delayedEqs) . numberCases . flip execStateT (ChainRuleState [] [] facts1 Nothing) $ ( initialIntruderKnowledge m `mplus` @@ -1055,10 +1063,10 @@ \facts -> foldl' insertSingle facts prev where insertSingle p prevEv = insertEvOrdNonTrivial (certEvOrd p (prevEv, ev)) p - + -- enumerate chainRuleFacts starting from the given role roleChains :: Typing -> TID -> Role -> ChainRuleM () - roleChains typ tid role = do + roleChains typ tid role = do modifyFacts $ insertRole tid role addCaseFragment $ roleName role msum . map stepChains $ roleSteps role @@ -1072,7 +1080,7 @@ mapM_ annotateMVarType $ S.toList $ patFMV pt msgChains [(Step tid step)] (inst tid pt) where - -- annotating message variables with their type + -- annotating message variables with their type annotateMVarType mv = case M.lookup (mv, role) typ of Nothing -> error $ "stepChains: no type provided for '"++show v++"'" @@ -1105,8 +1113,8 @@ msgChains prev v@(MMVar _) = do addCaseFragment (msgName v) typChains prev v - - msgChains prev m'@(MEnc m1 m2) = + + msgChains prev m'@(MEnc m1 m2) = do insertPrevious prev (Learn m') ( do -- trace ("msgChains: unify " ++ show m' ++ " =?= " ++ show m) (return ()) addCaseFragment $ msgName m' @@ -1120,7 +1128,7 @@ insertPrevious prev (Learn m') addCaseFragment $ msgName m' -- here we have to unify, as Isabelle is also doing it early - unify m' m + unify m' m -- the m' is an atomic message: just unify and be done with it. msgChains prev m' = do @@ -1136,7 +1144,7 @@ then msgChains prev v' else do tya <- getTypeAnn v - case tya of + case tya of (_,tyaTy,tyaTid) -> case tyaTy of KnownT _ -> mzero -- protocol wellformedness checks that KnownT implies cyclicity AgentT -> mzero -- we already know the agent names @@ -1158,7 +1166,7 @@ -- | Equalities that can be splitted. splittableEqs :: Facts -> [MsgEq] -splittableEqs facts = +splittableEqs facts = do eq@(MShrK _ _, MShrK _ _) <- getPostEqs $ equalities facts guard (not $ uncurry (==) eq) return eq @@ -1172,7 +1180,7 @@ where addEqs eqs = solve (map (certAnyEq facts) eqs) facts -splitEqFacts eq _ = +splitEqFacts eq _ = error $ "splitEqFacts: cannot split equality '" ++ show eq ++ "'" @@ -1215,7 +1223,7 @@ -- | Apply the mapping of agent and thread equalities to the facts. -- --- TODO: Improve error handling. Currently, 'error' is called if the facts +-- TODO: Improve error handling. Currently, 'error' is called if the facts -- are contradictory after the substitution. applyMapping :: Mapping -> Facts -> Facts applyMapping mapping facts0 = case newFacts of @@ -1232,11 +1240,11 @@ quantifyTIDs facts = foldM qTID facts $ S.toList $ tidQuantifiers facts0 quantifyAIDs facts = foldM qAID facts $ S.toList $ amQuantifiers facts0 - addAtoms = conjoinAtoms atoms + addAtoms = conjoinAtoms atoms atoms = map (F.substAtom (getMappingEqs mapping)) . toAtoms $ facts0 extractArbMsgId (MArbMsg aid) = aid - extractArbMsgId m = error $ + extractArbMsgId m = error $ "applyMapping: arbitrary-message id mapped to '" ++ show m ++ "'" @@ -1260,7 +1268,7 @@ ---------- -- | Pretty print the facts in Isar format. -isaFacts :: IsarConf -> Facts +isaFacts :: IsarConf -> Facts -> ([Doc],[Doc],[Doc]) -- ^ Quantified variables, representable facts, and non-representable facts isaFacts conf facts = ( ppSet (isar conf) (tidQuantifiers facts) ++ @@ -1271,7 +1279,7 @@ ppSet (isaEventOrd conf (Mapping eqs)) (eventOrd facts) ++ ppSet (isaEvent conf (Mapping eqs)) (events facts) , map (isar conf) nonReprEqs - ) + ) where eqs = equalities facts (reprEqs, nonReprEqs) = partition isReprEq $ E.toAnyEqs eqs @@ -1295,21 +1303,21 @@ , (map (sptTypeAnn (`threadRole` facts)) $ S.toList $ typeAnns facts) ++ map sptAnyEq nonReprEqs ++ (map ppCovered $ S.toList $ covered facts) - ) + ) where eqs = equalities facts (reprEqs, nonReprEqs) = partition isReprEq $ E.toAnyEqs eqs ppCovered m = text "covered" <> parens (sptMessage m) - ppComprInfo setName set + ppComprInfo setName set | S.null set = mzero | otherwise = return . fsep $ - (text setName <> lparen : (map (nest 2) . punctuate comma) + (text setName <> lparen : (map (nest 2) . punctuate comma) (ppSet sptMessage set)) ++ [rparen] {- sptSimpleFacts :: Facts -> Doc -sptSimpleFacts facts = case sptFacts facts of +sptSimpleFacts facts = case sptFacts facts of (ds1, ds2, ds3) -> vcat $ map vcat [ds1, [text ""], ds2, [text ""], ds3] -} @@ -1321,7 +1329,7 @@ findChain sel x cs = case break ((x ==) . sel) cs of (_,[]) -> (cs, [x]) (cs1, c:cs2) -> (cs1 ++ cs2, c) - insertEdge chains0 (from,to) = + insertEdge chains0 (from,to) = let (chains1, prefix) = findChain last from chains0 (chains2, suffix) = findChain head to chains1 in (prefix ++ suffix) : chains2 diff --git a/src/Scyther/Formula.hs b/src/Scyther/Formula.hs --- a/src/Scyther/Formula.hs +++ b/src/Scyther/Formula.hs @@ -15,6 +15,7 @@ , isTypingFormula , destTypingFormula , atomTIDs + , formulaTIDs , findRole -- * Pretty Printing @@ -48,7 +49,7 @@ -- | A representable logical atom. data Atom = - AFalse -- ^ 'False' in Isabelle. + ABool Bool -- ^ 'False' and 'True' in Isabelle. | AEq AnyEq -- ^ An equality | AEv Event -- ^ An event must have happened. | AEvOrd (Event, Event) -- ^ An event order. @@ -61,7 +62,7 @@ deriving( Eq, Show, Ord, Data, Typeable ) -- | A representable logical formula. Currently these are monotonic formula. -data Formula = +data Formula = FAtom Atom | FConj Formula Formula | FExists (Either TID ArbMsgId) Formula @@ -81,7 +82,7 @@ -- | Relabel quantified TIDs according to the given list of labels. relabelTIDs :: [TID] -> Formula -> Formula -relabelTIDs tids0 formula = +relabelTIDs tids0 formula = runReader (evalStateT (go formula) tids0) (Mapping E.empty) where go (FAtom atom) = FAtom <$> ((substAtom . getMappingEqs) <$> ask <*> pure atom) @@ -90,7 +91,7 @@ tids <- get case tids of [] -> error "relabelTIDs: out of labels" - tid':tids' -> do + tid':tids' -> do put tids' FExists (Left tid') <$> local (addTIDMapping tid tid') (go inner) go (FExists q@(Right _) inner) = FExists q <$> go inner @@ -98,7 +99,7 @@ -- | Compute the threads associated to the given atom. atomTIDs :: Atom -> [TID] -atomTIDs AFalse = mzero +atomTIDs (ABool _) = mzero atomTIDs (ATyping _) = mzero atomTIDs (AReachable _) = mzero atomTIDs (AEv e) = evTIDs e @@ -107,18 +108,25 @@ atomTIDs (AUncompr m) = msgTIDs m atomTIDs (AHasType tya) = typeAnnTIDs tya atomTIDs (AEq eq) = anyEqTIDs eq - +-- | Compute the free thread variables of the given formula. +formulaTIDs :: Formula -> [TID] +formulaTIDs (FAtom atom) = atomTIDs atom +formulaTIDs (FConj f1 f2) = formulaTIDs f1 ++ formulaTIDs f2 +formulaTIDs (FExists (Left tid) f) = filter (tid /=) $ formulaTIDs f +formulaTIDs (FExists (Right _) f) = formulaTIDs f + + -- Substitution --------------- -- | Substitute all variables in an atom. --- +-- -- NOTE: A 'HasType' atom will only have its thread identifier substituted, but -- not the whole message variable. substAtom :: Equalities -> Atom -> Atom substAtom eqs atom = case atom of - AFalse -> atom + ABool _ -> atom AEq eq -> AEq $ substAnyEq eqs eq AEv ev -> AEv $ substEv eqs ev AEvOrd ord -> AEvOrd $ substEvOrd eqs ord @@ -140,9 +148,9 @@ -- 'fail' for error reporting. conjunctionToAtoms :: MonadPlus m => Formula -> m [Atom] conjunctionToAtoms (FAtom a) = return [a] -conjunctionToAtoms (FConj f1 f2) = +conjunctionToAtoms (FConj f1 f2) = (++) `liftM` conjunctionToAtoms f1 `ap` conjunctionToAtoms f2 -conjunctionToAtoms _ = +conjunctionToAtoms _ = fail "conjunctionToAtoms: existential quantifier encountered." -- | Split all toplevel conjunctions. @@ -188,17 +196,18 @@ -- | Pretty print an atom in Isar format. isaAtom :: IsarConf -> Mapping -> Atom -> Doc isaAtom conf mapping atom = case atom of - AFalse -> text "False" + ABool False -> text "False" + ABool True -> text "True" AEq eq -> ppIsar eq AEv ev -> isaEvent conf mapping ev AEvOrd ord -> isaEventOrd conf mapping ord ACompr av -> isaCompr conf av AUncompr av -> isaUncompr conf av - AHasType (m,ty,i) -> ppIsar m <-> isaIn conf <-> - isar conf ty <-> ppIsar i <-> + AHasType (m,ty,i) -> ppIsar m <-> isaIn conf <-> + isar conf ty <-> ppIsar i <-> isaExecutionSystemState conf ATyping _ -> text "well-typed" - AReachable p -> + AReachable p -> text "(t,r,s)" <-> isaIn conf <-> text "reachable" <-> text (protoName p) where ppIsar :: Isar a => a -> Doc @@ -208,13 +217,14 @@ -- | Pretty print an atom in security protocol theory format. sptAtom :: Mapping -> Atom -> Doc sptAtom mapping atom = case atom of - AFalse -> text "False" + ABool False -> text "False" + ABool True -> text "True" AEq eq -> sptAnyEq eq AEv ev -> sptEvent mapping ev AEvOrd (e1,e2) -> sptEventOrd mapping [e1,e2] ACompr av -> sptCompr av AUncompr av -> sptUncompr av - AHasType tya -> sptTypeAnn (const Nothing) tya + AHasType tya -> sptTypeAnn (const Nothing) tya ATyping typ -> sptTyping typ AReachable p -> text "reachable" <-> text (protoName p) @@ -225,7 +235,7 @@ where ppIsar :: Isar a => a -> Doc ppIsar = isar conf - + pp m (FAtom atom) = isaAtom conf m atom pp m (FConj f1 f2) = sep [pp m f1 <-> isaAnd conf, pp m f2] pp m (FExists v f) = parens $ diff --git a/src/Scyther/Proof.hs b/src/Scyther/Proof.hs --- a/src/Scyther/Proof.hs +++ b/src/Scyther/Proof.hs @@ -49,8 +49,8 @@ import Extension.Prelude -import Scyther.Facts -import qualified Scyther.Equalities as E +import Scyther.Facts +import qualified Scyther.Equalities as E import Scyther.Sequent ------------------------------------------------------------------------------ @@ -79,6 +79,7 @@ -- | Supported rules. data Rule = Saturate + | ReduceInjectivity | ForwardResolution (Named Sequent) E.Mapping | ChainRule Message [(String, [Either TID ArbMsgId])] | SplitEq E.MsgEq [Bool] -- True, if sub-proof for this case is present. @@ -121,38 +122,45 @@ -- | Try proving a sequent by assumption; i.e. by showing that the premises -- directly imply the conclusion. byAssumption :: Monad m => Sequent -> m Proof -byAssumption se@(Sequent prem concl) +byAssumption se@(Sequent prem concl Standard) | proveFalse prem = return $ Trivial se TrivContradictoryPremises | proveFormula prem concl = return $ Trivial se TrivPremisesImplyConclusion | otherwise = case exploitLongTermKeySecrecy prem of Just key -> return $ Trivial se (TrivLongTermKeySecrecy key) Nothing -> fail $ "byAssumption: cannot prove conclusion from premises" +byAssumption _ = fail $ "byAssumption: only work for standard sequents" -- | An order preferring typing conclusions and then false conclusions. reuseOrder :: Formula -> Formula -> Ordering -reuseOrder (FAtom (ATyping typ1)) (FAtom (ATyping typ2)) = compare typ1 typ2 -reuseOrder (FAtom (ATyping _)) _ = LT -reuseOrder _ (FAtom (ATyping _)) = GT -reuseOrder (FAtom AFalse) (FAtom AFalse) = EQ -reuseOrder (FAtom AFalse) _ = LT -reuseOrder _ (FAtom AFalse) = GT -reuseOrder f1 f2 = compare f1 f2 +reuseOrder (FAtom (ATyping typ1)) (FAtom (ATyping typ2)) = compare typ1 typ2 +reuseOrder (FAtom (ATyping _)) _ = LT +reuseOrder _ (FAtom (ATyping _)) = GT +reuseOrder (FAtom (ABool False)) (FAtom (ABool False)) = EQ +reuseOrder (FAtom (ABool False)) _ = LT +reuseOrder _ (FAtom (ABool False)) = GT +reuseOrder f1 f2 = compare f1 f2 -- | A generic proof strategy for proving sequents. Eagerly reuses lemmas in -- the order they were given using forward resolution. -genericProof :: MonadPlus m +genericProof :: MonadPlus m => m () -- ^ A marker for usages of the chain rule. -> (Facts -> [Message]) -- ^ A heuristic for the order of -- messages to be tried using the chain rule. -> [Named Sequent] -- ^ Rules that should be reused in this proof. -> Sequent -- ^ The sequent to be proven -> m Proof -genericProof chainRuleMarker goals rawRules se0 = - case saturate se0 of - Just se1 -> (RuleApp se0 Saturate . return) `liftM` prove se1 - Nothing -> prove se0 +genericProof chainRuleMarker goals rawRules se0 = + case reduceInjectivity se0 of + Just (Left err) -> + return $ Missing se0 ("failed to reduce injectivity: " ++ err) True + Just (Right se1) -> + (RuleApp se0 ReduceInjectivity . return) `liftM` + (genericProof chainRuleMarker goals rawRules se1) + Nothing -> case saturate se0 of + Just se1 -> (RuleApp se0 Saturate . return) `liftM` prove se1 + Nothing -> prove se0 where -- the theorems for reuse: prefer false conclusions over arbitrary conclusions reusableRules :: [Named Sequent] @@ -162,7 +170,7 @@ reuseRule se rule = do (mapping, optSequent) <- frule (snd rule) se let mkProof = RuleApp se (ForwardResolution rule mapping) - case optSequent of + case optSequent of Nothing -> return $ return $ mkProof [] Just sequent -> return $ (mkProof . return) `liftM` prove sequent @@ -176,7 +184,7 @@ Nothing -> return $ Missing se "prover stuck => no type invariant available" True -- prove a sequent - prove se = + prove se = case byAssumption se of Just prf -> return prf -- proven by assumption Nothing -> @@ -194,7 +202,7 @@ let sequents = splitEq eq se RuleApp se (SplitEq eq (map isJust sequents)) `liftM` mapM prove (catMaybes sequents) - + -- there is none => chain rule is our last resort [] -> case goals (sePrem se) of @@ -206,23 +214,23 @@ -- | Use a (possibly bounded) depth-first search for finding the proof. -- TODO: Make error handling explicit. dfsProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof -dfsProof Nothing heuristic rules se = +dfsProof Nothing heuristic rules se = runUnboundedDFS $ genericProof (return ()) heuristic rules se -dfsProof (Just bound) heuristic rules se = +dfsProof (Just bound) heuristic rules se = evalBoundedDFS (genericProof (updateCost succ) heuristic rules se) (<= bound) 0 - + -- | Use branch-and-bound search to find the shortest proof. -- TODO: Make error handling explicit. shortestProof :: Maybe Int -> (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof -shortestProof optBound heuristic rules se = +shortestProof optBound heuristic rules se = evalBranchAndBound (genericProof (updateCost (fmap succ)) heuristic rules se) - optBound + optBound -- | Check if there exists a case where the prover gets stuck using unbounded DFS -- and the given heuristic and theorems to reuse. existsPossibleAttack :: (Facts -> [Message]) -> [Named Sequent] -> Sequent -> Maybe Proof -existsPossibleAttack heuristic rules se = +existsPossibleAttack heuristic rules se = findAttack =<< (runUnboundedDFS $ genericProof (return ()) heuristic rules se) ------------------------------------------------------------------------------ @@ -236,7 +244,7 @@ mkSubproof se prf = put se >> go prf go :: Proof -> StateT Sequent Maybe Proof - go (Missing _ reason showSequent) = + go (Missing _ reason showSequent) = Missing <$> get <*> pure reason <*> pure showSequent go prf@(Axiom seAxiom) = do se <- get @@ -260,6 +268,13 @@ Just key' -> do guard (key == key') Trivial <$> get <*> pure reason Nothing -> mzero + go (RuleApp _ ReduceInjectivity [prf]) = do + se <- get + case reduceInjectivity se of + Just (Right se') -> + (RuleApp se ReduceInjectivity . return) <$> (put se' >> go prf) + Just _ -> mzero + Nothing -> go prf go (RuleApp _ Saturate [prf]) = do se <- get case saturate se of @@ -270,7 +285,7 @@ let statePrem = sePrem se guard (proveFacts statePrem (sePrem $ snd thm) mapping) optSequent <- fruleInst (snd thm) mapping se - case optSequent of + case optSequent of Nothing -> do guard (null prfs) return $ RuleApp se rule prfs Just sequent -> case prfs of @@ -309,19 +324,19 @@ findAttack = fmap head . go . return where unvisited prf = Missing (prfSequent prf) "not yet investigated" False - + go :: [Proof] -> Maybe [Proof] go [] = Nothing go (prf : prfs) = case prf of - RuleApp se rule subprfs -> + RuleApp se rule subprfs -> -- look for an attack in the subproofs of the given rule (do subprfs' <- go subprfs return $ RuleApp se rule subprfs' : map unvisited prfs ) `mplus` -- look for an attack in the remaining proofs - ((unvisited prf :) `liftM` go prfs) + ((unvisited prf :) `liftM` go prfs) -- attack found: return it together with the unvisited siblings - PossibleAttack _ _ -> return $ prf : map unvisited prfs + PossibleAttack _ _ -> return $ prf : map unvisited prfs -- look for an attack in the siblings and prepend ourselves unvisited _ -> (unvisited prf :) `liftM` go prfs @@ -339,10 +354,10 @@ -- | Minimize a proof by removing all unnecesary forward resolutions. minimizeProof :: Proof -> Proof minimizeProof prf0 = fromMaybe prf0 $ do - prf <- go prf0 + prf <- go prf0 checkProof (prfSequent prf) prf where - go (RuleApp se rule@(ForwardResolution _ _) [prf]) = do + go (RuleApp se rule@(ForwardResolution _ _) [prf]) = do prf' <- go prf (checkProof se prf' <|> pure (RuleApp se rule [prf'])) go (RuleApp se rule prfs) = @@ -358,7 +373,7 @@ -- | Extracts the first type invariant occurring in a forward resolution. This -- is required because in Isabelle type invariants are handled using locales, --- while we are handling them using forward resolution. +-- while we are handling them using forward resolution. -- -- Note that our system here is more general, but for the current setup, we do -- not see this generality. @@ -381,14 +396,14 @@ deriving( Eq, Ord, Monoid ) instance Show ProofSize where - show s = + show s = concat ["C:", show nChain, " F:", show nForward, " M:", show nMissing] where (nChain, nForward, nMissing) = getProofSize s -- | Extract the raw proof size information. getProofSize :: ProofSize -> (Int, Int, Int) -getProofSize (ProofSize (nChain, nForward, nMissing)) = +getProofSize (ProofSize (nChain, nForward, nMissing)) = (getSum nChain, getSum nForward, getSum nMissing) -- | The size of a missing proof. @@ -425,10 +440,10 @@ displayChainRule :: Protocol -> Maybe Typing -> Proof displayChainRule _ _ = error "displayChainRule: not yet upgraded" {- -displayChainRule proto optTyp = +displayChainRule proto optTyp = RuleApp se (ChainRule optTyp m (map fst cases)) (map mkPrf cases) where - tid = 0 + tid = 0 m = (MMVar (LocalId (Id "m", tid))) prem = insertEv (Learn m) $ insertThread tid $ emptyFacts se = Sequent proto (FFacts prem) FFalse diff --git a/src/Scyther/Sequent.hs b/src/Scyther/Sequent.hs --- a/src/Scyther/Sequent.hs +++ b/src/Scyther/Sequent.hs @@ -3,10 +3,12 @@ -- * Datatype Sequent(..) + , SequentQualifier(..) , seProto -- ** Logically safe construction , wellTypedCases + , reduceInjectivity , saturate , frule , fruleInst @@ -23,7 +25,10 @@ import Control.Arrow import Control.Monad +import Control.Applicative +import Extension.Prelude (sortednub) + import qualified Scyther.Equalities as E import Scyther.Facts import Scyther.Formula @@ -33,12 +38,25 @@ -- Sequents ------------------------------------------------------------------------------ +-- | A qualifier changing the interpretation of a sequent. +data SequentQualifier = + Standard + -- ^ The standard interpretation of a sequent as given in our CSF'10 + -- paper on strong invariants for the efficient construction of + -- machine-checked security proofs. + | Injective + -- ^ An injective interpretation of a sequent. Only valid for sequents + -- that have exactly one free TID-variable in the premise and exactly + -- one further TID-variable in the conclusion. + deriving( Eq, Ord, Show, Data, Typeable ) + -- | A sequent with a conjunction of a set of facts as the premise and a single -- formula as the conclusion denoting a statement about a reachable state of -- a protocol. data Sequent = Sequent { - sePrem :: Facts - , seConcl :: Formula + sePrem :: Facts + , seConcl :: Formula + , seQualifier :: SequentQualifier } deriving( Eq, Show, Ord, Data, Typeable ) @@ -46,15 +64,19 @@ seProto :: Sequent -> Protocol seProto = protocol . sePrem +-- | 'True' iff the sequent is viewed with the 'Standard' interpretation. +isStandard :: Sequent -> Bool +isStandard = (Standard ==) . seQualifier + -- Construction --------------- -- | Make all thread identifiers occurring in the sequent unique by -- consistently relabeling the thread identifiers in the conclusion. uniqueTIDQuantifiers :: Sequent -> Sequent -uniqueTIDQuantifiers (Sequent prem concl) = - Sequent prem (relabelTIDs [nextTID prem..] concl) +uniqueTIDQuantifiers (Sequent prem concl quali) = + Sequent prem (relabelTIDs [nextTID prem..] concl) quali -- | Apply a function to the premise, but return only the updated sequent if -- the premise was changed. @@ -73,42 +95,40 @@ -- -- Uses 'fail' for error reporting. wellTypedCases :: MonadPlus m => Sequent -> m [(String, Sequent)] -wellTypedCases se = case seConcl se of - FAtom (ATyping typ) -> - return $ protoRoles (seProto se) >>= roleProofs typ - _ -> mzero +wellTypedCases se@(Sequent _ (FAtom (ATyping typ)) Standard) = + return $ protoRoles (seProto se) >>= roleProofs where - roleProofs typ role = proveRecvs S.empty (roleSteps role) - where - proveRecvs _ [] = [] - proveRecvs recv ( Send _ _ : steps) = proveRecvs recv steps - proveRecvs recv ((Recv _ (PMVar lid)) : steps) = - -- don't prove single reiceves as they are handled directly by the tactic - -- on the Isabelle side. - proveRecvs (S.insert lid recv) steps - proveRecvs recv (step@(Recv _ pt) : steps) = - let mvars = patFMV pt - in (S.toList mvars >>= proveVar) `mplus` - (proveRecvs (recv `S.union` mvars) steps) + roleProofs role = + proveRecvs S.empty (roleSteps role) where - proveVar v - | v `S.member` recv = fail "proveVar: not first receive" - | otherwise = do - return (name, Sequent prem concl) - where - name = roleName role ++ "_" ++ stepLabel step ++ "_" ++ getId v - (tid, prem0) = freshTID (sePrem se) - mv = MVar (LocalId (v, tid)) - premErr = error $ "wellTypedCases: could not add thread " ++ show tid ++ ". This should not happen." - prem1 = maybe premErr saturateFacts . join $ - conjoinAtoms [AEv (Step tid step), AEq (E.TIDRoleEq (tid, role))] prem0 - prem = fromMaybe (error "failed to set typing") $ setTyping typ prem1 - concl = FAtom $ - case M.lookup (v, role) typ of - Just ty -> AHasType (MMVar mv, ty, tid) - Nothing -> error $ - "wellTypedCases: no type given for '"++show v++"' in role '"++roleName role++"'" + proveRecvs _ [] = [] + proveRecvs recv ( Send _ _ : steps) = proveRecvs recv steps + proveRecvs recv ((Recv _ (PMVar lid)) : steps) = + -- don't prove single reiceves as they are handled directly by the tactic + -- on the Isabelle side. + proveRecvs (S.insert lid recv) steps + proveRecvs recv (step@(Recv _ pt) : steps) = + let mvars = patFMV pt + in (S.toList mvars >>= proveVar) `mplus` + (proveRecvs (recv `S.union` mvars) steps) + where + proveVar v + | v `S.member` recv = fail "proveVar: not first receive" + | otherwise = return (name, Sequent prem concl Standard) + where + name = roleName role ++ "_" ++ stepLabel step ++ "_" ++ getId v + (tid, prem0) = freshTID (sePrem se) + mv = MVar (LocalId (v, tid)) + premErr = error $ "wellTypedCases: could not add thread " ++ show tid ++ ". This should not happen." + prem1 = maybe premErr saturateFacts . join $ + conjoinAtoms [AEv (Step tid step), AEq (E.TIDRoleEq (tid, role))] prem0 + prem = fromMaybe (error "failed to set typing") $ setTyping typ prem1 + concl = FAtom $ case M.lookup (v, role) typ of + Just ty -> AHasType (MMVar mv, ty, tid) + Nothing -> error $ + "wellTypedCases: no type given for '"++show v++"' in role '"++roleName role++"'" +wellTypedCases _ = mzero -- | Emulate a variant Isabelle's 'frule' tactic. It works only if the given -- maping of free variables of the rule makes the premise of the rule provable @@ -117,10 +137,10 @@ -- last step works currently only for conclusions being false of pure -- conclusions. -- --- NOTE that 'frule' works only for rules that contain no existential --- quantifiers in the conclusion. +-- NOTE that 'frule' works only for rules that are standard sequents and that +-- contain no existential quantifiers in the conclusion. fruleInst :: MonadPlus m - => Sequent -- ^ rule + => Sequent -- ^ rule -> E.Mapping -- ^ mapping of free variables of rule to proof state -> Sequent -- ^ proof state -> m (Maybe Sequent) -- ^ some result if resolution worked. Nothing @@ -128,21 +148,23 @@ -- premises of proof state were extended. -- -- mzero if rule could not be applied -fruleInst rule mapping state = do - atoms <- conjunctionToAtoms $ seConcl rule - let statePrem = sePrem state - guard (proveFacts statePrem (sePrem rule) mapping) - optStatePrem' <- conjoinAtoms (map (substAtom (E.getMappingEqs mapping)) atoms) statePrem - case optStatePrem' of - Nothing -> do return Nothing - Just statePrem' -> do guard (statePrem /= statePrem') - return . Just $ Sequent statePrem' (seConcl state) +fruleInst rule mapping state + | isStandard rule && isStandard state = do + atoms <- conjunctionToAtoms $ seConcl rule + let statePrem = sePrem state + guard (proveFacts statePrem (sePrem rule) mapping) + optStatePrem' <- conjoinAtoms (map (substAtom (E.getMappingEqs mapping)) atoms) statePrem + case optStatePrem' of + Nothing -> do return Nothing + Just statePrem' -> do guard (statePrem /= statePrem') + return . Just $ Sequent statePrem' (seConcl state) Standard + | otherwise = mzero -- | Like 'fruleInst' but tries all mappings. frule :: MonadPlus m - => Sequent -- ^ rule + => Sequent -- ^ rule -> Sequent -- ^ proof state - -> m (E.Mapping, Maybe Sequent) + -> m (E.Mapping, Maybe Sequent) -- ^ some result if resolution worked. Nothing denotes that False was -- derived. Just means that premises of proof state were extended. -- @@ -180,21 +202,64 @@ return (mapping, Just $ Sequent prem1 (seConcl state)) -} +-- | Try to prove an 'Injective' sequent by reducing it to its non-injective +-- counterpart. +reduceInjectivity :: Sequent -> Maybe (Either String Sequent) +reduceInjectivity se + | seQualifier se /= Injective = Nothing + -- We have an injective sequent => we must reduce it or report a failure to + -- reduce it. + | otherwise = Just $ + case sortednub $ formulaTIDs $ toFormula $ sePrem se of + [premTID] -> case decomposeConcl $ seConcl se of + Just (concTID, atoms) -> + if check premTID concTID atoms + then Right (se { seQualifier = Standard }) + else Left "conclusion does not immediatly entail injectivity" + Nothing -> Left $ + "only works for conclusions of the form '? tid. ato1 & ... & atoN'" + premTIDs -> Left $ + "too few/many thread identifiers in premises " ++ show premTIDs + where + decomposeConcl (FExists (Left tid) fm) = (,) tid <$> conjunctionToAtoms fm + decomposeConcl _ = Nothing + + -- check that conclusion entails equality of premise TIDs + check premTID0 concTID atoms = + case E.solve (rawEqs0 ++ rawEqs1) E.empty of + Just eqs -> E.substTID eqs premTID0 == E.substTID eqs premTID1 + _ -> False + where + premTID1 = 1 + max premTID0 concTID + + rawEqs0 = [ eq | AEq eq <- atoms ] + rawEqs1 = map rename rawEqs0 + + rename = E.substAnyEq $ E.getMappingEqs $ + E.addTIDMapping premTID0 premTID1 E.emptyMapping + + + + + -- | Try to saturate a sequent, if possible and leading to new facts. saturate :: MonadPlus m => Sequent -> m Sequent -saturate = changePrem (return . saturateFacts) +saturate se = do + guard (isStandard se) + changePrem (return . saturateFacts) se --- | Try to use the chain rule. +-- | Try to use the chain rule. -- -- MonadPlus is used to report a failure to apply the rule. -- -chainRule :: MonadPlus m - => Sequent -> Message +chainRule :: MonadPlus m + => Sequent -> Message -> m [((String, [Either TID ArbMsgId]), Sequent)] -chainRule se m = +chainRule se m = do + guard (isStandard se) map (second mkSequent) `liftM` chainRuleFacts m (sePrem se) - where - mkSequent prem = Sequent prem (seConcl se) + where + mkSequent prem = Sequent prem (seConcl se) Standard -- | Try to exploit the typing. Fails if no new facts could be derived. exploitTyping :: MonadPlus m => Sequent -> m Sequent @@ -203,14 +268,14 @@ -- | Split a splittable equality. -- splitting can be done. splitEq :: E.MsgEq -> Sequent -> [Maybe Sequent] -splitEq eq se +splitEq eq se | eq `elem` splittableEqs prems = map (fmap updPrem) $ splitEqFacts eq prems | otherwise = error $ "splitEq: equality not present" where prems = sePrem se updPrem prem' = se {sePrem = prem'} - + diff --git a/src/Scyther/Theory.hs b/src/Scyther/Theory.hs --- a/src/Scyther/Theory.hs +++ b/src/Scyther/Theory.hs @@ -31,7 +31,7 @@ , theoryProofSize , theoryOverview , classifyProperties - -- , wfTheory -- TODO: Implement type wellformedness check. + -- , wfTheory -- TODO: Implement type wellformedness check. -- Currently, we rely on Isabelle for the last soundness check. ) where @@ -141,11 +141,11 @@ where mkTypingSequent p = case mscTyping p of Just typ -> return $ ThySequent ( protoName p ++ "_msc_typing" - , Sequent (empty p) (FAtom (ATyping typ))) + , Sequent (empty p) (FAtom (ATyping typ)) Standard) Nothing -> mzero add item = case item of - ThyProtocol p + ThyProtocol p | noTypingInvariant p -> [item] ++ mkTypingSequent p _ -> [item] @@ -160,10 +160,10 @@ -- | Prove all claims with the given heuristic optionally using the given -- bound. -proveSequents :: (Sequent -> Theorem -> Bool) +proveSequents :: (Sequent -> Theorem -> Bool) -- ^ Predicate determining theorems for reuse for proving the -- given sequent. - -> ([Named Sequent] -> Sequent -> Maybe Proof) + -> ([Named Sequent] -> Sequent -> Maybe Proof) -- ^ Proof construction function. -> Theory -> Theory proveSequents reuse prover thy = @@ -171,7 +171,7 @@ where prove (item@(ThySequent (name, se))) = do prevItems <- get - let reusableThms = [ (thmName th, thmSequent th) + let reusableThms = [ (thmName th, thmSequent th) | ThyTheorem th <- prevItems, reuse se th, thmProto th == seProto se] case prover reusableThms se of @@ -189,7 +189,7 @@ thmInfo thm = (thmName thm, thmProto thm) kept = [ thmInfo thm | ThyTheorem thm <- items, mustKeep $ thmName thm ] dependencies = - [ (thmInfo thm, dep) + [ (thmInfo thm, dep) | ThyTheorem thm <- items, dep <- S.toList . depends $ thmProof thm ] toKeep = reachableSet kept dependencies keep :: ThyItem -> Bool @@ -224,35 +224,34 @@ -- | Compose all protocol in the theory in parallel. Assumes that both protocol -- names as well as role names are /globally/ unique. composeParallel :: Theory -> Theory -composeParallel thy +composeParallel thy | length ps <= 1 = thy | otherwise = thy { thyItems = [ThyProtocol pc, ThySequent sec] ++ items3 } where (ps, items1) = partitionEithers $ do item <- thyItems thy - case item of + case item of ThyProtocol p -> return $ Left p _ -> return $ Right item (typs, items2) = partitionEithers $ do - item <- items1 + item <- items1 case item of - ThySequent (_, Sequent _ (FAtom (ATyping typ))) + ThySequent (_, Sequent _ (FAtom (ATyping typ)) Standard) -> return $ Left typ ThySequent x -> return $ Right $ ThySequent $ prefixProtoName (seProto $ snd x) x ThyTheorem x -> return $ Right $ ThyTheorem $ prefixProtoName (thmProto x) x _ -> return $ Right item - prefixProtoName :: Protocol -> (String, a) -> (String, a) prefixProtoName p x@(n, v) | protoName p `isPrefixOf` n = x | otherwise = (protoName p ++ "_" ++ n, v) - + namec = thyName thy pc = Protocol namec (concatMap protoRoles ps) sec = ( namec ++ "_composed_typing" - , Sequent (empty pc) (FAtom (ATyping (M.unions typs))) + , Sequent (empty pc) (FAtom (ATyping (M.unions typs))) Standard ) replaceProtocol :: Protocol -> Protocol @@ -266,16 +265,16 @@ -- | Find a protocol in the theory according to its name. lookupProtocol :: String -> Theory -> Maybe Protocol -lookupProtocol name thy = +lookupProtocol name thy = headMay [proto | ThyProtocol proto <- thyItems thy, protoName proto == name] -- | Find all unsound theorems of the theory. unsoundTheorems :: Theory -> [(Protocol, String)] -unsoundTheorems (Theory _ items) = - [ (prfProto prf, name) - | ThyTheorem (name, prf) <- items, not (sound prf) +unsoundTheorems (Theory _ items) = + [ (prfProto prf, name) + | ThyTheorem (name, prf) <- items, not (sound prf) ] ++ - [ (seProto se, name) + [ (seProto se, name) | ThySequent (name, se) <- items ] @@ -291,7 +290,7 @@ classifyProperties toClassify = foldl classify (0,0,0) . thyItems where getSequent (ThyTheorem thm) = do - guard (toClassify $ thmName thm) + guard (toClassify $ thmName thm) return $ thmSequent thm getSequent (ThySequent se) = do guard (toClassify (fst se)) @@ -306,7 +305,7 @@ -- | True, if the sequent implies 'FFalse'. isContradictionProp :: Sequent -> Bool - isContradictionProp = (FAtom AFalse ==) . seConcl + isContradictionProp = (FAtom (ABool False) ==) . seConcl -- | True, if the sequents conclusion contains an existentially quantified -- thread. @@ -337,11 +336,11 @@ -- together with the corresponding chain rule. If no typing is given, then it -- tries to infer it from the message sequence chart. theoryOverview :: Theory -> Theory -theoryOverview thy@(Theory name items) = +theoryOverview thy@(Theory name items) = Theory name $ concat [ protoOverview proto | ThyProtocol proto <- items] where - protoOverview proto = - (ThyText "section" $ "Overview of protocol '"++protoName proto++"'") : + protoOverview proto = + (ThyText "section" $ "Overview of protocol '"++protoName proto++"'") : ThyProtocol proto : typInvs where typInvs = case lookupTypeInvariants proto thy of @@ -355,7 +354,7 @@ \(maybe some message patterns are not unifiable)" xs -> concatMap addChainRule xs - addChainRule (item, typ) = + addChainRule (item, typ) = [ item , ThyText "text" $ unlines [ "Note that the chain rule below is only an informal representation of the" diff --git a/src/Scyther/Theory/Parser.hs b/src/Scyther/Theory/Parser.hs --- a/src/Scyther/Theory/Parser.hs +++ b/src/Scyther/Theory/Parser.hs @@ -34,7 +34,7 @@ , genFunApp , funOpen , funApp - + -- ** Security protocol theorys for the free-algebra , protocol , claims @@ -90,7 +90,7 @@ -- -- NOTE: Lexical errors are thrown using 'error'. scanString :: FilePath -> String -> [Token] -scanString filename s = +scanString filename s = case runAlex s gatherUntilEOF of Left err -> error err Right kws -> kws @@ -99,7 +99,7 @@ AlexPn _ line col <- alexGetPos let pos = newPos filename line col k <- alexMonadScan - case k of + case k of EOF -> return [(pos,EOF)] _ -> do kws <- gatherUntilEOF return $ (pos,k) : kws @@ -125,7 +125,7 @@ -- | Parse a term. kw :: Keyword -> Parser s () kw t = token check - where + where check t' | t == t' = Just () | otherwise = Nothing -- | Parse content between keywords. @@ -210,7 +210,7 @@ Left err -> error $ show err -- | Parse a security protocol theory given as a string using the given --- filename for the error messages +-- filename for the error messages parseTheory :: FilePath -> IO Theory parseTheory = parseFile theory () @@ -339,7 +339,7 @@ -- | Resolve all identifiers in the pattern. resolveIds :: S.Set Id -> S.Set Id -> Pattern -> Pattern resolveIds avars mvars = go - where + where resolve = resolveId avars mvars go pt@(PConst _) = pt go pt@(PFresh _) = pt @@ -360,7 +360,7 @@ -- PRE: The role must use disjoint identifiers for fresh messages, agent -- variables, and message variables. resolveIdsLocalToRole :: Role -> Pattern -> Pattern -resolveIdsLocalToRole role = resolveIds (roleFAV role) (roleFMV role) +resolveIdsLocalToRole role = resolveIds (roleFAV role) (roleFMV role) -- Messages @@ -377,13 +377,13 @@ -- | Resolve a thread identifier resolveTID :: MonadPlus m => E.Mapping -> TID -> m Role resolveTID mapping tid = - liftMaybe' ("resolveTID: no role assigned to thread "++show tid) + liftMaybe' ("resolveTID: no role assigned to thread "++show tid) (E.threadRole tid (E.getMappingEqs mapping)) -- | Resolve a local identifier. -- PRE: Thread id must be in the role equalities. resolveLocalId :: MonadPlus m => E.Mapping -> LocalId -> m Message -resolveLocalId mapping (LocalId (i, tid)) = +resolveLocalId mapping (LocalId (i, tid)) = do role <- resolveTID mapping tid return $ inst tid (resolveId (roleFAV role) (roleFMV role) i) `mplus` @@ -395,16 +395,16 @@ role <- resolveTID mapping tid let roleId = roleName role if isPrefixOf roleId stepId - then liftMaybe' ("resolveStep: step '"++stepId++"' not part of role '"++roleName role++"'") + then liftMaybe' ("resolveStep: step '"++stepId++"' not part of role '"++roleName role++"'") (lookupRoleStep (drop (length roleId + 1) stepId) role) else fail ("resolveStep: role of step '"++stepId++"' does not agree to role '" - ++roleName role++"' of thread "++show tid) + ++roleName role++"' of thread "++show tid) -- | Parse an instantiation of a pattern. instantiation :: MonadPlus m => Parser s (E.Mapping -> m Message) -instantiation = do +instantiation = do tid <- TID <$> (funOpen "inst" *> integer <* kw COMMA) - m <- (do i <- identifier + m <- (do i <- identifier let (stepId, iTyp) = splitAt (length i - 3) i when (iTyp /= "_pt") (fail $ "inst: could not resolve pattern '"++i++"'") return $ \mapping -> do @@ -449,7 +449,7 @@ TODO: Update to new syntax Protocol := "protocol" Identifier "{" Transfer+ "}" -Transfer := Identifier "->" Identifier ":" Term +Transfer := Identifier "->" Identifier ":" Term | Identifier "->" ":" Term "<-" Identifier ":" Term | Identifier "<-" ":" Term "->" Identifier ":" Term Term := "{" Term "}" Key @@ -504,36 +504,36 @@ return [(left, Recv lbl pt), (right, Send lbl pt)] ) ) - ) + ) -- | Parse a protocol. protocol :: Parser s Protocol protocol = do - name <- string "protocol" *> identifier + name <- string "protocol" *> identifier transfers <- concat <$> braced (many1 transfer) -- convert parsed transfers into role scripts let roleIds = S.fromList $ map fst transfers roles = do actor <- S.toList roleIds let steps = [ step | (i, step) <- transfers, i == actor ] - return $ Role (getId actor) + return $ Role (getId actor) (ensureFreshSteps actor (S.map addSpacePrefix roleIds) steps) return $ Protocol name roles where addSpacePrefix = Id . (' ':) . getId dropSpacePrefixes = S.map dropSpacePrefix -- | Ensure message variables are received before they are sent. - ensureFreshSteps actor possibleAvars = + ensureFreshSteps actor possibleAvars = go (S.singleton (addSpacePrefix actor)) S.empty S.empty where go _ _ _ [] = [] - go avars mvars fresh (Send l pt : rs) = - let avars' = avars `S.union` (((patFMV pt `S.intersection` possibleAvars) + go avars mvars fresh (Send l pt : rs) = + let avars' = avars `S.union` (((patFMV pt `S.intersection` possibleAvars) `S.difference` mvars) `S.difference` fresh) fresh' = fresh `S.union` ((patFMV pt `S.difference` avars') `S.difference` mvars) pt' = resolveIds (dropSpacePrefixes avars') (dropSpacePrefixes mvars) pt in Send l pt' : go avars' mvars fresh' rs - go avars mvars fresh (Recv l pt : rs) = + go avars mvars fresh (Recv l pt : rs) = let mvars' = mvars `S.union` ((patFMV pt `S.difference` avars) `S.difference` fresh) pt' = resolveIds (dropSpacePrefixes avars) (dropSpacePrefixes mvars') pt in Recv l pt' : go avars mvars' fresh rs @@ -542,23 +542,23 @@ -- Parse Claims ------------------------------------------------------------------------------ --- | Parse a claim. +-- | Parse a claim. claims :: (String -> Maybe Protocol) -> Parser s [ThyItem] claims protoMap = do let mkAxiom (name, se) = ThyTheorem (name, Axiom se) - (multiplicity, mkThyItem) <- - (string "property" *> pure (id, ThySequent)) <|> + (multiplicity, mkThyItem) <- + (string "property" *> pure (id, ThySequent)) <|> (string "properties" *> pure ((concat <$>) . many1, ThySequent)) <|> (string "axiom" *> pure (id, mkAxiom )) protoId <- kw LPAREN *> string "of" *> identifier - proto <- liftMaybe' ("unknown protocol '"++protoId++"'") $ protoMap protoId + proto <- liftMaybe' ("unknown protocol '"++protoId++"'") $ protoMap protoId kw RPAREN multiplicity $ do claimId <- try $ identifier <* kw COLON when ('-' `elem` claimId) (fail $ "hyphen '-' not allowed in property name '"++claimId++"'") let mkThySequent (mkClaimId, se) = mkThyItem (mkClaimId claimId, se) singleSequents = map (liftM (return . (,) id) . ($ proto)) - [ niagreeSequent, secrecySequent, implicationSequent, parseTypingSequent ] + [ agreeSequent, secrecySequent, implicationSequent, parseTypingSequent ] multiSequents = map ($ proto) [ parseNonceSecrecy, parseFirstSends , parseTransferTyping, parseAutoProps ] @@ -569,74 +569,74 @@ -- msc-typing parseAutoProps :: Protocol -> Parser s [(String -> String,Sequent)] parseAutoProps proto = - string "auto" *> kw MINUS *> string "properties" *> + string "auto" *> kw MINUS *> string "properties" *> pure (concat [ transferTyping proto, firstSendSequents proto, nonceSecrecySequents proto ]) -- | Create secrecy claims for nonces and variables. parseNonceSecrecy :: Protocol -> Parser s [(String -> String,Sequent)] -parseNonceSecrecy proto = +parseNonceSecrecy proto = string "nonce" *> kw MINUS *> string "secrecy" *> pure (nonceSecrecySequents proto) -- | Create secrecy claims for nonces and variables. nonceSecrecySequents :: Protocol -> [(String -> String,Sequent)] -nonceSecrecySequents proto = - concatMap mkSequent . toposort $ protoOrd proto +nonceSecrecySequents proto = + concatMap mkSequent . toposort $ protoOrd proto where - mkSequent (step, role) = case step of - Send _ pt -> do - n@(PFresh i) <- S.toList $ subpatterns pt - guard (not (plainUse pt n) && firstUse n) - return $ secrecySe (MFresh . Fresh) i - Recv _ pt -> do - v@(PMVar i) <- S.toList $ subpatterns pt - guard (not (plainUse pt v) && firstUse v) - return $ secrecySe (MMVar . MVar) i - where - (tid, prem0) = freshTID (empty proto) - (prefix, _) = break (step ==) $ roleSteps role - firstUse = (`S.notMember` (S.unions $ map (subpatterns . stepPat) prefix)) - plainUse pt = (`S.member` splitpatterns pt) - avars = [ MAVar (AVar (LocalId (v,tid))) - | (PAVar v) <- S.toList . S.unions . map (subpatterns.stepPat) $ roleSteps role ] - secrecySe constr i = - ( (++("_"++roleName role++"_sec_"++getId i)) - , Sequent prem (FAtom AFalse) - ) - -- flip (Sequent proto) FFalse $ FFacts $ - -- insertEv (Learn (constr (LocalId (i,tid)))) $ - -- insertEv (Step tid step) $ - -- foldr uncompromise (insertRole tid role emptyFacts) avars + mkSequent (step, role) = case step of + Send _ pt -> do + n@(PFresh i) <- S.toList $ subpatterns pt + guard (not (plainUse pt n) && firstUse n) + return $ secrecySe (MFresh . Fresh) i + Recv _ pt -> do + v@(PMVar i) <- S.toList $ subpatterns pt + guard (not (plainUse pt v) && firstUse v) + return $ secrecySe (MMVar . MVar) i where - -- here we know that conjunction will work, as we build it by ourselves - Just (Just prem) = conjoinAtoms atoms prem0 - atoms = [ AEq (E.TIDRoleEq (tid, role)) - , AEv (Step tid step) - , AEv (Learn (constr (LocalId (i, tid)))) - ] ++ map AUncompr avars + (tid, prem0) = freshTID (empty proto) + (prefix, _) = break (step ==) $ roleSteps role + firstUse = (`S.notMember` (S.unions $ map (subpatterns . stepPat) prefix)) + plainUse pt = (`S.member` splitpatterns pt) + avars = [ MAVar (AVar (LocalId (v,tid))) + | (PAVar v) <- S.toList . S.unions . map (subpatterns.stepPat) $ roleSteps role ] + secrecySe constr i = + ( (++("_"++roleName role++"_sec_"++getId i)) + , Sequent prem (FAtom (ABool False)) Standard + ) + -- flip (Sequent proto) FFalse $ FFacts $ + -- insertEv (Learn (constr (LocalId (i,tid)))) $ + -- insertEv (Step tid step) $ + -- foldr uncompromise (insertRole tid role emptyFacts) avars + where + -- here we know that conjunction will work, as we build it by ourselves + Just (Just prem) = conjoinAtoms atoms prem0 + atoms = [ AEq (E.TIDRoleEq (tid, role)) + , AEv (Step tid step) + , AEv (Learn (constr (LocalId (i, tid)))) + ] ++ map AUncompr avars parseFirstSends :: Protocol -> Parser s [(String -> String,Sequent)] parseFirstSends proto = string "first" *> kw MINUS *> string "sends" *> pure (firstSendSequents proto) firstSendSequents :: Protocol -> [(String -> String,Sequent)] -firstSendSequents proto = - concatMap mkRoleSequents $ protoRoles proto +firstSendSequents proto = + concatMap mkRoleSequents $ protoRoles proto where - mkRoleSequents role = - concatMap mkStepSequents $ zip (inits steps) steps - where - steps = roleSteps role - (tid, prem0) = freshTID (empty proto) - mkStepSequents (_, Recv _ _ ) = [] - mkStepSequents (prefix, step@(Send _ pt)) = do - n@(PFresh i) <- S.toList $ splitpatterns pt - guard (n `S.notMember` S.unions (map (subpatterns.stepPat) prefix)) - let learn = (Learn (MFresh (Fresh (LocalId (i, tid))))) - atoms = [ AEq (E.TIDRoleEq (tid, role)), AEv learn ] - Just (Just prem) = conjoinAtoms atoms prem0 - concl = FAtom (AEvOrd (Step tid step, learn)) - return ( (++("_" ++ getId i)), Sequent prem concl) + mkRoleSequents role = + concatMap mkStepSequents $ zip (inits steps) steps + where + steps = roleSteps role + (tid, prem0) = freshTID (empty proto) + mkStepSequents (_, Recv _ _ ) = [] + mkStepSequents (prefix, step@(Send _ pt)) = do + n@(PFresh i) <- S.toList $ splitpatterns pt + guard (n `S.notMember` S.unions (map (subpatterns.stepPat) prefix)) + let learn = (Learn (MFresh (Fresh (LocalId (i, tid))))) + atoms = [ AEq (E.TIDRoleEq (tid, role)), AEv learn ] + Just (Just prem) = conjoinAtoms atoms prem0 + concl = FAtom (AEvOrd (Step tid step, learn)) + return ( (++("_" ++ getId i)), Sequent prem concl Standard) parseTransferTyping :: Protocol -> Parser s [(String -> String, Sequent)] parseTransferTyping proto = @@ -645,7 +645,7 @@ transferTyping :: Protocol -> [(String -> String, Sequent)] transferTyping proto = case mscTyping proto of Just typing -> pure - ((++"_msc_typing"), Sequent (empty proto) (FAtom (ATyping typing))) + ((++"_msc_typing"), Sequent (empty proto) (FAtom (ATyping typing)) Standard) Nothing -> fail "transferTyping: failed to construct typing" -- | Parse secrecy formula. @@ -655,7 +655,7 @@ roleId <- funOpen "secret" *> identifier role <- liftMaybe' ("could not find role '"++roleId++"'") $ lookupRole roleId proto lbl <- kw COMMA *> (identifier <|> kw MINUS *> pure "-") - stepAtoms <- + stepAtoms <- (do step <- liftMaybe $ lookupRoleStep lbl role return $ [AEv (Step tid step)] `mplus` return []) @@ -667,22 +667,23 @@ kw COMMA uncompromised <- map (inst tid . resolveIdsLocalToRole role) <$> msgSet kw RPAREN - -- construct secrecy claim - let atoms = [ AEq (E.TIDRoleEq (tid, role)), AEv (Learn m) ] ++ stepAtoms ++ + -- construct secrecy claim + let atoms = [ AEq (E.TIDRoleEq (tid, role)), AEv (Learn m) ] ++ stepAtoms ++ map AUncompr uncompromised prem = case conjoinAtoms atoms prem0 of Just (Just prem1) -> prem1 Just Nothing -> error "secrecySequent: secrecy claim is trivially true" Nothing -> error "secrecySequent: failed to construct secrecy claim" - - return $ Sequent prem (FAtom AFalse) + + return $ Sequent prem (FAtom (ABool False)) Standard where msgSet = braced $ sepBy pattern (kw COMMA) --- | Parse non-injective agreement claim. -niagreeSequent :: Protocol -> Parser s Sequent -niagreeSequent proto = do - funOpen "niagree" +-- | Parse (non-)injective agreement claim. +agreeSequent :: Protocol -> Parser s Sequent +agreeSequent proto = do + qualifier <- (funOpen "niagree" *> pure Standard) <|> + (funOpen "iagree" *> pure Injective) (roleCom, stepCom, patCom) <- roleStepPattern kw RIGHTARROW (roleRun, stepRun, patRun) <- roleStepPattern @@ -690,12 +691,12 @@ uncompromised <- map (AUncompr . instPat tidCom roleCom) <$> patSet kw RPAREN let premAtoms = [ AEq (E.TIDRoleEq (tidCom, roleCom)) - , AEv (Step tidCom stepCom) - ] ++ + , AEv (Step tidCom stepCom) + ] ++ uncompromised conclAtoms = [ AEq (E.TIDRoleEq (tidRun, roleRun)) - , AEv (Step tidRun stepRun) + , AEv (Step tidRun stepRun) , AEq (E.MsgEq ( instPat tidRun roleRun patRun , instPat tidCom roleCom patCom )) ] @@ -705,11 +706,11 @@ Just Nothing -> error "niagreeSequent: claim is trivially true" Nothing -> error "niagreeSequent: failed to construct claim" - return (Sequent prem concl) + return (Sequent prem concl qualifier) where (tidCom, prem0) = freshTID (empty proto) tidRun = succ tidCom - + patSet = braced $ sepBy pattern (kw COMMA) instPat tid role = inst tid . resolveIdsLocalToRole role @@ -723,11 +724,11 @@ parseTypingSequent :: Protocol -> Parser s Sequent parseTypingSequent proto = do typ <- M.fromList <$> doubleQuoted (many1 typeAssertion) - return $ Sequent (empty proto) (FAtom (ATyping typ)) + return $ Sequent (empty proto) (FAtom (ATyping typ)) Standard where variable = (,) <$> (Id <$> identifier) <*> (kw AT *> roleById proto) - typeAssertion = (,) <$> (variable <* kw COLON <* kw COLON) + typeAssertion = (,) <$> (variable <* kw COLON <* kw COLON) <*> (normType <$> msgTypeDisj) msgTypeTup = foldr1 TupT <$> sepBy1 msgTypeDisj (kw COMMA) @@ -735,7 +736,7 @@ msgType = asum [ pure AgentT <* string "Agent" - , (ConstT . Id) <$> singleQuoted identifier + , (ConstT . Id) <$> singleQuoted identifier , HashT <$> funApp "h" msgTypeTup , EncT <$> braced msgTypeTup <*> msgType , SymKT <$> (funOpen "k" *> msgTypeDisj) <*> (kw COMMA *> msgTypeDisj <* kw RPAREN) @@ -760,11 +761,11 @@ roleStepById proto = do stepId <- identifier let (lbl, roleId) = (reverse *** (init . reverse)) (break ('_' ==) $ reverse stepId) - role <- liftMaybe' ("could not find role '" ++ roleId ++ + role <- liftMaybe' ("could not find role '" ++ roleId ++ "' in protocol '" ++ protoName proto ++ "'") (lookupRole roleId proto) - step <- liftMaybe' ("unknown label '" ++ lbl ++ "' in role '" ++ roleId ++ "'") + step <- liftMaybe' ("unknown label '" ++ lbl ++ "' in role '" ++ roleId ++ "'") (lookupRoleStep lbl role) return (role, step) @@ -849,13 +850,13 @@ -- | Parse a raw fact. rawFacts :: MonadPlus m => Parser s [RawFact m] -rawFacts = foldl1 (<|>) - ( [try orderFacts, honestFact] ++ +rawFacts = foldl1 (<|>) + ( [try orderFacts, honestFact] ++ map (liftM return) [roleEqFact, knowsFact, stepFact, eqFact] ) -- | Parse the conclusion "False". falseConcl :: Parser s Formula -falseConcl = doubleQuoted (string "False" *> pure (FAtom AFalse)) +falseConcl = doubleQuoted (string "False" *> pure (FAtom (ABool False))) -- | Parse a conclusion stating existence of some threads of a specific -- structure. @@ -870,9 +871,9 @@ return $ foldr FExists (foldr1 FConj . map FAtom $ atoms) tids where singleThread = pure <$> (strings ["a", "thread"] *> integer) - multiThreads = strings ["threads"] *> sepBy1 integer (kw COMMA) - threads = (singleThread <|> multiThreads) <* strings ["such","that"] - + multiThreads = strings ["threads"] *> sepBy1 integer (kw COMMA) + threads = (singleThread <|> multiThreads) <* strings ["such","that"] + -- | Parse a conclusion. -- currently only contradiction supported conclusion :: Protocol -> E.Mapping -> Parser s Formula @@ -881,7 +882,7 @@ -- | Parse a general implication claim. implicationSequent :: Protocol -> Parser s Sequent -implicationSequent proto = do +implicationSequent proto = do facts <- concat <$> (string "premises" *> many (doubleQuoted rawFacts)) roleeqs <- extractRoleEqs proto facts let mapping = foldr (uncurry E.addTIDRoleMapping) (E.Mapping E.empty) roleeqs @@ -893,7 +894,7 @@ prems <- maybe (fail "contradictory premises") return optPrems string "imply" concl <- conclusion proto mapping - return $ Sequent prems concl + return $ Sequent prems concl Standard {- -- | Construct the premise modifier. The given set of role equalities is used @@ -901,14 +902,14 @@ mkPremiseMod :: MonadPlus m => E.Mapping -> [RawFact m] -> Facts -> m Facts mkPremiseMod mapping rawfacts facts = do atoms <- sequence [ mkAtom mapping | RawAtom mkAtom <- rawfacts ] - optFacts <- conjoinAtoms atoms facts + optFacts <- conjoinAtoms atoms facts maybe (error "mkPremiseMod: contradictory facts") return $ optFacts -} -- | A formal comment; i.e., (header, body) formalComment :: Parser s (String, String) formalComment = - (,) <$> text begin + (,) <$> text begin <*> (concat <$> many (text content) <* text end) where text f = token (\t -> case t of TEXT ty -> f ty; _ -> mzero) @@ -920,11 +921,11 @@ end _ = mzero - ------------------------------------------------------------------------------ + ------------------------------------------------------------------------------ -- Parse a theory - ------------------------------------------------------------------------------ + ------------------------------------------------------------------------------ - + -- | Parse a theory. theory :: Parser s Theory theory = do @@ -933,7 +934,7 @@ string "begin" *> addItems (Theory thyId []) <* string "end" where addItems :: Theory -> Parser s (Theory) - addItems thy = + addItems thy = do p <- protocol case lookupProtocol (protoName p) thy of Just _ -> fail $ "duplicate protocol '" ++ protoName p ++ "'" diff --git a/src/Scyther/Theory/Pretty.hs b/src/Scyther/Theory/Pretty.hs --- a/src/Scyther/Theory/Pretty.hs +++ b/src/Scyther/Theory/Pretty.hs @@ -21,11 +21,13 @@ import Control.Monad.State import Control.Monad.Reader +import Extension.Prelude (sortednub) + import Text.Isar import Text.Dot (Dot) import qualified Scyther.Equalities as E -import Scyther.Facts +import Scyther.Facts import Scyther.Sequent import Scyther.Proof import Scyther.Theory @@ -55,8 +57,8 @@ nest = liftA2 nest . pure caseEmptyDoc = liftA3 caseEmptyDoc - + ------------------------------------------------------------------------------ -- A type-tagging identity monad transformer ------------------------------------------------------------------------------ @@ -65,7 +67,7 @@ deriving( Functor, Applicative, Monad ) instance MonadTrans (TaggedIdentityT t) where - lift = TaggedIdentityT + lift = TaggedIdentityT runTaggedIdentityT :: t -> TaggedIdentityT t m a -> m a runTaggedIdentityT _ = unTaggedIdentityT @@ -82,7 +84,7 @@ theoremRef :: Document d => Protocol -> String -> m d theoremDef :: Document d => Theorem -> m d -> m d keyword :: Document d => String -> m d -> m d - noteCases :: Document d => Dot a + noteCases :: Document d => Dot a -> [(String, Dot b)] -- ^ named non-trivial cases -> [(String, Dot b)] -- ^ named trivial cases -> m d -> m d @@ -110,6 +112,7 @@ prettyTrivial :: TrivReason -> m Doc prettyMissing :: Sequent -> String -> m Doc prettySaturate :: Sequent -> m Doc + prettyReduceInjectivity :: m Doc -> m Doc prettyForwardContradiction :: m Doc -> m Doc prettyForwardResolution :: m Doc -> Sequent -> E.Mapping -> m Doc prettyNextCase :: m Doc @@ -140,7 +143,7 @@ --------------- explainSequent :: Sequent -> String -explainSequent = +explainSequent = render . runIdentity . runTaggedIdentityT SlimOutput . prettySequent withExplainedSequent :: (Document d, MarkupMonad m) => Sequent -> m d -> m d @@ -167,29 +170,36 @@ extractTrivial (Trivial se reason) = case reason of TrivContradictoryPremises -> Just reason TrivLongTermKeySecrecy _ -> Nothing - TrivPremisesImplyConclusion -> - case seConcl se of + TrivPremisesImplyConclusion -> + case seConcl se of FAtom (AHasType _) -> Just reason _ -> Nothing extractTrivial _ = Nothing -- | Pretty print a sequent with quantifiers, logical, and meta-logical facts for -- the premise and a single document representing the conclusion. -prettySequentParts :: PrettyMonad m => Sequent -> m (([Doc], [Doc], [Doc]), Doc) -prettySequentParts (Sequent prem concl) = do - ppPrem <- prettyFacts prem - ppConcl <- prettyFormula (eqsToMapping prem) concl - return (ppPrem, ppConcl) +prettySequentParts :: PrettyMonad m + => Sequent + -> m (([Doc], [Doc], [Doc]), SequentQualifier, Doc) +prettySequentParts (Sequent prem concl qualifier) = do + ppPrem <- prettyFacts prem + ppConcl <- prettyFormula (eqsToMapping prem) concl + return (ppPrem, qualifier, ppConcl) +-- | Pretty-print a sequent qualifier. +prettySequentQualifier :: PrettyMonad m => SequentQualifier -> m Doc +prettySequentQualifier Standard = emptyDoc +prettySequentQualifier Injective = text "injectively" + -- | Pretty print a proof. -prettyProof :: PrettyMonad m => +prettyProof :: PrettyMonad m => String -- ^ Name of the theorem that is proven -> (Bool, Bool) -- ^ (facts are loaded, thesis is being proven) - -> Proof + -> Proof -> m Doc prettyProof _ _ (Axiom _) = emptyDoc -prettyProof _ prfConf (Trivial _ reason) = +prettyProof _ prfConf (Trivial _ reason) = ensureProofMode prfConf <-> prettyTrivial reason prettyProof _ _ (Missing se reason showSequent) @@ -204,15 +214,20 @@ withProofSequent prf (prettySaturate se) $-$ prettyProof thName (True, False) prf +prettyProof thName prfConf (RuleApp _ ReduceInjectivity [prf]) = + withFactsMode prfConf $ + withProofSequent prf $ + prettyReduceInjectivity $ prettyProof thName (True, False) prf + -- A forward resolution that lead to no further proofs prettyProof _ prfConf (RuleApp se (ForwardResolution (thName, _) _) []) = - ensureProofMode prfConf <-> + ensureProofMode prfConf <-> prettyForwardContradiction (theoremRef (seProto se) thName) -- a forward resolution with a single successor. prettyProof outerThName prfConf (RuleApp se (ForwardResolution (thName, thSe) tideqs) [prf]) = wrapper $ - withProofSequent prf - (prettyForwardResolution (theoremRef (seProto se) thName) thSe tideqs) $-$ + withProofSequent prf + (prettyForwardResolution (theoremRef (seProto se) thName) thSe tideqs) $-$ prettyProof outerThName newMode prf where isTyping = isTypingFormula . seConcl $ thSe @@ -234,7 +249,7 @@ $-$ vcat (intersperse prettyNextCase (map (pure . nest 2) ppCases)) $-$ prettyChainRuleQED m trivialCases - where + where selectCase (info, prf) = withProofSequent prf (prettyChainRuleCase info) $-$ prettyProof thName (True, False) prf @@ -243,14 +258,14 @@ let mkDot = dotSequentMarked S.empty . prfSequent nonTrivialCases = zip names $ map mkDot prfs noteCases (dotSequentMarked S.empty se) nonTrivialCases [] - (withExplanation (explainSequent se) pre) + (withExplanation (explainSequent se) pre) $-$ modifier (vcat . intersperse prettyNextCase $ map (nest 2 . pure) ppCases) $-$ post where (pre, modifier, post) = prettyTypeCheckInduction thName ppCase (name, prf) = - let caseDoc = prettyTypingCase thName name + let caseDoc = prettyTypingCase thName name in withProofSequent prf caseDoc $-$ prettyProof thName (True, True) prf prettyProof thName _ (RuleApp se (SplitEq eq@(MShrK _ _, MShrK _ _) [True,True]) prfs) = do @@ -260,20 +275,20 @@ prettySplitEqQed where ppCase (name, prf) = - withProofSequent prf (prettySplitEqCase name) $-$ + withProofSequent prf (prettySplitEqCase name) $-$ prettyProof thName (True, False) prf prettyProof _ _ (RuleApp _ rule _) = error $ "prettyProof: unmatched rule\n" ++ show rule - + -- | Pretty print a theory item. -- -- Note that this also ensures that quantifiers are made unique. prettyThyItem :: PrettyMonad m => [ThyItem] -> ThyItem -> m Doc -prettyThyItem items (ThyProtocol proto) = prettyProtoDef proto +prettyThyItem items (ThyProtocol proto) = prettyProtoDef proto [th | ThyTheorem th <- items, isAxiom th, thmProto th == proto] -prettyThyItem _ (ThySequent (name, se)) = +prettyThyItem _ (ThySequent (name, se)) = prettyTheorem (name, Missing (uniqueTIDQuantifiers se) ("proof to be done") False) -prettyThyItem _ (ThyTheorem (name, prf)) = +prettyThyItem _ (ThyTheorem (name, prf)) = prettyTheorem (name, prf) prettyThyItem _ (ThyText header txt) = prettyFormalComment header txt @@ -287,8 +302,8 @@ prettySoundness :: Applicative f => Theory -> f Doc prettySoundness thy = case unsoundTheorems thy of [] -> emptyDoc - ths -> vcat $ - map text ["", "(* NOTE that the proofs of the following theorems are UNSOUND:", ""] ++ + ths -> vcat $ + map text ["", "(* NOTE that the proofs of the following theorems are UNSOUND:", ""] ++ map ppThm ths ++ map text ["*)"] where @@ -317,7 +332,7 @@ withExplanation e = TaggedIdentityT . withExplanation e . unTaggedIdentityT theoremRef proto = lift . theoremRef proto theoremDef thm = TaggedIdentityT . theoremDef thm . unTaggedIdentityT - keyword tag = TaggedIdentityT . keyword tag . unTaggedIdentityT + keyword tag = TaggedIdentityT . keyword tag . unTaggedIdentityT noteCases se ntc tc = TaggedIdentityT . noteCases se ntc tc . unTaggedIdentityT @@ -329,7 +344,7 @@ isaTactic :: TrivReason -> String isaTactic TrivContradictoryPremises = "((clarsimp, order?) | order)" isaTactic (TrivLongTermKeySecrecy _) = "(fastsimp dest!: ltk_secrecy)" -isaTactic TrivPremisesImplyConclusion = "(fastsimp intro: event_predOrdI split: if_splits)" +isaTactic TrivPremisesImplyConclusion = "(fastsimp intro: event_predOrdI split: if_splits)" -- | Isabelle proof of long-term key secrecy. isaLongTermKeySecrecyProof :: Protocol -> Doc @@ -346,8 +361,8 @@ isaSequentProp :: MarkupMonad m => Sequent -> ReaderT IsarConf m Doc isaSequentProp se = do conf <- ask - ( (premTids, ppPremFacts, _), ppConcl ) <- prettySequentParts se - let quantify q vs = case vs of + ( (premTids, ppPremFacts, _), _qualifier, ppConcl ) <- prettySequentParts se + let quantify q vs = case vs of [] -> id _ -> ((q conf <> fsep vs <> char '.') $$) . nest 2 doc | nullFacts (sePrem se) = ppConcl @@ -389,7 +404,7 @@ -- where -- singleFact f = return ([], [f], []) prettySequent se = do - ( (_, ppPremFacts, _), ppConcl) <- prettySequentParts se + ( (_, ppPremFacts, _), _qualifier, ppConcl) <- prettySequentParts se let doc | nullFacts (sePrem se) = doubleQuotes ppConcl | otherwise = text "assumes facts:" $-$ @@ -398,7 +413,7 @@ pure doc -- proof output ensureProofMode (factsLoaded, proofMode) = - (if proofMode then emptyDoc else text "thus ?thesis") <-> + (if proofMode then emptyDoc else text "thus ?thesis") <-> (if factsLoaded then emptyDoc else text "using facts") withFactsMode (_, proofMode) doc @@ -411,6 +426,39 @@ prettySaturate _ = text "note_prefix_closed facts = facts" + -- NOTE: Proof script works only for two-party authentication. + prettyReduceInjectivity inner = + ask >>= pp + where + pp conf = vcat + [ lbrace + , nest 2 $ vcat + [ text "fix tid0 tid1" + , text "assume facts: \"?prems tid0\"" + , text "have \"" <-> isaExists conf <> text "tid1. ?concs tid0 tid1\"" + , text "proof -" + , nest 2 $ vcat + [ text "note_unified facts = facts" + , inner + ] + , text "qed" + ] + , rbrace + , text "note niagree = this" + , lbrace + , nest 2 $ vcat + [ text "fix i1 i2 j" + , text "assume \"?concs i1 j" <-> isaAnd conf <-> text "?concs i2 j\"" + , text "note_unified facts = this" + , text "have \"i1 = i2\" using facts by simp" + ] + , rbrace + , text "note conc_inj = this" + , text "show ?thesis" + , text " by (fast intro!: iagree_to_niagree elim!: niagree conc_inj)" + ] + + prettyForwardContradiction thRef = kwBy <-> text "(fastsimp dest:" <-> thRef <-> text "intro: event_predOrdI)" prettyForwardResolution thRef thSe mapping @@ -418,20 +466,20 @@ | otherwise = do conf <- ask let mappedPrems = applyMapping mapping $ sePrem thSe - ppPrems = zip [1..] . map (isaAtom conf (eqsToMapping mappedPrems)) $ + ppPrems = zip [1..] . map (isaAtom conf (eqsToMapping mappedPrems)) $ toAtoms mappedPrems - ppPremProve (i, premFact) = + ppPremProve (i, premFact) = text "have f" <> int i <> colon <-> doubleQuotes premFact <-> text "using facts by (auto intro: event_predOrdI)" ppProven = pure . vcat $ map ppPremProve ppPrems - ppResolve = - thRef <> text "[OF" <> (hcat $ map ((text " f" <>) . int . fst) ppPrems) <> + ppResolve = + thRef <> text "[OF" <> (hcat $ map ((text " f" <>) . int . fst) ppPrems) <> text ", simplified]" ppProven $-$ kwNote <-> text ("facts = facts") <-> ppResolve prettyNextCase = kwNext - prettyChainRuleSplitCases = return . fst . genericChainRuleSplitCases snd + prettyChainRuleSplitCases = return . fst . genericChainRuleSplitCases snd prettyChainRuleApplication m = sep [ kwProof <> text "(sources! \"", nest 4 m <-> text "\")"] prettyChainRuleCase (name, newVars) = @@ -444,25 +492,25 @@ | otherwise = parens $ text name <-> hsep (map ppNewVar newVars) prettyChainRuleQED _ trivCases | null tactics = kwQED <-> text "(insert facts, fastsimp+)?" -- be conservative - | otherwise = + | otherwise = kwQED <-> text "(insert facts, (" <> hsep (intersperse (text "|") tactics) <> text ")+)?" where tactics = map text . nub . map isaTactic . snd $ genericChainRuleSplitCases snd trivCases - prettyTypeCheckInduction typName = + prettyTypeCheckInduction typName = ( kwProof <-> text "-" $$ ( nest 2 $ vcat - [ text "have" <-> doubleQuotes + [ text "have" <-> doubleQuotes (text "(t,r,s)" <-> (isaIn <$> ask) <-> text wellTypedStates) , kwProof <> text "(cases rule: reachable_in_approxI_ext" - , text " [OF" <-> text monoTyp <> text ", completeness_cases_rule])" + , text " [OF" <-> text monoTyp <> text ", completeness_cases_rule])" ] ) , nest 2 , (nest 2 $ vcat [ kwQED , text "thus" <-> doubleQuotes (text (typingLocale typName) <-> text "t r s") <-> - text "by unfold_locales auto" + text "by unfold_locales auto" ] ) $$ kwQED ) @@ -474,10 +522,10 @@ kwCase <-> text ("("++ name ++" t r s") <-> prettyTID 0 <> text") note facts = this" $-$ text ("then interpret state: "++ typingLocale typName ++" t r s") $-$ nest 2 (text "by unfold_locales auto") $-$ - text "show ?case using facts" + text "show ?case using facts" -- equality splitting - prettySplitEqCase name = + prettySplitEqCase name = text "case" <-> text name <-> text "note_unified facts = this facts" prettySplitEqApplication eq = @@ -488,59 +536,63 @@ (text "thus ?thesis proof(cases rule: Kbd_cases)") prettySplitEqQed = text "qed (fastsimp+)?" - + -- theory output prettyComment comment = text "(*" <-> text comment <-> text "*)" - prettyFormalComment header comment = + prettyFormalComment header comment = text "(*" <-> text header <> colon <-> text comment <-> text "*)" - prettyProtoDef proto axioms = + prettyProtoDef proto axioms = withGraph (dotProtocol proto) $ (isar <$> ask <*> pure proto) $-$ text "" $-$ (text restrictedLocaleDecl) $-$ (nest 2 . vcat . map ppAxiom $ axioms) where - restrictedLocaleDecl = concat + restrictedLocaleDecl = concat [ "locale ", restrictedStateLocale proto, " = "++stateLocale proto , if null axioms then "" else " +" ] - ppAxiom axiom = - text "assumes" <-> text (thmName axiom) <> colon $-$ + ppAxiom axiom = + text "assumes" <-> text (thmName axiom) <> colon $-$ (nest 2 . doubleQuotes . isaSequentProp $ thmSequent axiom) - prettyTheorem th@(name, prf) + prettyTheorem th@(name, prf) | isAxiom th = emptyDoc - | otherwise = case destTypingFormula (seConcl se) of + | otherwise = case destTypingFormula (seConcl se) of Just typ -> ppTypingLocale typ - Nothing -> ppLemma + Nothing -> ask >>= ppLemma where - p = prfProto prf - se = prfSequent prf - ppPrf = prettyProof name (False, True) prf - - -- pretty print a lemma - ppLemma = ppProp $-$ ppPrf - where - locale = "(in " ++ restrictedStateLocale (seProto $ prfSequent prf) ++ ") " - ppName = keyword "property" (text "lemma") <-> text (locale ++ name ++ ":") - ppProp = withProofSequent prf $ - theoremDef th ppName $-$ nest 2 (prettySequent $ prfSequent prf) - -- pretty print a typing locale definition - ppTypingLocale typ = do - conf <- ask - vcat - [ keyword "property" (text "type_invariant") <-> - text name <-> - text "for" <-> text (protoName p) - , text "where \"" <> text name <-> text "= mk_typing" $$ - nest 2 (pure $ isar conf typ) <> char '"' - , text "" - , keyword "property" (text "sublocale") <-> - text (stateLocale p) <-> isaSublocale conf <-> text (typingLocale name) - , ppPrf - , text "" - , pure $ isaLongTermKeySecrecyProof p - ] + p = prfProto prf + se = prfSequent prf + ppPrf = prettyProof name (False, True) prf + -- pretty print a lemma + ppLemma conf = + ppProp $-$ ppPrf + where + locale = "(in " ++ restrictedStateLocale (seProto $ prfSequent prf) ++ ") " + ppName = keyword "property" (text "lemma") <-> text (locale ++ name ++ ":") + ppProp = withProofSequent prf $ theoremDef th ppName $-$ + case seQualifier se of + Standard -> nest 2 (prettySequent se) + Injective -> nest 2 (pure $ isaInjectivitySequent conf se) + + -- pretty print a typing locale definition + ppTypingLocale typ = do + conf <- ask + vcat + [ keyword "property" (text "type_invariant") <-> + text name <-> + text "for" <-> text (protoName p) + , text "where \"" <> text name <-> text "= mk_typing" $$ + nest 2 (pure $ isar conf typ) <> char '"' + , text "" + , keyword "property" (text "sublocale") <-> + text (stateLocale p) <-> isaSublocale conf <-> text (typingLocale name) + , ppPrf + , text "" + , pure $ isaLongTermKeySecrecyProof p + ] + prettyTheoryDef name body = text "theory" <-> doubleQuotes (text name) $-$ text "imports" $-$ @@ -552,6 +604,45 @@ imports = ["../ESPLogic"] +-- | Pretty-print an injectivity sequent. Works only for two-party +-- authentication; i.e., sequents that have one TID in the premise and one +-- additional, existentially quantified TID in the conclusion. +isaInjectivitySequent :: IsarConf -> Sequent -> Doc +isaInjectivitySequent conf se = + doubleQuotes ( + vcat [ text "let" + , nest 2 (sep [text "prems =", nest 2 $ ppPrems <> semi]) + , nest 2 (sep [text "concs =", nest 2 $ ppConcs]) + , text "in" <-> + isaExists conf <> text "f. inj_on f prems" <-> isaAnd conf <-> + parens ( isaForall conf <> text "i. prems i" <-> + isaImplies conf <-> text "concs i (f i)" ) + ] + ) $-$ + text "(is \"let prems = ?prems; concs = ?concs in ?P prems concs\")" + where + premFormula = toFormula $ sePrem se + premTIDs = sortednub $ formulaTIDs premFormula + premMapping = extendMapping premTIDs premFormula E.emptyMapping + ppPrems = abstract premMapping premTIDs premFormula + + (concTIDs0, concFormula) = dropTIDs [] $ seConcl se + concTIDs = premTIDs ++ filter (not . (`elem` premTIDs)) concTIDs0 + concMapping = extendMapping concTIDs0 concFormula premMapping + ppConcs = abstract concMapping concTIDs concFormula + + abstract mapping tids fm = parens $ sep + [ isaLambda conf <> hsep (map (isar conf) tids) <> text "." + , nest 2 (isaFormula conf mapping fm) + ] + + extendMapping tids fm mapping = foldr ($) mapping $ + [ maybe id (E.addTIDRoleMapping tid) (findRole tid fm) | tid <- tids ] + + dropTIDs tids (FExists (Left tid) fm) = dropTIDs (tid : tids) fm + dropTIDs tids fm = (reverse tids, fm) + + -- Slim Pretty Printing ----------------------- @@ -564,20 +655,21 @@ prettyTID = pure . sptTID prettyArbMsgId = pure . sptArbMsgId prettyMessage = pure . sptMessage - prettyFacts = pure . sptFacts + prettyFacts = pure . sptFacts prettyFormula mapping form = pure $ sptFormula mapping form -- case form of -- FFalse -> singleFact $ text "False" -- FFacts facts -> pure $ sptFacts moreRoleEqs facts -- FHasType lid Nothing -> singleFact $ text "weakly-atomic" <> parens (sptLocalId lid) - -- FHasType lid (Just ty) -> + -- FHasType lid (Just ty) -> -- singleFact $ text "hasType" <> parens (sptLocalId lid <> comma <-> sptType sptRoleStep ty) -- FTyping Nothing -> singleFact $ text "weakly-atomic" -- FTyping (Just typing) -> singleFact $ sptTyping typing -- where -- singleFact f = return ([], [f], []) prettySequent se = do - ( (premQuantified, ppPremRepr, ppPremNonRepr), ppConclRaw) <- prettySequentParts se + ((premQuantified, ppPremRepr, ppPremNonRepr), qualifier, ppConclRaw) + <- prettySequentParts se let ppPremFacts = ppPremRepr ++ ppPremNonRepr premQuantifier = pure $ case premQuantified of [] -> text "premises" @@ -587,31 +679,34 @@ | otherwise = premQuantifier $-$ (nest 2 . vcat $ map (kwFact . pure . doubleQuotes) ppPremFacts) $-$ - (sep [text "imply", nest 2 ppConcl]) + (sep [ text "imply" <-> prettySequentQualifier qualifier + , nest 2 ppConcl]) doc -- proof output ensureProofMode _ = emptyDoc withFactsMode _ = id prettyTrivial reason = case reason of TrivPremisesImplyConclusion -> text "tautology" - TrivLongTermKeySecrecy key -> + TrivLongTermKeySecrecy key -> text "contradicts secrecy of" <-> pure (sptMessage key) _ -> emptyDoc - prettyMissing se reason = + prettyMissing se reason = nestShort' "(*" "*)" (text reason $-$ prettySequent se) prettySaturate _ = keyword "proof" $ text "saturate" + prettyReduceInjectivity inner = + keyword "proof" (text "reduce_injectivity") $-$ inner prettyForwardContradiction thRef = text "contradictory due to '" <> thRef <> text "'" - prettyForwardResolution thRef _ mapping = + prettyForwardResolution thRef _ mapping = keyword "proof" (text "resolve") <-> text "'" <> thRef <> ppMapping where ppMapping | null (E.toAnyEqs (E.getMappingEqs mapping)) = emptyDoc | otherwise = text "' mapping" <-> ppTidEqs - ppTidEqs = pure . hsep . punctuate comma . map E.sptAnyEq . E.toAnyEqs $ + ppTidEqs = pure . hsep . punctuate comma . map E.sptAnyEq . E.toAnyEqs $ E.getMappingEqs mapping prettyNextCase = kwNext - prettyChainRuleSplitCases = return . fst . genericChainRuleSplitCases snd - prettyChainRuleApplication m = - sep [ keyword "proof" (text "sources") <> lparen, + prettyChainRuleSplitCases = return . fst . genericChainRuleSplitCases snd + prettyChainRuleApplication m = + sep [ keyword "proof" (text "sources") <> lparen, nest 4 (m <-> rparen)] prettyChainRuleCase (name, newVars) = kwCase <-> selector @@ -632,14 +727,14 @@ prettySplitEqCase name = text "case" <-> text name prettySplitEqApplication eq = - sep [ keyword "proof" (text "split") <> lparen, + sep [ keyword "proof" (text "split") <> lparen, nest 4 (pure $ E.sptAnyEq (E.MsgEq eq) <-> rparen)] prettySplitEqQed = text "qed" - + -- theory output prettyComment comment = text "/*" <-> text comment <-> text "*/" - prettyFormalComment header comment = + prettyFormalComment header comment = text (header ++ "{*") <> text comment <> text "*}" prettyProtoDef proto _ = withGraph (dotProtocol proto) (pure $ sptProtocol proto) @@ -648,19 +743,19 @@ withProofSequent prf ppProp $-$ ppPrf where p = prfProto prf - thmType | isAxiom th = "axiom" + thmType | isAxiom th = "axiom" | otherwise = "property" - ppName = keyword "property" (text thmType) <-> + ppName = keyword "property" (text thmType) <-> text ("(of "++protoName p++") "++name++":") ppProp = theoremDef th ppName $-$ nest 2 (prettySequent $ prfSequent prf) ppPrf = prettyProof name (False, True) prf prettyTheoryDef name body = vcat [ - keyword "theory" (text "theory") <-> text name <-> + keyword "theory" (text "theory") <-> text name <-> keyword "theory" (text "begin") , text "" , pure body - , text "" + , text "" , keyword "theory" (text "end") ] kwFact :: (MarkupMonad m, Document d) => m d -> m d @@ -693,7 +788,7 @@ isar conf se = runReader (prettySequent se) conf instance Isar Proof where isar conf prf = runReader (prettyProof "" (False, True) prf) conf - + -- instance Isar Theorem where -- isar conf thm = runReader (prettyTheorem thm Nothing) conf diff --git a/src/Text/Isar.hs b/src/Text/Isar.hs --- a/src/Text/Isar.hs +++ b/src/Text/Isar.hs @@ -22,7 +22,10 @@ , isaRBrack , isaMetaAll , isaExists + , isaForall + , isaLambda , isaAnd + , isaImplies , isaNotIn , isaIn , isaSubsetEq @@ -50,14 +53,14 @@ import Text.PrettyPrint.Class -- | The ISAR style to be used for output. -data IsarStyle = - PlainText +data IsarStyle = + PlainText | XSymbol deriving( Eq, Show ) -- | The configuration to be used for output. Apart from the ISAR style, the -- configuration also stores the representation of the reachable state of the --- protocol which we are reasoning about. +-- protocol which we are reasoning about. data IsarConf = IsarConf { isarStyle :: IsarStyle , isarTrace :: Doc -- ^ The ISAR code of the trace @@ -68,14 +71,14 @@ -- | Default configuration: plaintext ISAR style and reachable state @(t,r,s)@. defaultIsarConf :: IsarConf -defaultIsarConf = IsarConf PlainText (char 't') (char 'r') (char 's') +defaultIsarConf = IsarConf PlainText (char 't') (char 'r') (char 's') -- | Check if the plaintext style was chosen. isPlainStyle :: IsarConf -> Bool isPlainStyle = (PlainText ==) . isarStyle --- | Values that can be output as ISAR code. +-- | Values that can be output as ISAR code. -- -- Minimal definition: 'isar' class Isar a where @@ -117,7 +120,7 @@ -- | Nest document between two strings and indent body by @length lead + 1@. nestShort' :: Document d => String -> String -> d -> d -nestShort' lead finish = +nestShort' lead finish = nestShort (length lead + 1) (text lead) (text finish) -- | Like 'nestShort' but doesn't print the lead and finish, if the document is @@ -129,7 +132,7 @@ -- | Like 'nestShort'' but doesn't print the lead and finish, if the document is -- empty. nestShortNonEmpty' :: Document d => String -> String -> d -> d -nestShortNonEmpty' lead finish = +nestShortNonEmpty' lead finish = nestShortNonEmpty (length lead + 1) (text lead) (text finish) -- | Output text with a fixed width: if it is smaller then nothing happens, @@ -138,7 +141,7 @@ fixedWidthText n cs | length cs <= n = text cs | otherwise = text as <> zeroWidthText bs - where + where (as,bs) = splitAt n cs -- | Print string as symbol having width 1. @@ -149,13 +152,13 @@ -- separator. numbered :: Document d => d -> [d] -> d numbered _ [] = emptyDoc -numbered vsep ds = +numbered vsep ds = foldr1 ($-$) $ intersperse vsep $ map pp $ zip [(1::Int)..] ds where n = length ds nWidth = length (show n) pp (i, d) = text (flushRight nWidth (show i)) <> d - + -- | Number a list of documents with numbers terminated by "." and vertically -- separate using an empty line. numbered' :: Document d => [d] -> d @@ -169,8 +172,8 @@ -- | Isabelle representation of the exeuction system state of our operational -- semantics. isaExecutionSystemState :: IsarConf -> Doc -isaExecutionSystemState conf = - parens . hcat . punctuate comma $ +isaExecutionSystemState conf = + parens . hcat . punctuate comma $ [isarTrace conf, isarPool conf, isarSubst conf] @@ -245,12 +248,30 @@ | isPlainStyle conf = text "? " | otherwise = symbol "\\" +-- | The forall symbol: @!@ +isaForall :: Document d => IsarConf -> d +isaForall conf + | isPlainStyle conf = text "! " + | otherwise = symbol "\\" + +-- | The lambda symbol: @%@ +isaLambda :: Document d => IsarConf -> d +isaLambda conf + | isPlainStyle conf = text "% " + | otherwise = symbol "\\" + -- | The logical and symbol: @&@ isaAnd :: Document d => IsarConf -> d isaAnd conf | isPlainStyle conf = text "&" | otherwise = symbol "\\" +-- | The logical and symbol: @-->@ +isaImplies :: Document d => IsarConf -> d +isaImplies conf + | isPlainStyle conf = text "-->" + | otherwise = symbol "\\" + -- | The non-strict subset symbol. isaSubsetEq :: Document d => IsarConf -> d isaSubsetEq conf @@ -291,7 +312,7 @@ -- | A generic text command. genTextCmd :: String -> String -> Doc -genTextCmd name content = +genTextCmd name content = sep [text name <> text "{*", nest 2 (fsep . map text $ words content), text "*}"] chapter = genTextCmd "chapter"