Expi2Java Tutorial
Contents
1. 17 host any x listens on all hosts x 18 port 1234 19 20 21 config PSNonceCfg extends NonceCfg 22 size 8 23 24 25 config PSKeyStoreCfg extends KeyStoreChCfg 26 keystore_filename key store 27 28 29 30 typedef PSNonce Int PSNonceCfg 31 32 typedef Bobld ConstStr BobldCfg 33 11 34 35 36 37 38 39 40 41 42 43 44 45 46 Oo oN Aa BP WYN HB e e rn H e N Ee O 15 16 LT 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 typedef PSKey SymKey AES lt Top gt typedef PSKStoreRequest Channel PSKeyStoreCfg lt Top gt to send a request gt typedef PSKStoreAnswer Channel PSKeyStoreCfg lt PSKey gt x to receive a key x config UserPrompt extends ConstStrCfg message Please enter the message typedef PromptMsg ConstStr UserPrompt typedef Msg1 Identifier PSNonce typedef Msg2Plain PSNonce PSNonce Bobld typedef Msg2 SymEnc AES lt Msg2Plain gt typedef Msg3Plain PSNonce String typedef Msg3 SymEnc AES lt Msg3Plain gt Listing 23 Perrig Song mutual authentication protocol perrigsong exdef x Perrig Song mutual authentication protocol x http ww cs l sri com users millen capsl examples html x http sparrow ece cmu edu adrian projects protgen csfw csfw pdf x eXpi version x 1 A gt B alice Na 2 B gt A2. typedef Bobld ConstStr BobldCfg typedef Msgl ldentifier PSNonce Listing 10 Implemented first message perrigsong exdef x Perrig Song mutual authentication protocol x http ww cs sri com users millen capsl examples html x http sparrow ece cmu edu adrian projects protgen csfw csfw pdf x eXpi version x 1 A gt B alice Na include exdef default exdef include perrigsong exdef let pA 25 27 29 Msg1 A gt B alice Na x new Na PSNonce out cl alice Na let pB x listen to connections on cl x let cl accept gt ChanB c1 in Msg1 A gt B alice Na x in cl name Na free alice ldentifier process new bob Bobld create common communication channel x new cl Channel ChanA lt Msg1 gt pA pB Listing 11 Implemented first message perrigsong expi filename expi Both files can be checked for errors by running expi2java with the type check t flag expi2java t testData expi perrigsong expi c r parsing OK type checking OK inferring types OK checking configuration OK The flag check config c is needed to also check that all types are configured correctly for code generation 3 2 Second Message In the second message Bob encrypts the received nonce together with a fresh nonce and his identity Fortunately the default set of configurations see the Configur
3. console channels generate the prompt message show it to the user and enter the message Afterwards we complete Alice s process by sending the third message let pA let ok eq Nx Na in x User interaction x new cin STDIN new cout STDOUT new prompt PromptMsg out cout prompt in cin message Msg3 A gt B enc Nb M Kab x out c3 enc Nb message Kab process 10 new bob Bobld console channels x new cin STDIN new cout STDOUT Listing 21 Sent the third message perrigsong expi In Bob s process we receive the message decrypt it split the resulting pair check that the received nonce equals the one just sent and display the message to the user let pB Msg3 A gt B enc Nb M Kab x in c3 msg3 let Nx message dec msg3 Kab in let ok eq Nx Nb in show the received message out cout message Listing 22 Received the third message perrigsong expi Finally we get the complete implementation of the Perrig Song mutual authentication protocol in Extensible Spi Calculus 1 x 2 x Perrig Song protocol configuration 3 4 5 config BobldCfg extends ASCIIStringCfg 6 message bob me 8 9 config ChanA extends TcplpChCfg_ x client x 10 variable SMEA y 11 host 127 0 0 1 x ip of the server x 12 port 1234 13 14 15 config ChanB extends TcplpChCfg server x 16 variable cB
4. enc Na Nb bob Kab 3 A gt B enc Nb message Kab include exdef default exdef include perrigsong exdef let pA Msg1 A gt B alice Na x new Na PSNonce out cl alice Na get the saved key for communication wih Bob x new ks_request PSKStoreRequest new ks_answer PSKStoreAnswer out ks_request bob in ks_answer Kab Msg2 B gt A enc Na Nb bob KAB x in c2 msg2 let Nx Nb name dec msg2 Kab in check received data x let ok eq name Nx bob Na in User interaction x new prompt PromptMsg out cout prompt in cin message Msg3 A gt B enc Nb M Kab x out c3 enc Nb message Kab let pB x listen to connections on cl x let cl accept gt ChanB c1 in let c2 accept gt ChanB c2 in let c3 accept gt ChanB c3 in Msg1 A gt B alice Na x 12 ouaaa aaa aaa a A A A B BA SCO MON AAR WBN EP CHOWAN O A 61 62 63 64 65 66 67 68 69 70 71 72 in cl name Na x get the saved key for communication wih Alice x new ks_request PSKStoreRequest new ks_answer PSKStoreAnswer out ks_request name in ks_answer Kab Msg2 B gt A enc Na Nb bob K_AB x new Nb PSNonce out c2 enc Na Nb bob Kab Msg3 A gt B enc Nb M Kab x in c3 msg3 let Nx message dec msg3 Kab in let ok eq Nx Nb in show the received message x out cou
5. runs both participants in parallel to run only one of the participants the option participant can be used With debug some additional information about the protocol progress is shown With keygen and copy key we can modify the contents of a key store 14 Since the Perrig Song protocol relies on the known shared key we first need to create it and store it in the key store java perrigsong Application k alice AESKeyCfg java perrigsong Application c alice bob AESKeyCfg ls jcex jce keystore mv jce keystore key store ls key key store Note that jce keystore is used as the key store filename by default and we need to rename it first to match our settings Now we can finally test the generated protocol We open another shell go to the code directory set up the class path as before and start the server cd testCode expi2java CLASSPATH bin eXpiLibrary jar lib bcprov jdk16 141 jar java perrigsong Application p pB In the previous shell we start the client after some short time a prompt should appear We enter the message Hello and press enter java perrigsong Application p pA Please enter the message Hello This message should be printed on the shell where the server is running then both programs should terminate java perrigsong Application p pB Hello References MM01 J Millen and F Muller Cryptographic protocol generation from CAPSL Techni
6. Expi2Java Tutorial Generating Code For The Perrig Song Protocol Alex Busenius July 29 2009 1 Introduction This tutorial presents the process of writing a formal specification and generating runnable code for the Perrig Song mutual authentication protocol We will start with an informal specification of the protocol and write a formal specification in the Extensible Spi Calculus We will use an iterative approach we will write the protocol specification step by step and add the needed configurations as we need them Finally we will generate Java code implementing the protocol and test the interaction between the participants 2 Informal Specification The Perrig Song protocol is given in Figure 1 Alice Bob Alice Na enc N4 Ng Bob Kag enc Ng M Kap Figure 1 Perrig Song mutual authentication protocol The Perrig Song protocol uses a shared key to authenticate two participants and send an en crypted message It is composed of three message exchanges First the initiator of the protocol Alice sends her identity together with a fresh nonce N4 to the responder Bob Bob encrypts the nonce N4 which he received from Alice together with another fresh nonce Np and his iden tity with the shared key K4pg and sends this encryption to Alice Alice receives the encrypted message decrypts it with the shared key K4g and checks that the nonce N4 inside is the same as her nonce Ny If the nonces mat
7. Na x get the saved key for communication wih Alice x new ks_request PSKStoreRequest new ks_answer PSKStoreAnswer a oma on a N Qo F WN oa om oO Oo ot o0 out ks_request name in ks_answer Kab Msg2 B gt A enc Na Nb bob K_AB new Nb PSNonce out c2 enc Na Nb bob Kab 0 free alice ldentifier process new bob Bobld create common communication channel x new cl Channel ChanA lt Msg1 gt new c2 Channel ChanA lt Msg2 gt new c3 Channel ChanA lt Msg3 gt pA pB Listing 19 Implemented second message perrigsong expi 3 3 Third Message In third message Alice encrypts the previously received nonce Nb together with the text message and sends them to Bob We first need to prompt the user to enter the message and assign the entered text to a variable that we can then encrypt In order to access the console we use the channel configuration ConsoleChCfg and the corresponding typedefs STDIN and STDOUT For the message type we will use String since it is UTF 8 encoded by default We extend the ConstStrCfg to define the prompt message and define the type that the third message is going to have config UserPrompt extends ConstStrCfg message Please enter the message typedef PromptMsg ConstStr UserPrompt typedef Msg3Plain PSNonce String Listing 20 Console configuration perrigsong exdef In Alice s process we set up the
8. PSKStoreAnswer out ks_request bob in ks_answer Kab Msg2 B A enc Na Nb bob K_AB x in c2 msg2 let Nx Nb name dec msg2 Kab in 0 Listing 16 Key store configuration perrigsong exdef Now Alice must check that the received name is Bob and the first nonce equals the one she sent to Bob in the first message otherwise we abort the protocol let pA let Nx Nb name dec msg2 Kab in check received data x let ok eq name Nx bob Na in 0 Listing 17 Checked received data perrigsong expi The result after implementing two messages is as follows Perrig Song protocol configuration config BobldCfg extends ASClIStringCfg Ja message bob config ChanA extends TcplpChCfg_ client x variable cA host 127 0 0 1 x ip of the server x port 1234 config ChanB extends TcplpChCfg server x variable eB host any x listens on all hosts x port 1234 config PSNonceCfg extends NonceCfg Ja size 8 config PSKeyStoreCfg extends KeyStoreChCfg J keystore_filename key store 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 Oo ON Da FF wn Boe Be BP RP a a e wN FO 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 typedef PSNonce Int PSNonceCfg typedef Bobld ConstStr BobldCfg typedef P
9. SKey SymKey AES lt Top gt typedef PSKStoreRequest Channel PSKeyStoreCfg lt Top gt to send a request x typedef PSKStoreAnswer Channel PSKeyStoreCfg lt PSKey gt x to receive a key x typedef Msgl ldentifier PSNonce typedef Msg2Plain PSNonce PSNonce Bobld typedef Msg2 SymEnc AES lt Msg2Plain gt typedef Msg3Plain Top typedef Msg3 SymEnc AES lt Msg3Plain gt Listing 18 Implemented second message perrigsong exdef x Perrig Song mutual authentication protocol x http ww cs sri com users millen capsl examples html x http sparrow ece cmu edu adrian projects protgen csfw csfw pdf x eXpi version x 1 A gt B alice Na x 2 B A enc Na Nb bob Kab include exdef default exdef include perrigsong exdef let let pA Msg1 A gt B alice Na x new Na PSNonce out cl alice Na x get the saved key for communication wih Bob x new ks_request PSKStoreRequest new ks_answer PSKStoreAnswer out ks_request bob in ks_answer Kab Msg2 B gt A enc Na Nb bob K_AB x in c2 msg2 let Nx Nb name dec msg2 Kab in check received data x let ok eq name Nx bob Na in 0 pB x listen to connections on cl x let cl accept gt ChanB c1 in let c2 accept gt ChanB c2 in let c3 accept gt ChanB c3 in Msg1 A gt B alice Na x in cl name
10. anB c3 in Msg1 A gt B alice Na x process create common communication channel x new cl Channel ChanA lt Msg1 gt new c2 Channel ChanA lt Msg2 gt new c3 Channel ChanA lt Msg3 gt pA pB Listing 13 Added remaining channels perrigsong expi We send a request for the key to the key store channel receive a key generate a fresh nonce and send the second message We use the received identity to request the key thus allowing Bob to communicate with other participants as long as he has the corresponding key let pB in cl name Na x get the saved key for communication wih Alice x new ks_request PSKStoreRequest new ks_answer PSKStoreAnswer out ks_request name in ks_answer Kab Msg2 B gt A enc Na Nb bob K_AB x new Nb PSNonce out c2 enc Na Nb bob Kab Listing 14 Sent second message perrigsong expi Now we can change the Msg2Plain typedef to the correct type typedef Msg2Plain PSNonce PSNonce Bobld Listing 15 Key store configuration perrigsong exdef In Alice s process we first get the stored shared key for the communication with Bob in the same way as before then receive the message decrypt it and split the pairs 15 16 17 18 19 20 22 23 24 25 26 27 28 29 let pA out cl alice Na x get the saved key for communication with Bob x new ks_request PSKStoreRequest new ks_answer
11. ations Section of User Manual already contains the configuration AES that has exactly the settings we need by default We have already created the configurations for nonce and Bob s identity so the only part we still need to care about is the way we get the shared key According to the informal specification we store the key using the Java key store mechanism in the file key store The default library of cryptographic primitives and data structures provides a special channel configuration KeyStoreChCfg that can be used to retrieve the key We extend the key store configuration in order to set up the file name We also define a typedef for the key type two typedefs for the key store channels and preliminary typedefs for message types encrypted and plaintext config PSKeyStoreCfg extends KeyStoreChCfg keystore filename key store typedef PSKey SymKey AESKeyCfg lt Top gt typedef PSKStoreRequest Channel PSKeyStoreCfg lt Top gt x to send a request typedef PSKStoreAnswer Channel PSKeyStoreCfg lt PSKey gt to receive a key x typedef Msg2Plain Top typedef Msg2 SymEnc AES lt Msg2Plain gt Listing 12 Key store configuration perrigsong exdef We set up the communication channels for the second message in the same way as for the first message let pB x listen to connections on cl x let cl accept gt ChanB c1 in let c2 accept gt ChanB c2 in let c3 accept gt Ch
12. cal Report SRI CSL 01 07 SRI International December 2001 1 List of Figures 1 Perrig Song mutual authentication protocol osoo e e 2 ee 1 15 Listings OOAONDOTKBWNHFH j j pe vrrrirrvrovnrnrernrerrernerneme OOA WwWNhNhrF OwWOoOnr nm or WLW bY Simple setup perrigsong expi os sso co kere ad eee eee aes 2 Simple setup perrigsong exdef eroe dut rc Etra 3 Added Alice s identity perrigsong expi aoaaa a 3 Added BobldCfg perrigsong exdef aoao a 3 Added Bob s identity perrigsong expi s a a 3 Channel configurations perrigsong exdef aaau 4 Created a common channel perrigsong expi aaao 4 Nonce configuration perrigsong exdef ossaa 4 First message perrigsong eZpi s o sa sy ren agaaa aa a ee A a 4 Implemented first message perrigsong exdef aaou a 5 Implemented first message perrigsong eXpi aaou a 5 Key store configuration perrigsong exdef l oaoa a 6 Added remaining channels perrigsong expi oaoa a 1 Sent second message perrigsong expi oaao e a 7 Key store configuration perrigsong exdef 00 7 Key store configuration perrigsong exdef 00 8 Checked received data perrigsong expi 00 0 000004 8 Implemented second message perrigsong exdef 8 Implemented second message perrigsong expi 9 Console configuration perrigsong exdef 000 10 Sent the thir
13. ch she encrypts the received nonce Ng and a message M Can be found as one of the examples for CAPSL by J Millen et al MMO1 at http www csl sri com users millen capsl examples html she wanted to send with the shared key K4pg and sends the resulting message to Bob Bob decrypts the message and checks that the received nonce Nj is the same as his nonce Np If the nonces match the protocol completes successfully We will assume that the identities are UTF 8 encoded strings nonces are randomly chosen 64 bit integers and the used encryption is AES 256 Further we will use the usual Java key store mechanism to store the shared key in the file key store that is supposed to be first shared between Alice and Bob in a secure way For communication we will use TCP IP the data will be sent from IP 127 0 0 1 to IP 127 0 0 1 on the port 1234 The localhost is only used here for convenience the example can be easily extended to use the LAN by specifying the according IP addresses in the configuration The message that Alice sends to Bob will be an UTF 8 encoded string We will generate two programs called progA and progB one for each participant Since TCP IP assumes one of the participants to be a server and all other to be clients progB will act as a server and progA will act as a client For simplicity both programs will have a simple command line interface In a successful protocol run progA will prompt the user to enter the message an
14. d BobldCfg perrigsong exdef Then we create a fresh name bob in the main process it should be visible in both named processes process new bob ConstStr BobldCfg pA pB Listing 5 Added Bob s identity perrigsong expi Now we need to set up the communication channel for the first message First we create two TCP IP channel configurations one for each participant and set them up according to the informal specification We will also need to enter the type of the first message soon we don t know it at this point but we can already create a dummy typedef for it config ChanA extends TcplpChCfg_ gt client x variable SMAS host 127 0 0 1 x ip of the server x port 1234 config ChanB extends TcplpChCfg server x variable cB host any x listens on all hosts x port 1234 Ja typedef Msgl Top Listing 6 Channel configurations perrigsong exdef Now we create a common channel c1 and start a server on Bob s side by calling accept We use the typedef Msg1 as the type of the first message let pB x listen to connections on cl x let cl accept gt ChanB c1 in 0 process new bob ConstStr BobldCfg create common communication channel x new cl Channel ChanA lt Msg1 gt pA pB Listing 7 Created a common channel perrigsong expi Finally we generate a fresh nonce and let Alice send it in the first message We define a confi
15. d message perrigsong expi 0 000 10 Received the third message perrigsong expi 00 11 Perrig Song mutual authentication protocol perrigsong exdef 11 Perrig Song mutual authentication protocol perrigsong expi 12 Generated perrigsong Application java 02004 14 Initialized free names in perrigsong Application java 14 16
16. d progB will display the received message In case of an error the programs will abort with an error message 3 Formal Specification in Extensible Spi Calculus We will write the formal specification iteratively message by message First we create two new files in testData expi perrigsong expi and perrigsong exdef To be able to use the provided types and constructors see the Input Language Section of User Manual we include the file default exdef We will put all custom configurations into perrigsong exdef it should also be included Furthermore we add two empty processes named pA and pB and let them be executed in parallel to model the interaction of two participants x Perrig Song mutual authentication protocol x http ww cs sri com users millen capsl examples html x http sparrow ece cmu edu adrian projects protgen csfw csfw pdf x eXpi version include exdef default exdef include perrigsong exdef let pA 0 let pB 0 process pA pB Listing 1 Simple setup perrigsong expi N The configuration file only contains a comment for now x Perrig Song protocol configuration Listing 2 Simple setup perrigsong exdef 3 1 First Message In the first message Alice sends a concatenation of her identity and a fresh nonce to Bob over a communication channel To do this we first need to set up a channel declare the needed variables and generate a nonce I
17. guration for the 64 bit nonce and a short typedef for convenience config PSNonceCfg extends NonceCfg size 8 typedef PSNonce Int PSNonceCfg Listing 8 Nonce configuration perrigsong exdef In Alice s process we generate a fresh nonce and send the first message In Bob s process we receive the message and give both components a name let pA Msg1 A gt B alice Na x new Na PSNonce out cl alice Na let pB oma Naw Ff won W W N nn nN NNN NNN KK KB BBB BB BP H O O WN DoT FF wWwnNrF O HDT AN DTH FF WN FP OO omar oan amp pr wn Fe Boe 1 2 13 14 an Msg1 A gt B alice Na x in cl name Na Listing 9 First message perrigsong expi At this point we can finally correct the type of the first message we preliminary set to Top it should be ldentifier PSNonce Additionally we define a shorter typedef for ConstStr BobldCfg and use it in the code As the result we get x Perrig Song protocol configuration config BobldCfg extends ASCIIStringCfg message bob config ChanA extends TcplpChCfg_ client x variable er cy eae host 127 0 0 1 x ip of the server x port 1234 config ChanB extends TcplpChCfg server x variable ne B host any x listens on all hosts x port 1234 Ja config PSNonceCfg extends NonceCfg size 8 typedef PSNonce Int PSNonceCfg
18. n general constant terms can be modelled in two different ways as free variables or fresh names Fresh names are generated using the restriction process new a P and must initialized using configurations The disadvantage of the restriction processes is however that it can only handle terms of generative types Free variables are declared using the free a construct and can have any type but must be initialized manually by modifying the generated code Identities of both participants are constant strings we can use the generative type ConstStr and configuration ConstStrCfg to model them but there is also a specialized configuration IdentifierCfg that is used together with the non generative type String to model identifiers As an example we will use both representations a free variable alice of type ldentifier as Alice s identity and a fresh name bob of type String as Bob s identity In order to declare Alice s identity we only need to add the declaration line with the type annotation just before process free alice ldentifier process pA pB Listing 3 Added Alice s identity perrigsong expi Generating Bob s identity as a fresh name requires adjusting the ConstStrCfg configuration we need to set up the value of the generated string First we create a configuration called BobldCfg by extending ConstStrCfg in perrigsong exdef config BobldCfg extends ConstStrCfg message bob Listing 4 Adde
19. t message free alice ldentifier process new bob Bobld x console channels x new cin STDIN new cout STDOUT create common communication channel x new cl Channel ChanA lt Msgl1 gt new c2 Channel ChanA lt Msg2 gt new c3 Channel ChanA lt Msg3 gt pA pB Listing 24 Perrig Song mutual authentication protocol perrigsong expi 4 Code Generation The code generation step is automated only some configuration options must be specified by the user We will use the testCode expi2java perrigsong directory as the target directory and perrigsong as the package name The implementation class will be called PerrigSong We will use the default code templates in data expi2java javaTemplates and no additional imports since we do not use any additional implementation classes In addition the output directory must be created first This results in the following calls mkdir testCode expi2java perrigsong expi2java g testData expi perrigsong expi p perrigsong m data expi2java javaTemplates o testCode expi2java perrigsong n PerrigsSong parsing OK type checking OK inferring types OK checking configuration OK generating code OK 13 Since we decided to use a free name for the Alice s identity in Section 3 1 we need to initialize all free names in the generated code We go to the code directory and open the file perrigsong Application java and search for
20. the word FIXME In the lines 102 103 we find the following code FIXME all free names are user provided initialize and finalize them Identifier alice_139 null Listing 25 Generated perrigsong Application java We change it to Identifier alice_139 new Identifier alice Listing 26 Initialized free names in perrigsong Application java Now we need to compile the generated code We set the class path to contain the library and the Bouncy Castle Provider Jar file and run the compiler cd testCode expi2java CLASSPATH bin eXpiLibrary jar lib bcprov jdk16 141 jar javac perrigsong java Now we can start the generated test application java perrigsong Application help eXpi2Java protocol test Run the generated PerrigSong protocol USAGE h options OPTIONS h help Print this help d debug Enable debug modus show Show the content of the keystore buggy k lt name gt lt config gt keygen lt name gt lt config gt Generate a new symmetric key store it under this name and exit c lt from gt lt to gt lt config gt copy key lt from gt lt to gt lt config gt Copy a symmetric key stored under the name lt from gt as lt to gt and exit p lt name gt participant lt name gt Only run code for this participant lt name gt can be on of pA pB The default test application offer several options If started without parameters it
Download Pdf Manuals
Related Search