Download Expi2Java Tutorial

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 protocol1 . 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 )
o
enc((NA , NB , Bob), KAB )
enc((NB , M ), KAB )
/
Figure 1: Perrig-Song mutual authentication protocol
The Perrig-Song protocol uses a shared key to authenticate two participants and send an encrypted message. It is composed of three message exchanges. First, the initiator of the protocol,
Alice, sends her identity together with a fresh nonce NA to the responder, Bob. Bob encrypts
the nonce NA , which he received from Alice together with another fresh nonce NB and his identity with the shared key KAB and sends this encryption to Alice. Alice receives the encrypted
message, decrypts it with the shared key KAB and checks that the nonce NA0 inside is the same
as her nonce NA . If the nonces match, she encrypts the received nonce NB and a message M
1
Can be found as one of the examples for CAPSL by J. Millen et al. [MM01], at http://www.csl.sri.com/
users/millen/capsl/examples.html
1
she wanted to send with the shared key KAB and sends the resulting message to Bob. Bob
decrypts the message and checks that the received nonce NB0 is the same as his nonce NB . 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
and 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:
1
2
3
4
5
6
7
(∗
∗ P e r r i g −Song m u t u a l a u t h e n t i c a t i o n p r o t o c o l
∗
∗ h t t p : / /www . c s l . s r i . com/ u s e r s / m i l l e n / c a p s l / e x a m p l e s . h tm l
∗ h t t p : / / s p a r r o w . e c e . cmu . edu /˜ a d r i a n / p r o j e c t s / p r o t g e n −c s f w / c s f w . p d f
∗ eXpi v e r s i o n
∗)
8
9
10
include ” . . / exdef / default . exdef ”
include ” perrigsong . exdef ”
11
12
13
14
l e t pA =
0.
15
16
17
l e t pB =
0.
18
19
20
process
( pA | pB )
Listing 1: Simple setup: perrigsong.expi
2
The configuration file only contains a comment for now:
1
2
3
(∗
∗ P e r r i g −Song p r o t o c o l c o n f i g u r a t i o n
∗)
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.
In 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 $Identifier 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 a l i c e : $ I d e n t i f i e r
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 BobIdCfg
by extending ConstStrCfg in perrigsong.exdef:
c o n f i g B o bIdCfg e x t e n d s C o n s t S t r C f g (
message = ” bob ”
).
Listing 4: Added BobIdCfg: perrigsong.exdef
Then we create a fresh name bob in the main process (it should be visible in both named
processes):
process
new bob : C o n s t S t r @ B o b I d C f g ;
( pA | pB )
Listing 5: Added Bob’s identity: perrigsong.expi
3
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.
c o n f i g ChanA e x t e n d s T c p I p C h C f g ( ( ∗ c l i e n t ∗ )
variable
= ”cA” ,
host
= ” 1 2 7 . 0 . 0 . 1 ” , (∗ i p of the s e r v e r ∗)
port
= ” 1234 ”
).
c o n f i g ChanB e x t e n d s T c p I p C h C f g ( ( ∗ s e r v e r ∗ )
variable
= ”cB” ,
host
= ” any ” , ( ∗ l i s t e n s on a l l h o s t s ∗ )
port
= ” 1234 ”
).
t y p e d e f $Msg1 = 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.
l e t pB =
( ∗ l i s t e n t o c o n n e c t i o n s on c1 ∗ )
l e t c1 = a c c e p t [−>@ChanB ] ( c1 ) i n
0.
...
process
new bob : C o n s t S t r @ B o b I d C f g ;
( ∗ c r e a t e common c o m m u n i c a t i o n c h a n n e l ∗ )
new c1 : Channel@ChanA<$Msg1 >;
( 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
configuration for the 64-bit nonce and a short typedef for convenience:
c o n f i g PSNonceCfg e x t e n d s NonceCfg (
s i z e = ”8”
).
t y p e d e f $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:
l e t pA =
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
new Na : $PSNonce ;
out ( c1 , ( a l i c e , Na ) ) .
l e t pB =
...
4
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
i n ( c1 , ( 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 ( $Identifier , $PSNonce). Additionally, we define a shorter typedef for ConstStr@BobIdCfg
and use it in the code. As the result, we get:
1
2
3
(∗
∗ P e r r i g −Song p r o t o c o l c o n f i g u r a t i o n
∗)
4
5
6
7
c o n f i g B o bIdCfg e x t e n d s A S C I I S t r i n g C f g (
message = ” bob ”
).
8
9
10
11
12
13
c o n f i g ChanA e x t e n d s T c p I p C h C f g ( ( ∗ c l i e n t ∗ )
variable
= ”cA” ,
host
= ” 1 2 7 . 0 . 0 . 1 ” , (∗ i p of the s e r v e r ∗)
port
= ” 1234 ”
).
14
15
16
17
18
19
c o n f i g ChanB e x t e n d s T c p I p C h C f g ( ( ∗ s e r v e r ∗ )
variable
= ”cB” ,
host
= ” any ” , ( ∗ l i s t e n s on a l l h o s t s ∗ )
port
= ” 1234 ”
).
20
21
22
23
c o n f i g PSNonceCfg e x t e n d s NonceCfg (
s i z e = ”8”
).
24
25
26
t y p e d e f $PSNonce = Int@PSNonceCfg .
27
28
t y p e d e f $BobId
= ConstStr@BobIdCfg .
29
30
31
t y p e d e f $Msg1 = ( $ I d e n t i f i e r , $PSNonce ) .
Listing 10: Implemented first message: perrigsong.exdef
1
2
3
4
5
6
7
8
9
(∗
∗ P e r r i g −Song m u t u a l a u t h e n t i c a t i o n p r o t o c o l
∗
∗ h t t p : / /www . c s l . s r i . com/ u s e r s / m i l l e n / c a p s l / e x a m p l e s . h tm l
∗ h t t p : / / s p a r r o w . e c e . cmu . edu /˜ a d r i a n / p r o j e c t s / p r o t g e n −c s f w / c s f w . p d f
∗ eXpi v e r s i o n
∗
∗ 1 . A−>B : ( a l i c e , Na )
∗)
10
11
12
include ” . . / exdef / default . exdef ”
include ” perrigsong . exdef ”
13
14
15
l e t pA =
5
16
17
18
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
new Na : $PSNonce ;
out ( c1 , ( a l i c e , Na ) ) .
19
20
21
22
23
24
l e t pB =
( ∗ l i s t e n t o c o n n e c t i o n s on c1 ∗ )
l e t c1 = a c c e p t [−>@ChanB ] ( c1 ) i n
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
i n ( c1 , ( name , Na ) ) .
25
26
27
free a l i c e : $ I d e n t i f i e r .
28
29
30
31
32
33
process
new bob : $BobId ;
( ∗ c r e a t e common c o m m u n i c a t i o n c h a n n e l ∗ )
new c1 : Channel@ChanA<$Msg1 >;
( 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 “Configurations” 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):
c o n f i g P SKeyStoreCfg e x t e n d s K e y S t o r e C h C f g (
k e y s t o r e f i l e n a m e = ” key . s t o r e ” ,
).
6
t y p e d e f $PSKey
= SymKey@AESKeyCfg<Top>.
t y p e d e f $ P S K S t o r e R e q u e s t = Channel@PSKeyStoreCfg<Top>. ( ∗ t o s e n d a r e q u e s t ∗ )
t y p e d e f $PSKStoreAnswer = Channel@PSKeyStoreCfg<$PSKey >. ( ∗ t o r e c e i v e a k e y ∗ )
typedef $Msg2Plain
t y p e d e f $Msg2
= Top .
= SymEnc@AES<$Msg2Plain >.
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:
l e t pB =
( ∗ l i s t e n t o c o n n e c t i o n s on c1 ∗ )
l e t c1 = a c c e p t [−>@ChanB ] ( c1 ) i n
l e t c2 = a c c e p t [−>@ChanB ] ( c2 ) i n
l e t c3 = a c c e p t [−>@ChanB ] ( c3 ) i n
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
...
process
...
( ∗ c r e a t e common c o m m u n i c a t i o n c h a n n e l ∗ )
new c1 : Channel@ChanA<$Msg1 >;
new c2 : Channel@ChanA<$Msg2 >;
new c3 : Channel@ChanA<$Msg3 >;
( 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:
l e t pB =
...
i n ( c1 , ( name , Na ) ) ;
( ∗ g e t t h e s a v e d k e y f o r c o m m u n i c a t i o n wih A l i c e ∗ )
new k s r e q u e s t : $ P S K S t o r e R e q u e s t ;
new k s a n s w e r : $PSKStoreAnswer ;
out ( k s r e q u e s t , name ) ;
i n ( k s a n s w e r , Kab ) ;
( ∗ Msg2 . B−>A : e n c ( ( Na , Nb , bob ) , K AB ) ∗ )
new Nb : $PSNonce ;
out ( c2 , e n c ( ( 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 , $BobId ) .
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:
7
l e t pA =
...
out ( c1 , ( a l i c e , Na ) ) ;
( ∗ g e t t h e s a v e d k e y f o r c o m m u n i c a t i o n w i t h Bob ∗ )
new k s r e q u e s t : $ P S K S t o r e R e q u e s t ;
new k s a n s w e r : $PSKStoreAnswer ;
out ( k s r e q u e s t , bob ) ;
i n ( k s a n s w e r , Kab ) ;
( ∗ Msg2 . B−>A : e n c ( ( Na , Nb , bob ) , K AB ) ∗ )
i n ( c2 , msg2 ) ;
l e t ( Nx , Nb , name ) = d e c ( msg2 , Kab ) i n
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:
l e t pA =
...
l e t ( Nx , Nb , name ) = d e c ( msg2 , Kab ) i n
(∗ check r e c e i v e d data ∗)
l e t ok = eq ( ( name , Nx ) , ( bob , Na ) ) i n
0.
Listing 17: Checked received data: perrigsong.expi
The result after implementing two messages is as follows:
1
2
3
(∗
∗ P e r r i g −Song p r o t o c o l c o n f i g u r a t i o n
∗)
4
5
6
7
c o n f i g B o bIdCfg e x t e n d s A S C I I S t r i n g C f g (
message = ” bob ”
).
8
9
10
11
12
13
c o n f i g ChanA e x t e n d s T c p I p C h C f g ( ( ∗ c l i e n t ∗ )
variable
= ”cA” ,
host
= ” 1 2 7 . 0 . 0 . 1 ” , (∗ i p of the s e r v e r ∗)
port
= ” 1234 ”
).
14
15
16
17
18
19
c o n f i g ChanB e x t e n d s T c p I p C h C f g ( ( ∗ s e r v e r ∗ )
variable
= ”cB” ,
host
= ” any ” , ( ∗ l i s t e n s on a l l h o s t s ∗ )
port
= ” 1234 ”
).
20
21
22
23
c o n f i g PSNonceCfg e x t e n d s NonceCfg (
s i z e = ”8”
).
24
25
26
27
c o n f i g P SKeyStoreCfg e x t e n d s K e y S t o r e C h C f g (
k e y s t o r e f i l e n a m e = ” key . s t o r e ”
).
28
29
8
30
t y p e d e f $PSNonce = Int@PSNonceCfg .
31
32
t y p e d e f $BobId
= ConstStr@BobIdCfg .
t y p e d e f $PSKey
= SymKey@AES<Top>.
33
34
35
36
37
t y p e d e f $ P S K S t o r e R e q u e s t = Channel@PSKeyStoreCfg<Top>. ( ∗ t o s e n d a r e q u e s t ∗ )
t y p e d e f $PSKStoreAnswer = Channel@PSKeyStoreCfg<$PSKey >. ( ∗ t o r e c e i v e a k e y ∗ )
38
39
40
41
42
43
44
typedef
typedef
typedef
typedef
typedef
$Msg1
$Msg2Plain
$Msg2
$Msg3Plain
$Msg3
=
=
=
=
=
( $ I d e n t i f i e r , $PSNonce ) .
( $PSNonce , $PSNonce , $BobId ) .
SymEnc@AES<$Msg2Plain >.
Top .
SymEnc@AES<$Msg3Plain >.
Listing 18: Implemented second message: perrigsong.exdef
1
2
3
4
5
6
7
8
9
10
(∗
∗ P e r r i g −Song m u t u a l a u t h e n t i c a t i o n p r o t o c o l
∗
∗ h t t p : / /www . c s l . s r i . com/ u s e r s / m i l l e n / c a p s l / e x a m p l e s . h tm l
∗ h t t p : / / s p a r r o w . e c e . cmu . edu /˜ a d r i a n / p r o j e c t s / p r o t g e n −c s f w / c s f w . p d f
∗ eXpi v e r s i o n
∗
∗ 1 . A−>B : ( a l i c e , Na )
∗ 2 . B−>A : e n c ( ( Na , Nb , bob ) , Kab )
∗)
11
12
13
include ” . . / exdef / default . exdef ”
include ” perrigsong . exdef ”
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
l e t pA =
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
new Na : $PSNonce ;
out ( c1 , ( a l i c e , Na ) ) ;
( ∗ g e t t h e s a v e d k e y f o r c o m m u n i c a t i o n wih Bob ∗ )
new k s r e q u e s t : $ P S K S t o r e R e q u e s t ;
new k s a n s w e r : $PSKStoreAnswer ;
out ( k s r e q u e s t , bob ) ;
i n ( k s a n s w e r , Kab ) ;
( ∗ Msg2 . B−>A : e n c ( ( Na , Nb , bob ) , K AB ) ∗ )
i n ( c2 , msg2 ) ;
l e t ( Nx , Nb , name ) = d e c ( msg2 , Kab ) i n
(∗ check r e c e i v e d data ∗)
l e t ok = eq ( ( name , Nx ) , ( bob , Na ) ) i n
0.
31
32
33
34
35
36
37
38
39
40
41
l e t pB =
( ∗ l i s t e n t o c o n n e c t i o n s on c1 ∗ )
l e t c1 = a c c e p t [−>@ChanB ] ( c1 ) i n
l e t c2 = a c c e p t [−>@ChanB ] ( c2 ) i n
l e t c3 = a c c e p t [−>@ChanB ] ( c3 ) i n
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
i n ( c1 , ( name , Na ) ) ;
( ∗ g e t t h e s a v e d k e y f o r c o m m u n i c a t i o n wih A l i c e ∗ )
new k s r e q u e s t : $ P S K S t o r e R e q u e s t ;
new k s a n s w e r : $PSKStoreAnswer ;
9
42
43
44
45
46
47
out ( k s r e q u e s t , name ) ;
i n ( k s a n s w e r , Kab ) ;
( ∗ Msg2 . B−>A : e n c ( ( Na , Nb , bob ) , K AB ) ∗ )
new Nb : $PSNonce ;
out ( c2 , e n c ( ( Na , Nb , bob ) , Kab ) ) ;
0.
48
49
50
free a l i c e : $ I d e n t i f i e r .
51
52
53
54
55
56
57
58
process
new bob : $BobId ;
( ∗ c r e a t e common c o m m u n i c a t i o n c h a n n e l ∗ )
new c1 : Channel@ChanA<$Msg1 >;
new c2 : Channel@ChanA<$Msg2 >;
new c3 : Channel@ChanA<$Msg3 >;
( 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:
c o n f i g UserPrompt e x t e n d s C o n s t S t r C f g ( message = ” P l e a s e e n t e r t h e message : ” ) .
t y p e d e f $PromptMsg = C o n s t S t r @ U s e r P r o m p t .
typedef $Msg3Plain
= ( $PSNonce , S t r i n g ) .
Listing 20: Console configuration: perrigsong.exdef
In Alice’s process, we set up the 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:
l e t pA =
...
l e t ok = eq ( Nx , Na ) i n
(∗ User i n t e r a c t i o n ∗)
new c i n : $STDIN ;
new c o u t : $STDOUT ;
new prompt : $PromptMsg ;
out ( cout , prompt ) ;
i n ( c i n , message ) ;
( ∗ Msg3 . A−>B : e n c ( ( Nb , M) , Kab ) ∗ )
out ( c3 , e n c ( ( Nb , message ) , Kab ) ) .
...
process
10
new bob : $BobId ;
(∗ c o n s o l e c h a n n e l s ∗)
new c i n : $STDIN ;
new c o u t : $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:
l e t pB =
...
( ∗ Msg3 . A−>B : e n c ( ( Nb , M) , Kab ) ∗ )
i n ( c3 , msg3 ) ;
l e t ( Nx , message ) = d e c ( msg3 , Kab ) i n
l e t ok = eq ( Nx , Nb ) i n
( ∗ show t h e r e c e i v e d 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
2
3
(∗
∗ P e r r i g −Song p r o t o c o l c o n f i g u r a t i o n
∗)
4
5
6
7
c o n f i g B o bIdCfg e x t e n d s A S C I I S t r i n g C f g (
message = ” bob ”
).
8
9
10
11
12
13
c o n f i g ChanA e x t e n d s T c p I p C h C f g ( ( ∗ c l i e n t ∗ )
variable
= ”cA” ,
host
= ” 1 2 7 . 0 . 0 . 1 ” , (∗ i p of the s e r v e r ∗)
port
= ” 1234 ”
).
14
15
16
17
18
19
c o n f i g ChanB e x t e n d s T c p I p C h C f g ( ( ∗ s e r v e r ∗ )
variable
= ”cB” ,
host
= ” any ” , ( ∗ l i s t e n s on a l l h o s t s ∗ )
port
= ” 1234 ”
).
20
21
22
23
c o n f i g PSNonceCfg e x t e n d s NonceCfg (
s i z e = ”8”
).
24
25
26
27
c o n f i g P SKeyStoreCfg e x t e n d s K e y S t o r e C h C f g (
k e y s t o r e f i l e n a m e = ” key . s t o r e ”
).
28
29
30
t y p e d e f $PSNonce = Int@PSNonceCfg .
31
32
t y p e d e f $BobId
= ConstStr@BobIdCfg .
33
11
34
t y p e d e f $PSKey
= SymKey@AES<Top>.
35
36
37
t y p e d e f $ P S K S t o r e R e q u e s t = Channel@PSKeyStoreCfg<Top>. ( ∗ t o s e n d a r e q u e s t ∗ )
t y p e d e f $PSKStoreAnswer = Channel@PSKeyStoreCfg<$PSKey >. ( ∗ t o r e c e i v e a k e y ∗ )
38
39
40
c o n f i g UserPrompt e x t e n d s C o n s t S t r C f g ( message = ” P l e a s e e n t e r t h e message : ” ) .
t y p e d e f $PromptMsg = C o n s t S t r @ U s e r P r o m p t .
41
42
43
44
45
46
typedef
typedef
typedef
typedef
typedef
$Msg1
$Msg2Plain
$Msg2
$Msg3Plain
$Msg3
=
=
=
=
=
( $ I d e n t i f i e r , $PSNonce ) .
( $PSNonce , $PSNonce , $BobId ) .
SymEnc@AES<$Msg2Plain >.
( $PSNonce , S t r i n g ) .
SymEnc@AES<$Msg3Plain >.
Listing 23: Perrig-Song mutual authentication protocol: perrigsong.exdef
1
2
3
4
5
6
7
8
9
10
11
(∗
∗ P e r r i g −Song m u t u a l a u t h e n t i c a t i o n p r o t o c o l
∗
∗ h t t p : / /www . c s l . s r i . com/ u s e r s / m i l l e n / c a p s l / e x a m p l e s . h tm l
∗ h t t p : / / s p a r r o w . e c e . cmu . edu /˜ a d r i a n / p r o j e c t s / p r o t g e n −c s f w / c s f w . p d f
∗ eXpi v e r s i o n
∗
∗ 1 . A−>B : ( a l i c e , Na )
∗ 2 . B−>A : e n c ( ( Na , Nb , bob ) , Kab )
∗ 3 . A−>B : e n c ( ( Nb , message ) , Kab )
∗)
12
13
14
include ” . . / exdef / default . exdef ”
include ” perrigsong . exdef ”
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
l e t pA =
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
new Na : $PSNonce ;
out ( c1 , ( a l i c e , Na ) ) ;
( ∗ g e t t h e s a v e d k e y f o r c o m m u n i c a t i o n wih Bob ∗ )
new k s r e q u e s t : $ P S K S t o r e R e q u e s t ;
new k s a n s w e r : $PSKStoreAnswer ;
out ( k s r e q u e s t , bob ) ;
i n ( k s a n s w e r , Kab ) ;
( ∗ Msg2 . B−>A : e n c ( ( Na , Nb , bob ) , K AB ) ∗ )
i n ( c2 , msg2 ) ;
l e t ( Nx , Nb , name ) = d e c ( msg2 , Kab ) i n
(∗ check r e c e i v e d data ∗)
l e t ok = eq ( ( name , Nx ) , ( bob , Na ) ) i n
(∗ User i n t e r a c t i o n ∗)
new prompt : $PromptMsg ;
out ( cout , prompt ) ;
i n ( c i n , message ) ;
( ∗ Msg3 . A−>B : e n c ( ( Nb , M) , Kab ) ∗ )
out ( c3 , e n c ( ( Nb , message ) , Kab ) ) .
37
38
39
40
41
42
43
l e t pB =
( ∗ l i s t e n t o c o n n e c t i o n s on c1 ∗ )
l e t c1 = a c c e p t [−>@ChanB ] ( c1 ) i n
l e t c2 = a c c e p t [−>@ChanB ] ( c2 ) i n
l e t c3 = a c c e p t [−>@ChanB ] ( c3 ) i n
( ∗ Msg1 . A−>B : ( a l i c e , Na ) ∗ )
12
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
i n ( c1 , ( name , Na ) ) ;
( ∗ g e t t h e s a v e d k e y f o r c o m m u n i c a t i o n wih A l i c e ∗ )
new k s r e q u e s t : $ P S K S t o r e R e q u e s t ;
new k s a n s w e r : $PSKStoreAnswer ;
out ( k s r e q u e s t , name ) ;
i n ( k s a n s w e r , Kab ) ;
( ∗ Msg2 . B−>A : e n c ( ( Na , Nb , bob ) , K AB ) ∗ )
new Nb : $PSNonce ;
out ( c2 , e n c ( ( Na , Nb , bob ) , Kab ) ) ;
( ∗ Msg3 . A−>B : e n c ( ( Nb , M) , Kab ) ∗ )
i n ( c3 , msg3 ) ;
l e t ( Nx , message ) = d e c ( msg3 , Kab ) i n
l e t ok = eq ( Nx , Nb ) i n
( ∗ show t h e r e c e i v e d message ∗ )
out ( cout , message ) .
59
60
61
free a l i c e : $ I d e n t i f i e r .
62
63
64
65
66
67
68
69
70
71
72
process
new bob : $BobId ;
(∗ c o n s o l e c h a n n e l s ∗)
new c i n : $STDIN ;
new c o u t : $STDOUT ;
( ∗ c r e a t e common c o m m u n i c a t i o n c h a n n e l ∗ )
new c1 : Channel@ChanA<$Msg1 >;
new c2 : Channel@ChanA<$Msg2 >;
new c3 : Channel@ChanA<$Msg3 >;
( 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 "PerrigSong"
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
the word “FIXME”. In the lines 102-103 we find the following code:
// FIXME a l l f r e e names a r e u s e r −p r o v i d e d ,
I d e n t i f i e r alice 139 = null ;
i n i t i a l i z e and f i n a l i z e them . . .
Listing 25: Generated perrigsong/Application.java
We change it to:
Identifier
a l i c e 1 3 9 = new I d e n t i f i e r ( ” a l i c e ” ) ;
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
-d, --debug
--show
-k <name> <config>
--keygen <name> <config>
: Print this help
: Enable debug modus
: Show the content of the keystore (buggy)
: Generate a new symmetric key, store it under
this name and exit
-c <from> <to> <config>
--copy-key <from> <to> <config>
: Copy a symmetric key stored under the name
<from> as <to> and exit
-p <name>
--participant <name>
: Only run code for this participant
<name> can be on of: pA, pB
The default test application offer several options. If started without parameters, it 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 jce*
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. Technical
Report SRI-CSL-01-07, SRI International, December 2001. 1
List of Figures
1
Perrig-Song mutual authentication protocol . . . . . . . . . . . . . . . . . . . . .
15
1
Listings
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
Simple setup: perrigsong.expi . . . . . . . . . . . . . . . . . .
Simple setup: perrigsong.exdef . . . . . . . . . . . . . . . . . .
Added Alice’s identity: perrigsong.expi . . . . . . . . . . . . .
Added BobIdCfg: perrigsong.exdef . . . . . . . . . . . . . . . .
Added Bob’s identity: perrigsong.expi . . . . . . . . . . . . . .
Channel configurations: perrigsong.exdef . . . . . . . . . . . .
Created a common channel: perrigsong.expi . . . . . . . . . .
Nonce configuration: perrigsong.exdef . . . . . . . . . . . . . .
First message: perrigsong.expi . . . . . . . . . . . . . . . . . .
Implemented first message: perrigsong.exdef . . . . . . . . . .
Implemented first message: perrigsong.expi . . . . . . . . . . .
Key store configuration: perrigsong.exdef . . . . . . . . . . . .
Added remaining channels: perrigsong.expi . . . . . . . . . . .
Sent second message: perrigsong.expi . . . . . . . . . . . . . .
Key store configuration: perrigsong.exdef . . . . . . . . . . . .
Key store configuration: perrigsong.exdef . . . . . . . . . . . .
Checked received data: perrigsong.expi . . . . . . . . . . . . .
Implemented second message: perrigsong.exdef . . . . . . . . .
Implemented second message: perrigsong.expi . . . . . . . . .
Console configuration: perrigsong.exdef . . . . . . . . . . . . .
Sent the third message: perrigsong.expi . . . . . . . . . . . . .
Received the third message: perrigsong.expi . . . . . . . . . .
Perrig-Song mutual authentication protocol: perrigsong.exdef
Perrig-Song mutual authentication protocol: perrigsong.expi .
Generated perrigsong/Application.java . . . . . . . . . . . .
Initialized free names in perrigsong/Application.java . . . .
16
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2
3
3
3
3
4
4
4
4
5
5
6
7
7
7
8
8
8
9
10
10
11
11
12
14
14